[antonkov]

Change

Part of #1226.

Adds Complexity/Computability/Complexity/FineGrained/SparseCountingScale.lean and concrete tests in ComplexityTests/SparseCountingScale.lean, formalizing the exact integer-comparison floor characterization and sharp permanent $s_n \ge 2$ threshold for Proposition 6.4's discrete sparsification parameter $s_n = \lfloor \sqrt{\lambda_n} / \nu_n^2 \rfloor$ (reusing Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups and Nat.clog directly for $\lambda_n = \lceil \log_2 n \rceil$ and $\nu_n = \lceil \log_2 \lambda_n \rceil$), the tree-exponent bound $n / s_n = O(\rho(n))$, the polylogarithmic and quasi-polynomial query-overhead absorption underlying equation (6.4), the leaf-occurrence bound $B = O_k((s_n \log s_n)^{k-1}) \le \lambda_n^k$ discharging Lemma 4.8 replacement feasibility, and the uniform runtime-composition theorems of §6.3 equation (6.4) and §6.4 Proposition 6.4 from [OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH] (pinned revision 7ef5c0cc, printed pp. 43–44).

Source statements ([OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH], printed pp. 43–44)

(Mathematical-transcription note: Plain-text extraction from the source PDF flattens rendered superscripts, subscripts, radicals, and floor/ceiling delimiters such as $3n(2m)^P + 1$, $O_k(1)$, $2^{O_k(n(\log \log n)^2 / \sqrt{\log n})}$, $\sigma^{-1}$, $\lambda_n = \lceil \log_2 n \rceil$, $\nu_n = \lceil \log_2 \lambda_n \rceil$, $s = \lfloor \sqrt{\lambda_n} / \nu_n^2 \rfloor$, $s^2 \nu_n^4 \le \lambda_n$, $2^{n/s}$, $B = O_k((s \log s)^{k-1})$, and $n / s = O(n \nu_n^2 / \sqrt{\lambda_n}) = O(\rho(n))$ into "3n(2m)P + 1", "Ok (1)", "σ −1", "λn", "νn", "s2 νn4 ⩽ λn", "2n/s", and "nνn2 /√λn"; in the contiguous source passages below, all mathematical superscripts, subscripts, radicals, floors/ceilings, and displayed equations are restored to match rendered printed pages 43 and 44.)

• §6.3, counting one sparse formula and equation (6.4) (printed p. 43):

  At most $3n(2m)^P + 1 = \exp((\log n)^{O_k(1)})$ calls suffice, including one final count. Each call takes $2^{O_k(n(\log \log n)^2 / \sqrt{\log n})}$ bit operations. Since any fixed power of $\log n$ is $o(n(\log \log n)^2 / \sqrt{\log n})$, the total time, including construction and candidate comparisons, is
  $$(n + m)^{O_k(1)} 2^{O_k(n(\log \log n)^2 / \sqrt{\log n})}. \tag{6.4}$$

• §6.4, Lemma 6.3 node count and leaf occurrence bound (printed p. 43):

  The tree has
  $$\operatorname{poly}_k(n, \sigma^{-1}), 2^{\sigma n}$$
  nodes and depth $\operatorname{poly}_k(n, \sigma^{-1})$. In every leaf, each variable occurs at most $B$ times, where $B$ is an explicitly computed integer satisfying
  $$B = O_k\bigl((\sigma^{-1} \log(2/\sigma))^{k-1}\bigr).$$

• §6.4, Proposition 6.4 statement (printed p. 43):

  Proposition 6.4. For each fixed $k \ge 2$, the interpolation algorithm counts the satisfying assignments of a $k$-CNF on $n \ge 20$ declared variables with $m$ clauses in $(n + m)^{O_k(1)} 2^{O_k(\rho(n))}$ bit operations and $(n + m)^{O_k(1)}$ bits of space.

• §6.4, Proof of Proposition 6.4, discrete parameter schedule and integer-comparison floor (printed pp. 43–44):

  For $n \ge 20$, we next select the sparsification parameter. Define
  $$\lambda_n = \lceil \log_2 n \rceil, \qquad \nu_n = \lceil \log_2 \lambda_n \rceil, \qquad s = \left\lfloor \frac{\sqrt{\lambda_n}}{\nu_n^2} \right\rfloor.$$
  We compute $s$ by integer comparisons, taking the largest nonnegative integer satisfying $s^2 \nu_n^4 \le \lambda_n$. If $s < 2$, we use exhaustive search; $\sqrt{\lambda_n} / \nu_n^2$ tends to infinity, so there are only finitely many such sizes.

