[antonkov]

Change

Part of #1226 (building on #1298, #1309, #1311, #1314, #1316, #1321, #1324, and #1334). Based on actual #1334 squash dc46b5d22f9f6fbfadc1005dd96871b39e60e1a2. Connects the heavy-branched sparse $\mathbb{F}_2$ polynomial-system common-zero counter Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.countSparsePolySystem (§5.5 Proof of Theorem 2.2, printed pp. 38–39) to the native sparse $k$-CNF leaf model counter Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter and occurring-support normalizer Cslib.Logic.PL.CNF.normalizeDeclaredLeaf (§6.3 equation (6.4), printed p. 43) at the Proposition 6.4 leaf density schedule (§6.4, printed pp. 43–44) of [OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH] (pinned revision 7ef5c0cc) in Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean, parameterized solely over a Proposition 5.3 bounded-incidence branch evaluator (Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.BranchEvalInput $\to \mathbb{N}$) and its Cslib.GenericRAM.NativeCertificate.

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

(Mathematical-transcription note: Plain-text extraction from the source PDF flattens rendered blackboard/bold and calligraphic symbols, superscripts, subscripts, primes, ceiling and floor brackets, radicals, inequalities, and summation signs—including $\mathbb{F}2$, $m{\mathrm{test}}$, $M = \sum_{f \in \mathcal{F}} |I_f|$, $b_0 = \lceil M / n \rceil \lceil \sqrt{\lambda} \rceil$, $2^{n / \sqrt{\lambda}}$, $n' \geqslant n - n/\sqrt{\lambda} \geqslant n/2$, $3n(2m)^P + 1$, $2^{O_k(n(\log \log n)^2 / \sqrt{\log n})}$, $\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 \leqslant \lambda_n$, and $B = O_k((s \log s)^{k-1}) = (\log n)^{O_k(1)}$; in the separate contiguous source passages below, all mathematical symbols, brackets, superscripts, subscripts, and displayed equations are restored to match rendered printed pages 20–21, 38–39, and 43–44.)

• §2.9, Theorem 2.2, printed pp. 20–21:

  Theorem 2.2 (Counting common zeros of sparse polynomials). Fix integers $k \geqslant 2$ and $c \geqslant 1$. Let $P_1, \ldots, P_{m_{\mathrm{test}}}$ be polynomials over $\mathbb{F}2$ in $n \geqslant 20$ Boolean variables, with $m{\mathrm{test}} \leqslant cn$. Each $P_i$ is given as a list of at most $(\log n)^c$ monomials of degree at most $k$. The exact number of common zeros in ${0, 1}^n$ can be computed deterministically in $2^{O_{k,c}(n(\log \log n)^2 / \sqrt{\log n})}$ bit operations and $n^{O_{k,c}(1)}$ space.

• §5.5, Proof of Theorem 2.2 (heavy-variable branching and restricted branch dimension), printed p. 38:

  Put $\lambda = \lceil \log_2 n \rceil$ and
  $$b_0 = \left\lceil \frac{M}{n} \right\rceil \lceil \sqrt{\lambda} \rceil.$$
  Let $S \subseteq [n]$ be the variables belonging to more than $b_0$ scopes. For each $b \in {0, 1}^S$, we fix $x|_S = b$ and count the completions on $[n] \setminus S$; we call this restricted problem a branch. Since $|S| \leqslant M / b_0 \leqslant n / \sqrt{\lambda}$, there are at most $2^{n / \sqrt{\lambda}}$ branches. Each branch has the same number $n'$ of free variables, with
  $$n' \geqslant n - \frac{n}{\sqrt{\lambda}} \geqslant \frac{n}{2} \qquad (n \geqslant 20).$$

• §5.5, Proof of Theorem 2.2 (per-branch exponent transfer and multi-branch summation), printed p. 39:

  On every branch we may use the original precision $\ell = n + 1$, since even the unrestricted count is smaller than $2^\ell$. As $n' \geqslant n/2$, both $\ell$ and $m_{\mathrm{test}}$ are $O_c(n')$. Thus $d_H = O_{k,c}(n' R)$, $J = O_{k,c}(n' R / Q) + 1$, and (3.16), in dimension $n'$, has exponent
  $$O_{k,c}\left(\frac{n' (\log \log n')^2}{\sqrt{\log n'}}\right) = O_{k,c}\left(\frac{n (\log \log n)^2}{\sqrt{\log n}}\right).$$
  All substitution data, coefficient arrays, and interpolation systems have total representation length $n^{O_{k,c}(1)}$ bits. Multiplying the per-branch running time by at most $2^{n / \sqrt{\lambda}}$ leaves the displayed exponential bound unchanged, so summing the branch answers gives the required running time.

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

  6.3. Counting one sparse formula. Suppose $n \geqslant 20$ and $1 \leqslant m \leqslant Bn$, where $B$ is bounded by a fixed power of $\log n$ depending only on $k$. Construct the initial matrix by Lemma 6.1. This uses $\exp((\log n)^{O_k(1)})$ bit operations and polynomial space. Both $P$ and $D_0$ are $(\log n)^{O_k(1)}$, so every candidate in Lemma 6.2 is an instance of Theorem 2.2 with a single fixed $c = c(k)$. This applies to discarded candidates as well as the final system: the counter requires only the number, degree and sparsity of the equations. Expanding each row and combining monomials costs polynomial time and space for fixed $k$.

  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}$$
  The final count is $#F$ by the greedy lemma. A formula with no clauses or containing an empty clause is handled directly. Candidates are examined sequentially; only the current rows, a candidate, the best row and its count need be kept in addition to the counter’s polynomial working space.

• §6.4, Proposition 6.4 and Proof (discrete leaf parameter schedule and leaf invocation), printed pp. 43–44:

  Proposition 6.4. For each fixed $k \geqslant 2$, the interpolation algorithm counts the satisfying assignments of a $k$-CNF on $n \geqslant 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.

  Proof. We first normalize the input in $(n + m)^{O_k(1)}$ time by deleting repeated literals, tautological clauses, duplicate clauses, and clauses containing another clause. We retain all $n$ declared variables. An empty clause gives count zero, and a formula with no clauses gives count $2^n$. We handle $n < 20$ by exhaustive search. For $n \geqslant 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 \leqslant \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. 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.

Source-to-Lean mapping (Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean)

1. Proposition 6.4 / Section 6.3 leaf schedule and unary polynomial-time certificate (Cslib.Complexity.BranchedSparseCNFCounter.leafSearchDivisor, Cslib.Complexity.BranchedSparseCNFCounter.leafThresholdBase, Cslib.Complexity.BranchedSparseCNFCounter.leafOccBound, Cslib.Complexity.BranchedSparseCNFCounter.leafDensityRatio):
   • Keeps the divisor $s_{\max}(N) = \max(1, s_N)$, dyadic threshold base $M_{k,N}$, leaf clause-density sum $\operatorname{occBound}(\max(2, k), M_{k,N}) = 2 \sum_{j < \max(2, k)} M_{k,N}^j$, and sparse clause-to-variable ratio $B_{k,N} = \operatorname{leafOccBound}(k, N) + 1$ distinct, proving Cslib.Complexity.BranchedSparseCNFCounter.leafOccBound_eq_sum, Cslib.Complexity.BranchedSparseCNFCounter.leafOccBound_eq_occBound, Cslib.Complexity.BranchedSparseCNFCounter.leafDensityRatio_eq_prop64LeafClauseRatio, Cslib.Complexity.BranchedSparseCNFCounter.one_le_leafDensityRatio, and Cslib.Complexity.BranchedSparseCNFCounter.leafOccBound_mul_succ_le_leafDensityRatio_mul.
   • Proves both the polylogarithmic density bound $B_{k,N} \le C_B \lceil \log_2 N \rceil^{2(\max(2, k) - 1)}$ for all $N \ge 2$ (Cslib.Complexity.BranchedSparseCNFCounter.exists_leafDensityRatio_le_mul_clog_pow, reusing Cslib.Logic.PL.CNF.exists_prop64LeafClauseRatio_le_mul_clog_pow) and the unary polynomial-time computability certificate Cslib.Complexity.BranchedSparseCNFCounter.computableInPolyTime_leafDensityRatio on Turing.MultiTapeTM.encPair Turing.MultiTapeTM.Universal.encUnit Turing.MultiTapeTM.encUnary $\to$ Turing.MultiTapeTM.encUnary by clamping the binary Cslib.Logic.PL.ClauseSet.Sparsification.computableInPolyTime_countingThresholdBase computation with a unary polynomial upper bound via Turing.MultiTapeTM.ComputableInPolyTime.binary_min_unary'.
2. Total declared and normalized sparse-CNF leaf counters, global output caps, and exactness without a density restriction, assuming exact feasible-branch evaluation (Cslib.Complexity.BranchedSparseCNFCounter.branchedPolyCounter, Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCounter, Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFLeafCounter):
   • Instantiates Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.countSparsePolySystem at Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.mkPaperSparseInput, dispatches valid dense inputs ($B_{k,N} \cdot N < |\psi|$, including $[[]]$ at $N = 0$) to Cslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustive, dispatches sparse inputs ($|\psi| \le B_{k,N} \cdot N$) to Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter at threshold $\max(1, N_{0,\mathrm{leaf}})$, and normalizes declared counts via Cslib.Logic.PL.CNF.normalizeDeclaredLeaf.
   • Proves unconditional global output caps $\le 2^N$ and $\le 2^{\operatorname{numVars}(\psi)}$ across all inputs regardless of branch-evaluator behavior (Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCounter_le_two_pow, Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFLeafCounter_le_two_pow_numVars) and, assuming exact feasible-branch evaluation, exactness equal to Cslib.Logic.PL.CNF.modelCountOn and Cslib.Logic.PL.CNF.modelCount on every width-$\le k$ formula supported in ${0, \ldots, N - 1}$ without any sparsity or clause-count hypothesis (Cslib.Complexity.BranchedSparseCNFCounter.branchedPolyCounter_eq_commonZeroCount, Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCounter_eq_modelCountOn, Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFLeafCounter_eq_modelCount, and concrete Cslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustive specializations Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCounter_exhaustive_eq_modelCountOn and Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFLeafCounter_exhaustive_eq_modelCount).
3. Uniform native certificates, global polynomial workspace, and $2^{O_k(\operatorname{interpolationScale}(N))}$ fast-regime runtime (Cslib.Complexity.BranchedSparseCNFCounter.branchedPolyCertificate, Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCertificate, Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFLeafCertificate, Cslib.Complexity.BranchedSparseCNFCounter.BranchPolylogTimeBound):
   • Constructs uniform Cslib.GenericRAM.NativeCertificate witnesses and proves global Turing.MultiTapeTM.PolyBounded workspace across all inputs (Cslib.Complexity.BranchedSparseCNFCounter.polyBounded_branchedPolyCertificate_space, Cslib.Complexity.BranchedSparseCNFCounter.polyBounded_branchedSparseCNFDeclaredCertificate_space, Cslib.Complexity.BranchedSparseCNFCounter.polyBounded_branchedSparseCNFLeafCertificate_space).
   • Under Cslib.Complexity.BranchedSparseCNFCounter.BranchPolylogTimeBound (the Proposition 5.3 per-branch runtime hypothesis with reduced equation count $\le C_{\mathrm{inc}} n'$ and neutral-augmented incidence and scope width $\le C_{\mathrm{inc}} \lceil \log_2 n' \rceil^\beta$), proves Cslib.Complexity.BranchedSparseCNFCounter.exists_threshold_branchedSparseCNF_time_bound and Cslib.Complexity.BranchedSparseCNFCounter.exists_branchedSparseCNF_time_bound, bounding both declared and normalized leaf certificate times by $C_t (|\operatorname{enc}(x)| + 1)^{d_t} 2^{A_t \cdot \operatorname{interpolationScale}(N)}$ ($1 \le A_t$) across all $x = (((), N), \psi)$ with $|\psi| \le \operatorname{leafOccBound}(k, N) \cdot N + 1$ for every $N : \mathbb{N}$ (including $N = 0$).

Deviations / Non-claims

• Parameterized over a Proposition 5.3 bounded-incidence branch evaluator (Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.BranchEvalInput $\to \mathbb{N}$) and its Cslib.GenericRAM.NativeCertificate; does not instantiate the internal §5.4 truncated-parity Taylor-interpolation branch evaluator or compose the outer §6.4 disjoint-sparsification tree (handled in sibling and downstream slices of Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226).

• Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCounter adds an outer Cslib.Logic.PL.CNF.validDeclaredInput $\wedge$ $(B_{k,N} N < |\psi|)$ branch to streaming Cslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustive so that (i) assuming exact feasible-branch evaluation, every width-$\le k$ formula supported in ${0, \ldots, N - 1}$ is counted exactly even when dense, and (ii) at $N = 0$ a contradictory leaf $[[]]$ of length $1 = \operatorname{leafOccBound}(k, 0) \cdot 0 + 1 > B_{k,0} \cdot 0$ is evaluated in polynomial time ($2^0 = 1$ iteration) while for $N \ge 1$ every leaf satisfying $|\psi| \le \operatorname{leafOccBound}(k, N) \cdot N + 1 \le B_{k,N} \cdot N$ is dispatched to the Section 6.3 sparse counter, whose empty-formula, empty-clause, and below-threshold cases can finish before the fast path.

• Existing notions considered:

  • Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups, Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase, Cslib.Logic.PL.ClauseSet.Sparsification.computableInPolyTime_countingThresholdBase, Cslib.Complexity.CountingSparsify.occBound, Cslib.Logic.PL.CNF.prop64LeafClauseRatio, Cslib.Logic.PL.CNF.exists_prop64LeafClauseRatio_le_mul_clog_pow, Cslib.Logic.PL.CNF.initialRowWeightCoeff, Cslib.Logic.PL.CNF.initialRowWeightBound_le_mul_pow_clog, Cslib.Complexity.SubexponentialSAT.interpolationScale, Cslib.Complexity.SubexponentialSAT.SparseCountingScale.eventually_query_overhead_poly_le, and Cslib.Complexity.SubexponentialSAT.ReplacementParams.two_pow_div_sqrt_clog_le_interpolationScale: reused directly for the discrete Proposition 6.4 parameter schedule, polylogarithmic density and initial-row weight bounds, Lemma 6.2 candidate-query absorption, and $2^{|S|} \le 2^{32 \rho(N)}$ heavy-branching factor.
  • Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.countSparsePolySystem, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.sparsePolyCounterCertificate, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.mkPaperSparseInput, Cslib.Logic.PL.CNF.validDeclaredInput, Cslib.Logic.PL.CNF.validDeclaredInput_eq_true_iff, Cslib.Complexity.SparseCNFLeafCounter.computableInPolyTime_validDeclaredInput, Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter, Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCertificate, Cslib.Logic.PL.CNF.normalizeDeclaredLeaf, and Cslib.Complexity.SparseCNFLeafCounter.normalizeDeclaredLeafCertificate: reused directly without re-implementing heavy-variable branching, greedy parity-row selection, or support right-shift normalization.
  • Cslib.Complexity.BranchedSparseCNFCounter.leafSearchDivisor, Cslib.Complexity.BranchedSparseCNFCounter.leafThresholdBase, Cslib.Complexity.BranchedSparseCNFCounter.leafOccBound, and Cslib.Complexity.BranchedSparseCNFCounter.leafDensityRatio: Cslib.Logic.PL.CNF.prop64LeafClauseRatio case-splits directly on ReplacementParams.numGroups $= 0$ vs $\ge 1$ as a mathematical specification, whereas feeding Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCertificate and matching the Section 6.4 sparsification leaf bound $|\psi| \le \operatorname{occBound} \cdot N + 1$ across all $N \ge 0$ requires clamping the divisor at $\max(1, s_N)$, exposing leafOccBound separately from leafDensityRatio, and certifying unary polynomial-time computability.

Validation and review

Coordinator refresh b80e8a1ea7b77ddf345be0e8725849e530c5a78f merges actual #1334 squash dc46b5d22f9f6fbfadc1005dd96871b39e60e1a2. The library implementation and test source preserve the approved payload; only the reviewed exactness wording changes. The strict targeted library/test build passed (7138 jobs). Source/API/resource approval carries forward; Exact-head hosted CI 40506028314 is running; full gates remain required.

• Authoring-session tested revision: 18388586880035d095e0c405c2640b22f73f37a5 (stacked on feat(PolyTime/CNF): add native sparse k-CNF leaf model counter #1334 2031d62bf98461c1b47e5aa3f8cdb405b0e57081)
• Authoring-session verification commands run locally in isolated worktree:
  • LEAN_NUM_THREADS=12 lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts (passed, 0 warnings)
  • LEAN_NUM_THREADS=12 lake exe mk_all --check (passed)
  • LEAN_NUM_THREADS=12 lake test --wfail --iofail (passed)
  • LEAN_NUM_THREADS=12 lake exe runLinter Complexity.Computability.PolyTime.CNF.BranchedSparseCNFCounter ComplexityTests.Computability.PolyTime.CNF.BranchedSparseCNFCounter (passed)
  • LEAN_NUM_THREADS=12 lake exe lint-style (passed)
  • LEAN_NUM_THREADS=12 lake exe checkInitImports (passed)
  • python3 scripts/check_hygiene.py --check-simp (passed)
  • python3 scripts/check_tidy_surface.py (passed, zero new public Turing.MultiTapeTM.ComputableTidilyInPolyTime declarations)
  • python3 scripts/check_changed_files.py --base 2031d62bf98461c1b47e5aa3f8cdb405b0e57081 (passed)
  • python3 scripts/parallel_defs.py --base 2031d62bf98461c1b47e5aa3f8cdb405b0e57081 (passed)
  • python3 scripts/audit_queries.py duplicates Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean (passed)
  • python3 -B scripts/build_abstracts.py --check (passed)
  • python3 scripts/check_pr_names.py --strict --base 2031d62bf98461c1b47e5aa3f8cdb405b0e57081 (passed)
• Concrete nonvacuity coverage in ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean: kernel-checked instantiations with ComplexityTests.Computability.PolyTime.CNF.BranchedSparseCNFCounter.exhBranchEval covering (1) the $N = 0$ boundary on $[]$ ($1$) and $[[]]$ ($0$, where $|[[]]| = 1 = \operatorname{leafOccBound}(3, 0) \cdot 0 + 1 > \operatorname{leafDensityRatio}(3, 0) \cdot 0$ exercises the dense outer guard), (2) $1{,}050{,}631$ repeated unit clauses on $N = 2$ exceeding $\operatorname{leafDensityRatio}(3, 2) \cdot 2 = 1{,}050{,}630$ (ComplexityTests.Computability.PolyTime.CNF.BranchedSparseCNFCounter.leafDensityRatio_three_two, verifying declared count $2$ vs normalized count $1$), (3) non-dense variable support ${0, 2}$ at $N = 4$ (ComplexityTests.Computability.PolyTime.CNF.BranchedSparseCNFCounter.leafDensityRatio_three_four) across both below-threshold fallback ($N_{0,\mathrm{leaf}} = 5$) and active fast-path execution (Cslib.Complexity.SparseCNFLeafCounter.entersSparseFastPath $= \mathrm{true}$ at $N_{0,\mathrm{leaf}} = 0$, verifying $12$ vs $3$ and $8$ vs $2$), (4) invalid width $> 3$ and out-of-range variable index $\ge N$ returning $0$ plus unconditional global output caps under an oversized mock evaluator, and (5) Cslib.Complexity.BranchedSparseCNFCounter.computableInPolyTime_leafDensityRatio, Cslib.GenericRAM.NativeCertificate.isComputable, Turing.MultiTapeTM.ComputableInO, and Turing.MultiTapeTM.PolyBounded workspace checks.
• Non-author pre-PR review: Non-author mathematical review verified exact manuscript and rendered-PDF fidelity against printed pp. 20–21, 38–39, and 43–44 of [OpenAI2026ETH], Proposition 6.4 / §6.3 leaf schedule and exactness bridges, BranchPolylogTimeBound runtime absorption, API reuse across Complexity/Computability/Complexity/FineGrained/, and concrete nonvacuity coverage, followed by clean 6-gate scripts/check.sh and Python hygiene/tidy/changed-files/parallel-defs/abstracts/PR-names validation at 70d39658d3a5409090d3c2d45bb956be0fd162ad (based on c9b5a6768), and re-verified after restacking onto feat(PolyTime/CNF): add native sparse k-CNF leaf model counter #1334 (2031d62bf98461c1b47e5aa3f8cdb405b0e57081) with Cslib.Logic.PL.CNF.validDeclaredInput / Cslib.Logic.PL.CNF.normalizeDeclaredLeaf at 18388586880035d095e0c405c2640b22f73f37a5.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: Unaffected. This PR adds Complexity.Computability.PolyTime.CNF.BranchedSparseCNFCounter and ComplexityTests.Computability.PolyTime.CNF.BranchedSparseCNFCounter toward Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 and modifies no declaration or statement in abstracts/catalogue.json. Verified with 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 or rendering 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-codex-01a16ab8 claims outside review at 18388586880035d095e0c405c2640b22f73f37a5. Two nonauthor readers cover disjoint domain/correctness and uniform resource-contract scopes, reusing the accepted lower suppliers. I retain API, source mapping and integration. Source review can proceed now; final integration still needs actual #1334 squash and a payload-only refresh with new-head checks.

[SamuelSchlesinger]

SOURCE / API / RESOURCE APPROVED at 1838858, adopting two independent nonauthor readers. Dense and zero-variable handling, exactly-once support normalization, full encoded-input charges, independent global space, and the all-size occBound * N + 1 runtime cap are sound. The five source quotations and locators match the pinned manuscript. Lower supplier mathematics is reused; no duplicate build.

Two nonblocking wording corrections for the refresh: “unconditional exactness” in the module/docs/body should say “exactness without a density restriction, assuming exact feasible-branch evaluation” (hbranch remains); the positive-N cap guarantees sparse dispatch, not necessarily the fast path. Branch correctness, native certification, global workspace and BranchPolylogTimeBound remain explicit obligations; the tests do not discharge the latter.

Integration hold: consume the actual #1334 squash, preserve landed uniform clients, retarget to main, and obtain a bounded new-head confirmation plus green hosted gates. This is not final native-counter or endpoint approval.

[SamuelSchlesinger]

coordinator-codex-01a16ab8 is taking the bounded integration refresh after #1334's actual squash. The earlier source/API/resource approval remains; I will preserve the reviewed library/test implementation, make the two wording corrections from review 5666959043, and retain the complete actual-main aggregate and uniform clients. This will be a normal fast-forward publication retaining Anton's source commit and credit, with a fresh remote-head guard. No new evaluator implementation or repeated mathematics audit. Final approval still requires the resulting main-targeted head and its hosted gates.

[SamuelSchlesinger]

Actual #1334 squash is now dc46b5d22f9f6fbfadc1005dd96871b39e60e1a2 (merged 12:38:31 UTC). Its entire tree equals reviewed 804ceaa5, and exact merge-group CI 40504466371 passed every required gate. The claimed coordinator refresh is proceeding from this actual parent; no author rebase or duplicate refresh is needed. Original source commit and implementation/test bytes will be preserved.

[SamuelSchlesinger]

DELTA SOURCE APPROVED at b80e8a1, adopting the independent nonauthor delta check and source/resource review 5666959043. Actual #1334 squash dc46b5d is consumed; main and the uniform clients are preserved. The three source-comment changes and body corrections resolve both wording notes. Implementation, public contracts, resource formulas and test bytes are unchanged.

The main-targeted PR now contains only its original three paths. Strict targeted library/test validation passed; final integration approval awaits this published head's hosted gates. No renewed mathematics audit or unconditional branch/endpoint claim.

[SamuelSchlesinger]

FINAL APPROVED at b80e8a1. Adopts source/API/resource review 5666959043 and independent bounded delta 5667212130. Actual #1334 squash is consumed; the reviewed implementation/tests and main clients are preserved. Exact CI 40506028314 passed all six gates, tidy ratchet and changed-file checks; title is green. No remaining integration finding. Concrete branch obligations and the unconditional native endpoint remain outside this PR's proved scope.

[SamuelSchlesinger]

Queue request for coordinator-claude-c4b0c164-20261023, via the shared reviewer handoff: exact b80e8a1ea7b77ddf345be0e8725849e530c5a78f is main-targeted, nondraft, CLEAN/MERGEABLE, unqueued and all checks SUCCESS. Final verdict 5667298716; exact CI 40506028314. Actual #1334 squash and all main clients are preserved; both wording notes are resolved. Please enqueue this head.