• §6.4, Proof of Proposition 6.4, leaf occurrence bound, tree exponent, and combined runtime (printed p. 44):

  Otherwise we apply Lemma 6.3 with $\sigma = 1/s$. The tree has at most $2^{n/s} \operatorname{poly}_k(n, s)$ nodes, and its leaves have occurrence bound
  $$B = O_k\bigl((s \log s)^{k-1}\bigr) = (\log n)^{O_k(1)}.$$
  Each leaf uses the original $n$ variables and has at most $Bn$ nonempty clauses. We count each leaf by the sparse-formula algorithm of Section 6.3, whose running time is given by (6.4). Leaves with no clauses or containing an empty clause are handled directly. The clause count in that application is the number of clauses in the leaf; $m$ in the final bound remains the input clause count.

  For $s \ge 2$, the floor in its definition gives
  $$\frac{n}{s} = O!\left(\frac{n \nu_n^2}{\sqrt{\lambda_n}}\right) = O(\rho(n)).$$
  Thus both the number of leaves and the time to count each leaf have exponent $O_k(\rho(n))$. Their polynomial factors, together with normalization and the work at the tree nodes, are bounded by $(n + m)^{O_k(1)}$. The total number of bit operations is therefore
  $$(n + m)^{O_k(1)} 2^{O_k(\rho(n))}.$$
  The finite exhaustive-search cases are absorbed in the constants.

Public claims and assumptions

1. Integer-comparison floor characterization and permanent $s_n \ge 2$ threshold on Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups (Cslib.Complexity.SubexponentialSAT.SparseCountingScale):
   • interpolationScale_zero and interpolationScale_pos (in Cslib.Complexity.SubexponentialSAT) establish $\rho(0) = 0$ and strict positivity of $\rho(n)$ for $1 \le n$; numGroups_of_lt_three, numGroups_le_sqrt, numGroups_le_clog, and numGroups_le_self record $s_n = 0$ for $n < 3$ and $s_n \le \sqrt{\lambda_n} \le \lambda_n \le n$ for $s_n$ given by Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups.
   • When $1 \le \nu_n = \lceil \log_2 \lambda_n \rceil$ ($3 \le n$), sq_mul_pow_four_le_clog, clog_lt_succ_sq_mul_pow_four, numGroups_floor_bounds, le_numGroups_iff, and numGroups_eq_iff prove the exact integer-comparison characterization $s_n^2 \nu_n^4 \le \lambda_n < (s_n + 1)^2 \nu_n^4$.
   • Because $\nu_n$ jumps at powers of $2$, $s_n$ is not globally monotone ($s_{2^{524288}} = 2$ while $s_{2^{524289}} = 1$); two_le_numGroups_of_clog_ge, two_le_numGroups_of_pow_lt, two_le_numGroups_of_pow_le, eventually_two_le_numGroups, and five_le_of_two_le_numGroups establish the sharp permanent threshold $2 \le s_n$ for all $\lambda_n \ge 640000$ ($n \ge 2^{640000}$), and tendsto_numGroups_atTop and finite_numGroups_lt prove $s_n \to \infty$ and finiteness of ${n \mid s_n < B}$.
2. Core §6.4 tree-exponent and polynomial leaf-factor bounds:
   • div_numGroups_le_two_mul proves $n / s_n \le 2 n \nu_n^2 / \sqrt{\lambda_n}$ whenever $1 \le s_n$.
   • div_numGroups_le_interpolationScale_of_clog_ge, eventually_div_numGroups_le, and isBigO_div_numGroups_interpolationScale prove $n / s_n \le 16 \cdot \rho(n)$ for all $\lambda_n \ge 640000$ and $(n \mapsto n / s_n) = O(\rho(n))$ against Cslib.Complexity.SubexponentialSAT.interpolationScale.
   • eventually_poly_mul_two_pow_div_numGroups_le and exists_eventually_poly_mul_two_pow_div_numGroups_le absorb any polynomial leaf factor $(n + s_n + 1)^d \cdot 2^{n / s_n}$ into $2^{17 \rho(n)}$ eventually.
3. Core §6.3 equation (6.4) polylogarithmic and quasi-polynomial query-overhead absorption:
   • isLittleO_log_pow_interpolationScale, isLittleO_clog_pow_interpolationScale, eventually_mul_log_pow_le_interpolationScale, and eventually_mul_clog_pow_le_interpolationScale prove $(\log(n + 16))^d = o(\rho(n))$ and $\lambda_n^d = o(\rho(n))$ for every $d : \mathbb{N}$.
   • eventually_two_pow_clog_pow_le, eventually_exp_clog_pow_le, eventually_query_overhead_le, and eventually_query_overhead_poly_le deduce that $2^{C \lambda_n^d}$, $\exp(C \lambda_n^d)$, and the Lemma 6.2 candidate-query count $3n(2m + 2)^P + 1$ (under $m \le B n$, $B \le C_B \lambda_n^\beta$, and either $P \le C_P \lceil \log_2(2m + 2) \rceil$ or polynomial $P \le C_P B^{e_B} \lceil \log_2(2m + 4) \rceil^{e_\mu}$ as in Lemma 6.1's $P = 20000 B^2 \mu^2$) are eventually bounded by $2^{\varepsilon \rho(n)}$ for every $\varepsilon > 0$.
4. Leaf occurrence polylogarithmic bound and uniform runtime composition (sparse_formula_time_bound on the sparse domain and prop64_time_bound across all $n, m : \mathbb{N}$):
   • leafOccurrenceBound defines $C_k (s (\lceil \log_2(2s) \rceil + 1))^{k-1}$; numGroups_mul_clog_le_clog, leafOccurrenceBound_le_mul_pow, leafOccurrenceBound_le_of_le, eventually_leafOccurrenceBound_le, exists_eventually_leafOccurrenceBound_le, and eventually_leafOccurrenceBound_feasible prove that at $s = s_n$, leafOccurrenceBound is bounded by $C_k \lambda_n^{k-1}$ for all $n \ge 5$ and eventually by $\lambda_n^k$ for $k \ge 1$, directly discharging Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible at $\beta = k$ via Cslib.Complexity.SubexponentialSAT.ReplacementParams.exists_feasible.
   • sparse_formula_time_bound combines the finite $n < N_0$ fallback, Lemma 6.1 initial-matrix construction $2^{C_{\mathrm{init}} \lambda_n^{d_{\mathrm{init}}}}$, and Lemma 6.2 candidate-query overhead into a uniform bound $C_{\mathrm{sparse}} (n + m + 1)^{d_{\mathrm{sparse}}} 2^{A_{\mathrm{sparse}} \rho(n)}$ ($0 < A_{\mathrm{sparse}}$) across the promised sparse domain $m \le C_B \lambda_n^\beta \cdot n$.
   • prop64_time_bound_general and prop64_time_bound combine the finite $n < N_0$ / $s_n < 2$ exhaustive-search fallback $C_{\mathrm{exhaust}} (n + m + 1)^{d_{\mathrm{exhaust}}} 2^n$, the sparsification-tree node/leaf factor $C_{\mathrm{tree}} (n + s_n + 1)^{d_{\mathrm{tree}}} 2^{\lfloor n / s_n \rfloor + 1}$, per-node overhead $(n + m + 1)^{d_{\mathrm{node}}}$ in the original clause count $m$, and per-leaf sparse-formula counting cost at bounded leaf clause count $m_{\mathrm{leaf}} \le B_n n$ into a single uniform bound $C_{\mathrm{total}} (n + m + 1)^{d_{\mathrm{total}}} 2^{A_{\mathrm{total}} \rho(n)}$ ($0 < A_{\mathrm{total}}$) valid for all $n, m : \mathbb{N}$.

Deviations / Non-claims

• Parameterized runtime-composition theorems rather than end-to-end Turing-machine assembly: Following the slice decomposition in Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226, this module formalizes the §6.3–6.4 asymptotic estimates and uniform runtime-composition bounds (sparse_formula_time_bound, prop64_time_bound_general, prop64_time_bound) over abstract cost functions time : ℕ → ℕ → ℝ satisfying the component bounds of Theorem 2.2 and Lemmas 6.1–6.3; wiring the concrete multi-tape Turing-machine implementations of disjoint sparsification, Tanner/greedy parity-row construction, and common-zero counting into top-level #k-SAT and k-SAT complexity bounds is handled in companion integration slices.

• Discrete logarithmic factor in leafOccurrenceBound: Lemma 6.3 states $B = O_k((\sigma^{-1} \log(2/\sigma))^{k-1})$ at $\sigma = 1/s$; leafOccurrenceBound writes this in exact integer arithmetic as $C_k (s (\lceil \log_2(2s) \rceil + 1))^{k-1}$, which upper-bounds any natural-logarithm discretization up to adjusting $C_k$ ($\log(2s) \le \lceil \log_2(2s) \rceil + 1$ for $s \ge 1$).

• Existing notions considered:

  • Cslib.Complexity.SubexponentialSAT.interpolationScale, Cslib.Complexity.SubexponentialSAT.interpolationScale_nonneg, Cslib.Complexity.SubexponentialSAT.isLittleO_interpolationScale, and Cslib.Complexity.SubexponentialSAT.eventually_mul_interpolationScale_le (Complexity/Computability/Complexity/FineGrained/CountingScale.lean): reused directly as the target sublinear exponent $\rho(n)$ and its nonnegativity without modifying CountingScale.lean.
  • Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups, Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups_eq_floor, Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible, and Cslib.Complexity.SubexponentialSAT.ReplacementParams.exists_feasible (Complexity/Computability/Complexity/FineGrained/ReplacementParams.lean): reused directly for Proposition 6.4's discrete sparsification parameter $s_n = \lfloor \sqrt{\lambda_n} / \nu_n^2 \rfloor$, alongside Nat.clog and Nat.sqrt (Mathlib.Data.Nat.Log, Batteries.Data.Nat.Lemmas) for $\lambda_n = \lceil \log_2 n \rceil$ and $\nu_n = \lceil \log_2 \lambda_n \rceil$, avoiding any parallel parameter-schedule definitions and leaving leafOccurrenceBound as the sole new public definition. ReplacementParams.lean proves real-floor agreement (Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups_eq_floor) and Lemma 4.8 feasibility (Cslib.Complexity.SubexponentialSAT.ReplacementParams.exists_feasible), whereas Proposition 6.4 additionally requires the integer-comparison characterization (numGroups_eq_iff), sharp permanent $2 \le s_n$ threshold (two_le_numGroups_of_clog_ge), divergence $s_n \to \infty$ (tendsto_numGroups_atTop), tree-exponent bound $n / s_n = O(\rho(n))$ (isBigO_div_numGroups_interpolationScale), polylogarithmic query absorption (eventually_query_overhead_poly_le), and leaf-occurrence bound leafOccurrenceBound.
  • Cslib.Logic.PL.ClauseSet.Sparsification.threshold, Cslib.Logic.PL.ClauseSet.Sparsification.card_le_of_sparse, and Cslib.Complexity.Sparsify.rounds (Complexity/Logics/Propositional/ClauseSet/Sparsification.lean, Complexity/Computability/Complexity/FineGrained/Sparsification.lean): formalize fixed-$\varepsilon$ decision sparsification ($\varepsilon = 1/M$ constant in $n$), whereas Lemma 6.3 and Proposition 6.4 require the $n$-dependent diverging denominator Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups ($s_n \to \infty$) and the explicit polylogarithmic variable-occurrence bound leafOccurrenceBound.
  • scripts/parallel_defs.py reports 0 candidate parallel definitions among the 1 examined declaration (leafOccurrenceBound).

Validation and review

• Tested at commit 909c43f5a124300921d6a3c31bcc997687c3ecd2 (fast-forward merge of origin/main ae4c29e7eaa6af4bea435317e232c7cf9bdf1783 and removal of duplicate Cslib.Complexity.SubexponentialSAT.interpolationScale_nonneg now provided by CountingScale.lean):
  • LEAN_NUM_THREADS=4 lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts, lake exe mk_all --check, lake exe lint-style, lake exe checkInitImports — passed (0 warnings).
  • python3 scripts/check_hygiene.py --check-simp — passed (All hygiene checks passed.).
  • python3 scripts/check_tidy_surface.py — passed (zero new public Tidy declarations).
  • python3 scripts/check_changed_files.py — passed.
  • python3 scripts/parallel_defs.py — passed (0 candidate parallel definitions).
  • python3 -B scripts/build_abstracts.py --check — passed.
  • python3 scripts/check_pr_names.py --strict — passed.
• Representative concrete checks in ComplexityTests/SparseCountingScale.lean: decide evaluations of Nat.clog, leafOccurrenceBound, and integer floor inequalities across $n \in {0, 1, 2, 3, 4, 5, 16, 20, 64, 1024}$; exact Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups values including the non-monotonicity witness ($s_{2^{524288}} = 2$ vs. $s_{2^{524289}} = 1$) and sharpness of the permanent threshold ($s_{2^{639999}} = 1$ vs. $s_{2^{640000}} = 2$); nonvacuous instantiation of isBigO_div_numGroups_interpolationScale, div_numGroups_le_interpolationScale_of_clog_ge, and eventually_poly_mul_two_pow_div_numGroups_le at $d = 3$; nonvacuous $k = 3$ chaining of eventually_leafOccurrenceBound_le ($\beta = 3$) and eventually_leafOccurrenceBound_feasible into Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible and both eventually_query_overhead_le and eventually_query_overhead_poly_le ($P \le 20000 B^2 \mu^2$); positive instantiation of sparse_formula_time_bound on a concrete piecewise sparse $3$-SAT runtime model over $m \le 8 \lceil \log_2 n \rceil^3 n$ exercising both the $n < 5$ fallback ($(n, m) = (4, 40)$) and the active Lemma 6.1 + Lemma 6.2 sparse branch ($P = 20000 B^2 \mu^2$ and initial-test term $2^{3 \lceil \log_2 n \rceil^2}$) at the threshold boundary $(n, m) = (5, 1080)$; and instantiation of prop64_time_bound on a concrete piecewise $3$-SAT runtime model exercising both $s_n < 2$ fallback regimes ($n = 4$ and $n = 20$) and the active $2 \le s_n$ tree+leaf branch ($n = 2^{640000}$).
• Review and verification history: initial commit 4ef1ab113e1d audited against [OpenAI2026ETH] printed pp. 43–44 and ReplacementParams.lean (#1267), removing parallel schedule definitions in 875e4ad5659a and rebasing onto 813b4140e739 at 0318c3c8a541ab3b8e3e220ad41fb31d212e9775; PR review at 0318c3c8a541 requested restricting sparse_formula_time_bound's premise and conclusion to the intended sparse input domain and adding a concrete positive instantiation, resolved in fast-forward commit 46736295f796d2ccf656243dace99b3ecdab7471 while preserving prop64_time_bound_general and prop64_time_bound untouched, followed by non-author mathematical verification and full 6-gate scripts/check.sh verification at 46736295f796d2ccf656243dace99b3ecdab7471, fast-forward merge refreshes with origin/main at c01548d82825, 390768947395, and 82e13cb27, and deduplication of Cslib.Complexity.SubexponentialSAT.interpolationScale_nonneg (after #1255 added it to CountingScale.lean) at 909c43f5a124300921d6a3c31bcc997687c3ecd2.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: Unaffected. None of the curated abstracts or headline entries in abstracts/catalogue.json reference SparseCountingScale, and this PR adds an intermediate §6.3–6.4 asymptotic building block toward Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 without modifying CountingScale.lean or any existing declaration. Verified via python3 -B scripts/build_abstracts.py --check.
• Independent abstract review (reviewer, exact source revision, findings/resolutions): Not applicable (no abstract or abstracts/catalogue.json entry changed).
• PDF artifact/run and source/PR-head revisions; rendered-page and declaration-link checks: Not applicable (no abstract .lean or .tex sources changed).

AI assistance

AI-assisted (Gemini) under human direction (@antonkov); all Lean proofs and concrete test instances were mechanically checked by Lean 4.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): CLAIMED independent source/math/API review at 0318c3c8a541ab3b8e3e220ad41fb31d212e9775. The reader finishing #1299 will inspect the new discrete threshold, asymptotic estimates and conditional runtime composition, reusing the existing interpolation-scale and replacement-parameter results. No duplicate library build or complete native algorithm claim.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): CHANGES REQUESTED at 0318c3c8a541ab3b8e3e220ad41fb31d212e9775. The sparse-runtime wrapper has an unsatisfiable premise (inline finding); restrict its premise and conclusion to the intended sparse-input domain and exercise a positive instance. The rest of the independent source/math/API review is clean: discrete schedule, threshold, absorption and general Proposition 6.4 composition, with the latter correctly separating original clause count from bounded leaf clause count. Pinned pp.43–44 quotations were checked. This covers abstract cost estimates, not end-to-end native counting.

[SamuelSchlesinger]

[P1] No time can satisfy this htime. Put n = N₀, cap = C_B * Nat.clog 2 N₀ ^ β, and m = cap * N₀ + 1. The fallback requires N₀ < N₀; the active branch requires m ≤ B * N₀ and B ≤ cap, implying cap * N₀ + 1 ≤ cap * N₀. Thus sparse_formula_time_bound is vacuous for every choice of its parameters. Quantify both premise and conclusion over the intended sparse domain (or an explicit bounded B), and add a concrete instantiation of this theorem. Preserve the distinction between original m and sparse leaf m_leaf in the separate general composition theorem; that theorem is not affected by this counterexample.

[antonkov]

Addressed the bounded review item from pullrequestreview-5662412286 (inline 4385236506) in fast-forward commit 46736295f796 (0318c3c8a541..46736295f796):

• Complexity/Computability/Complexity/FineGrained/SparseCountingScale.lean: restricted both htime and the conclusion of sparse_formula_time_bound to the intended sparse input domain m ≤ C_B * Nat.clog 2 n ^ β * n (updating its docstring and the two module-summary lines accordingly), while leaving prop64_time_bound_general, prop64_time_bound, leafOccurrenceBound, and all other declarations and proofs untouched.
• ComplexityTests/SparseCountingScale.lean: added a concrete positive instantiation of sparse_formula_time_bound on an explicit piecewise sparse $3$-SAT runtime over m ≤ 8 * Nat.clog 2 n ^ 3 * n, exercising both the n < 5 fallback ((n, m) = (4, 40)) and the active Lemma 6.1 + Lemma 6.2 sparse branch (P = 20000 * B ^ 2 * μ ^ 2 and initial-test term 2 ^ (3 * ⌈log₂ n⌉ ^ 2)) right at the threshold and sparse-domain boundary (n, m) = (5, 1080).
• Verification: merges cleanly with origin/main (2bb224076) and passes all 6 scripts/check.sh gates, check_hygiene.py --check-simp, and check_pr_names.py --strict --pr 1298 (61/61 names declared at 46736295f796).

[antonkov]

Pushed fast-forward merge commit c01548d82825 (46736295f796..c01548d82825, merging origin/main 2bb224076 with 0-byte payload diff across Complexity/ and ComplexityTests/) to resolve the adjacent-line Complexity.lean import conflict after #1300.

[antonkov]

Pushed zero-payload fast-forward merge commit 390768947395 (c01548d82825..390768947395, merging origin/main @ 7a46ddd90 and regenerating Complexity.lean) to resolve the adjacent Complexity.lean import conflict from #1304; SparseCountingScale.lean and ComplexityTests/SparseCountingScale.lean are byte-for-byte unchanged from 46736295f796 / c01548d82825.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): DOMAIN FIX SOURCE APPROVED; CI HOLD at 390768947395ff3afa9c4762bc37846f1fab9dee. The repair resolves 5662412286: both premise and conclusion now restrict sparse m, with an actual positive runtime instance; unrelated Proposition 6.4 mathematics and both owned blobs survive the main merges. Exact CI fails at SparseCountingScale.lean:110: interpolationScale_nonneg is already declared by imported CountingScale.lean:83. Its header/proof are identical. Remove the duplicate local block and reuse the lower declaration; then obtain new-head green CI. No enqueue approval or repeat build.

[antonkov]

Pushed fast-forward commit 909c43f5a124 (390768947395..909c43f5a124, merging origin/main @ ae4c29e7eaa6): removed the duplicate Cslib.Complexity.SubexponentialSAT.interpolationScale_nonneg declaration in SparseCountingScale.lean (now exported by merged #1255's CountingScale.lean on main). All other declarations — including ReplacementParams.numGroups_mul_clog_le_clog — and all tests in ComplexityTests/SparseCountingScale.lean are 100% unchanged; all 6 local scripts/check.sh gates and check_pr_names.py --strict --pr 1298 passed.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE FINAL APPROVED at 909c43f5a124300921d6a3c31bcc997687c3ecd2. The sole owned-library delta deletes the duplicate interpolationScale_nonneg block and reuses its identical imported declaration. Tests are byte-identical; actual main ae4c29e7 and the exact sorted import union are preserved. This carries the substantive domain-fix review. Exact new-head CI now passes all six gates and fresh PR audits. GitHub is recalculating current-main mergeability; queue readiness still requires a clean preflight. Ready for the next eligible shared packet; no repeat build or native-endpoint claim.