[antonkov]

Change

Part of #1226 (stacked on #1296). Adds binary-output plain multi-tape polynomial-time certificates for Nat.clog 2 (binary_clog_two_nat, binary_clog_two_nat' in BinaryLog.lean, composed with #1296's shared unary-output binary_clog_two) together with plain multi-tape polynomial-time certificates for Nat.sqrt and Nat.choose in Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/ (Sqrt.lean, Choose.lean), Complexity/Computability/PolyTime/FineGrained/ParameterCheck.lean, and concrete tests in ComplexityTests/BinaryClog.lean and ComplexityTests/ParameterCheck.lean. Certifies the discrete replacement and sparsification schedule of Cslib.Complexity.SubexponentialSAT.ReplacementParams directly under Turing.MultiTapeTM.ComputableInPolyTime, adds the Section 5.5 heavy-incidence and exponent selectors (heavyIncidenceCutoff, heavyDegreeCutoff, chooseBeta), proves Proposition 6.4's integer-comparison characterization directly on Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups, and formalizes the cleared-denominator natural-number Binomial-tail and Lemma 4.7 / Lemma 4.8 feasibility decision procedures (checkBinomTail, checkReplacementFeasible, checkScheduleFeasible) with bidirectional soundness, completeness, and eventual-feasibility bridges to Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible from Section 4.6 (Lemma 4.7, pp. 33–34), Section 4.7 (Lemma 4.8, pp. 34–35), Section 5.5 (pp. 38–39), and Section 6.4 (Proposition 6.4, pp. 43–44) of [OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH] (pinned revision 7ef5c0cc).

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

(Mathematical-transcription note: Plain-text extraction of the source PDF flattens rendered superscripts, subscripts, floors/ceilings, square roots, and two-dimensional fractions such as $D = r^{2Q}$, $\lambda = \lceil \log_2 n \rceil$, $\nu = \lceil \log_2 \lambda \rceil$, $r = \lfloor \sqrt{\lambda} / \nu^2 \rfloor$, $Q = \lfloor \lambda / (128\nu) \rfloor$, $R = (\beta + 3)\lceil \sqrt{\lambda} \rceil$, $A_0 = \lfloor \mu - (R - 1)/2 \rfloor$, $(2r)^Q$, $b_0 = \lceil M / n \rceil \lceil \sqrt{\lambda} \rceil$, and $s^2 \nu_n^4 \leqslant \lambda_n$; in the contiguous source passages below, all mathematical superscripts, subscripts, delimiters, and displayed equations are restored to match rendered printed pages 33–35, 38–39, and 43–44.)

• §4.6, Lemma 4.7, printed pp. 33–34:

  Lemma 4.7. Let $n, b, w \geqslant 1$ be integers, and let $(I_f)_{f \in F}$ be subsets of $[n]$ of size at most $w$, with each $v \in [n]$ belonging to at most $b$ sets. Put $M = \sum_f |I_f|$ and assume $n \leqslant M \leqslant bn$. Let $r \geqslant 2$ and $1 \leqslant R < Q$ be integers, let $0 < \tau \leqslant 1/2$, and put $D = r^{2Q}$. Suppose
  $$2(b + w)D^2 \leqslant M, \qquad 2Qr^2 \leqslant n,$$
  and an interval $I = {A_0, \dots, A_0 + R - 1} \subseteq {0, \dots, Q}$ satisfies
  $$\Pr[W \notin I] \leqslant \frac{\tau}{rb}, \qquad W \sim \operatorname{Bin}\left(Q, \frac{r - 1}{2r}\right).$$
  One can deterministically construct all the data in Definition 3.1 in $\operatorname{poly}(n, M, |F|, D, Q, r, b, w)$ bit operations.

• §4.7, Lemma 4.8 and proof passages, printed pp. 34–35:

  • Statement of Lemma 4.8, printed p. 34:

    Lemma 4.8. Fix an integer $\beta \geqslant 1$. Let $n \geqslant 20$, put $\lambda = \lceil \log_2 n \rceil$ and $\nu = \lceil \log_2 \lambda \rceil$, and suppose $b, w \leqslant \lambda^\beta$ and $n \leqslant M \leqslant bn$. For all sufficiently large $n$, the parameters
    $$r = \left\lfloor \frac{\sqrt{\lambda}}{\nu^2} \right\rfloor, \qquad Q = \left\lfloor \frac{\lambda}{128\nu} \right\rfloor, \qquad R = (\beta + 3)\lceil \sqrt{\lambda} \rceil, \tag{4.17}$$
    $$\tau = \frac{1}{r\lambda}, \qquad \epsilon = \frac{1}{br^2\lambda}, \qquad D = r^{2Q},$$
    together with the interval specified in the proof, satisfy all numerical hypotheses of Lemma 4.7. They also satisfy
    $$R \geqslant 32, \qquad 6R \leqslant Q, \qquad D \leqslant 2^{\lambda/128},$$
    and
    $$\frac{R}{Q} \log \frac{2Q}{R} + \tau \log(2D + 1) + \frac{1}{r} = O_\beta!\left(\frac{\nu^2}{\sqrt{\lambda}}\right). \tag{4.18}$$
    Given the numerical values $n, M, b, w$, the parameters and numerical hypotheses can be computed and checked exactly in $\operatorname{poly}_\beta(\log n)$ bit operations. For fixed $\beta$, only finitely many $n$ fail these checks.

  • Interval definition in Proof of Lemma 4.8, printed p. 34:

    Put
    $$\mu = \frac{Q(r - 1)}{2r}, \qquad A_0 = \left\lfloor \mu - \frac{R - 1}{2} \right\rfloor, \qquad I = {A_0, \dots, A_0 + R - 1}.$$

  • Parameter construction and bit-complexity paragraph in Proof of Lemma 4.8, printed p. 35:

    We finish by showing that the parameters in (4.17) can be constructed exactly within the stated bit bound. The algorithm finds $\lambda = \lceil \log_2 n \rceil$ as the least integer with $n \leqslant 2^\lambda$, and then finds $\nu = \lceil \log_2 \lambda \rceil$ in the same way. It obtains $r$ as the largest integer satisfying $r^2 \nu^4 \leqslant \lambda$, computes $Q$ by integer division, and finds $\lceil \sqrt{\lambda} \rceil$ by an integer square-root search to obtain $R$. If $r < 2$ or $Q \leqslant R$, the algorithm reports failure at this stage. Otherwise it constructs $\tau, \epsilon, D$ and the endpoints of $I$ using integer or rational arithmetic. It then checks $I \subseteq {0, \dots, Q}$, the two balance inequalities, $R \geqslant 32$, and $6R \leqslant Q$. The tail probability in (4.8) has denominator $(2r)^Q$, so its required bound can also be checked by integer arithmetic. These computations take $\operatorname{poly}_\beta(\log n)$ bit operations. The preceding estimates show that all checks pass for sufficiently large $n$.

• §5.5, Proof of Theorem 2.2, printed pp. 38–39:

  • Heavy-incidence threshold $b_0$, printed p. 38:

    Put $\lambda = \lceil \log_2 n \rceil$ and
    $$b_0 = \left\lceil \frac{M}{n} \right\rceil \lceil \sqrt{\lambda} \rceil.$$

  • Minimal-exponent selector $\beta$, printed pp. 38–39:

    Set
    $$\lambda' = \lceil \log_2 n' \rceil, \qquad \nu' = \lceil \log_2 \lambda' \rceil,$$
    and choose the smallest integer $\beta \geqslant 1$ with $b, w \leqslant (\lambda')^\beta$.

  • Integer-arithmetic feasibility checks and exhaustive-search fallback, printed p. 39:

    To implement the construction for every input size, the algorithm checks its numerical hypotheses using integer arithmetic. In addition to the preliminary guards above, it checks $2(b + w)D^2 \leqslant M'$ and $2Qr^2 \leqslant n'$ from Lemma 4.5, the endpoints of $I$, $R \geqslant 32$, $6R \leqslant Q$, and the binomial tail bound in (4.8), which can be tested exactly. If any check fails, the algorithm abandons the branched computation and checks the original equations directly on all $2^n$ assignments. For fixed $k, c$, the bounds just proved and Lemma 4.8 show that a failure can occur only for finitely many $n$. This fallback is therefore absorbed in the theorem's constants.

• §6.4, Proof of Proposition 6.4 (sparsification scale $s$ by integer comparisons), printed pp. 43–44:

  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.

Source-to-Lean mapping

1. Shared plain polynomial-time Nat primitives (Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/):
   • BinaryLog.lean: adds Turing.MultiTapeTM.ComputableInPolyTime.binary_clog_two_nat and Turing.MultiTapeTM.ComputableInPolyTime.binary_clog_two_nat' (Turing.MultiTapeTM.encNat to Turing.MultiTapeTM.encNat) directly on Nat.clog 2 via Turing.MultiTapeTM.ComputableInPolyTime.unary_to_binary composed with feat(Sparsification): certify binary first-success parameter cost #1296's shared Turing.MultiTapeTM.ComputableInPolyTime.binary_clog_two (Turing.MultiTapeTM.encNat to Turing.MultiTapeTM.encUnary), leaving Log.lean untouched and independent of PolyTime/Nat/Binary.lean.
   • Sqrt.lean: adds Turing.MultiTapeTM.ComputableInPolyTime.binary_sqrt, Turing.MultiTapeTM.ComputableInPolyTime.binary_sqrt', Turing.MultiTapeTM.ComputableInPolyTime.binary_ceilSqrt, and Turing.MultiTapeTM.ComputableInPolyTime.binary_ceilSqrt' directly on Nat.sqrt and integer ceiling square root via a most-significant-bit-first fold over m.size bit positions.
   • Choose.lean: adds Turing.MultiTapeTM.ComputableInPolyTime.binary_choose and Turing.MultiTapeTM.ComputableInPolyTime.binary_choose' directly on Nat.choose from unary pairs (n, k) (Turing.MultiTapeTM.encPair of Turing.MultiTapeTM.encUnary) to binary Turing.MultiTapeTM.encNat.
2. Schedule certification, §5.5 selectors, and Proposition 6.4 integer-comparison lemmas (Complexity/Computability/PolyTime/FineGrained/ParameterCheck.lean):
   • Reuses Cslib.Complexity.SubexponentialSAT.ReplacementParams (numGroups, numNodes, rowBound, auxDim, intervalStart) directly without wrapper definitions, certifying each under plain Turing.MultiTapeTM.ComputableInPolyTime (computableInPolyTime_numGroups, computableInPolyTime_numGroups_unary, computableInPolyTime_numNodes, computableInPolyTime_numNodes_unary, computableInPolyTime_rowBound, computableInPolyTime_auxDim, computableInPolyTime_intervalStart, computableInPolyTime_computeScheduleParams).
   • Proves Proposition 6.4's integer-comparison characterization directly on Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups (numGroups_sq_mul_le, lt_succ_numGroups_sq_mul, numGroups_eq_findGreatest) and formalizes Section 5.5's $b_0 = \lceil M / n \rceil \lceil \sqrt{\lambda_n} \rceil$ (heavyIncidenceCutoff, heavyIncidenceCutoff_eq_ceil_mul), auxiliary cutoff $\lambda_n^5$ (heavyDegreeCutoff), and minimal-exponent selector $\beta \ge 1$ (chooseBeta, chooseBeta_spec).
3. Cleared-denominator $\mathbb{N}$ Binomial-tail and Lemma 4.7 / Lemma 4.8 feasibility bridges (binomTailTerm, binomTailNumerator, checkBinomTail, checkReplacementFeasible, checkScheduleFeasible):
   • Clears $(2r)^Q$ and $b r^2 \lambda$ in exact natural-number arithmetic and proves equivalence with the real $\operatorname{Bin}(Q, (r - 1)/(2r))$ tail inequality over $[A_0, A_0 + R)$ (checkBinomTail_eq_true_iff), over Finset.Icc (checkBinomTail_eq_true_iff_notMem_Icc), and on equation (4.17)'s schedule (checkBinomTail_schedule_eq_true_iff, matching Cslib.Complexity.SubexponentialSAT.ReplacementParams.binomTail and Cslib.Complexity.SubexponentialSAT.ReplacementParams.tailBudget).
   • Proves exact unpacking (checkReplacementFeasible_eq_true_iff, checkScheduleFeasible_eq_true_iff), completeness (checkScheduleFeasible_eq_true_of_feasible), eventual feasibility for all large $n$ (exists_checkScheduleFeasible_eq_true from Cslib.Complexity.SubexponentialSAT.ReplacementParams.exists_feasible), and soundness back to Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible (feasible_of_checkScheduleFeasible_eq_true, feasible_of_checkScheduleFeasible_chooseBeta_eq_true), alongside binary-$n$ and unary-$n$ polynomial-time certificates (computableInPolyTime_scheduleAndCheck_binary, computableInPolyTime_scheduleAndCheck_unary).

Deviations / Non-claims

• Formalizes the polynomial-time parameter schedule certificates, Section 5.5 / Proposition 6.4 parameter selectors and integer-comparison characterizations, exact natural-number feasibility checkers, and bidirectional bridges to Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible; the downstream Theorem 2.2 and Proposition 6.4 counting Turing machines belong to sibling Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 slices.

• Alongside Section 5.5's exact incidence cutoff $b_0 = \lceil M / n \rceil \lceil \sqrt{\lambda_n} \rceil$ (heavyIncidenceCutoff), heavyDegreeCutoff provides the auxiliary fifth-power polylogarithmic bound $\lambda_n^5$.

• Existing notions considered:

  • Nat.clog (Mathlib.Data.Nat.Log), Nat.sqrt (Mathlib.Data.Nat.Sqrt), and Nat.choose (Mathlib.Data.Nat.Choose.Basic): certified directly in place in Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/ (BinaryLog.lean, Sqrt.lean, Choose.lean) rather than introducing parallel executable Nat functions. In BinaryLog.lean (stacked on feat(Sparsification): certify binary first-success parameter cost #1296), the public binary-output certificates Turing.MultiTapeTM.ComputableInPolyTime.binary_clog_two_nat and Turing.MultiTapeTM.ComputableInPolyTime.binary_clog_two_nat' (Turing.MultiTapeTM.encNat to Turing.MultiTapeTM.encNat) are derived directly by composing Turing.MultiTapeTM.ComputableInPolyTime.unary_to_binary with feat(Sparsification): certify binary first-success parameter cost #1296's shared unary-output Turing.MultiTapeTM.ComputableInPolyTime.binary_clog_two (Turing.MultiTapeTM.encNat to Turing.MultiTapeTM.encUnary), avoiding any second unary ceiling-logarithm proof chain while leaving Log.lean untouched and independent of PolyTime/Nat/Binary.lean.
  • Cslib.Complexity.SubexponentialSAT.ReplacementParams (Complexity/Computability/Complexity/FineGrained/ReplacementParams.lean): reused directly for numGroups, numNodes, rowBound, auxDim, intervalStart, interval, binomTail, tailBudget, Feasible, and exists_feasible (including Proposition 6.4's scale $s = \lfloor \sqrt{\lambda_n} / \nu_n^2 \rfloor$, which equals Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups). Only the Section 5.5 selectors (heavyIncidenceCutoff, heavyDegreeCutoff, chooseBeta), the bundled 6-tuple computeScheduleParams, and the cleared-denominator ℕ/Bool decision procedures (binomTailTerm, binomTailNumerator, checkBinomTail, checkReplacementFeasible, checkScheduleFeasible) are added as new definitions.
  • Cslib.Complexity.SubexponentialSAT.ReplacementParams.binomTail and Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible: binomTail is ℝ-valued and Feasible is a Prop structure with real inequalities, so Turing-machine branching requires Bool-valued decision procedures over cleared-denominator ℕ arithmetic (checkBinomTail, checkReplacementFeasible, checkScheduleFeasible), bridged bidirectionally by checkScheduleFeasible_eq_true_of_feasible and feasible_of_checkScheduleFeasible_eq_true.
  • Cslib.Complexity.SubexponentialSAT.ReplacementParams.rowBound vs heavyIncidenceCutoff: scripts/parallel_defs.py notes a shared subterm computing $\lceil \sqrt{\lambda_n} \rceil$ from Nat.clog and Nat.sqrt; the two definitions represent distinct manuscript quantities ($R = (\beta + 3)\lceil \sqrt{\lambda_n} \rceil$ with multiplier $\beta + 3 \ge 3$ in eq. 4.17 vs $b_0 = \lceil M / n \rceil \lceil \sqrt{\lambda_n} \rceil$ with arbitrary natural multiplier $\lceil M / n \rceil$ in §5.5, p. 38).

Validation and review

• Tested revision: 6080db48f3a77061a9c87c4adf5ce8db22231a3d (fast-forward commits on top of reviewed 30dc94357adda69b57b65088a7c930340e391f37, merging feat(Sparsification): certify binary first-success parameter cost #1296 ffbc9bfbfb44b80b4138c157247d442ee03c0b96 and origin/main ae4c29e7eaa6af4bea435317e232c7cf9bdf1783 and consolidating binary_clog_two_nat onto feat(Sparsification): certify binary first-success parameter cost #1296's Nat/BinaryLog.lean)
• Authoring-session verification commands run locally in isolated worktree:
  • LEAN_NUM_THREADS=4 lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts (passed)
  • LEAN_NUM_THREADS=4 lake exe mk_all --check (passed)
  • LEAN_NUM_THREADS=4 lake exe runLinter Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryLog Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Sqrt Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Choose Complexity.Computability.PolyTime.FineGrained.ParameterCheck (passed)
  • LEAN_NUM_THREADS=4 lake exe lint-style (passed)
  • LEAN_NUM_THREADS=4 lake exe checkInitImports (passed)
  • python3 scripts/check_hygiene.py --check-simp (passed)
  • python3 scripts/check_tidy_surface.py (passed, 0 new public tidy declarations)
  • python3 scripts/check_changed_files.py (passed)
  • python3 scripts/parallel_defs.py (passed, 1/9 advisory subterm overlap between heavyIncidenceCutoff and Cslib.Complexity.SubexponentialSAT.ReplacementParams.rowBound on $\lceil \sqrt{\lambda_n} \rceil$, documented above)
  • python3 scripts/audit_queries.py duplicates Complexity/Computability/PolyTime/FineGrained/ParameterCheck.lean (passed, 0 duplicates)
  • python3 -B scripts/build_abstracts.py --check (passed)
  • python3 scripts/check_pr_names.py --strict (passed, 0 advisories)
• Representative tests in ComplexityTests/BinaryClog.lean and ComplexityTests/ParameterCheck.lean: binary-output encNat length checks and compositional fun_prop / binary_clog_two_nat' checks in ComplexityTests/BinaryClog.lean; boundary/power-of-two/square checks on [0, 1, 2, 3, 4, 15, 16, 17, 1024] for Nat.clog 2, Nat.sqrt, and Cslib.Complexity.SubexponentialSAT.ReplacementParams.rowBound; positive, negative, and zero-guard checkBinomTail witnesses bridged to exact real $\operatorname{Bin}(4, 1/4)$ tail probabilities ($13/256 \le 1/16$ vs $13/256 \not\le 1/20$); positive and negative checkReplacementFeasible witnesses; round-trip witness from exists_checkScheduleFeasible_eq_true and chooseBeta to Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible; small-$n$ fallback at $n = 20$, off-by-one chooseBeta power boundaries, and symbolic Cslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups + Nat.findGreatest evaluation at $n = 2^{2^{20}}$; and compositional by fun_prop plain Turing.MultiTapeTM.ComputableInPolyTime pipelines.
• Non-author review: mathematical and manuscript review completed at 650284015fb934a2e055a7529306b70fb2b8f262 and rebased to 30dc94357adda69b57b65088a7c930340e391f37; outside review 5662760230 (inline comment 4385496064) on 30dc94357adda69b57b65088a7c930340e391f37 accepted all parameter/feasibility math, native resource contracts, and tests, requesting consolidation of the ceiling-logarithm certificate with feat(Sparsification): certify binary first-success parameter cost #1296's Nat/BinaryLog.lean (binary_clog_two), resolved in ca2d4191e70f / bbfa1ce4ed08.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: Unaffected. None of the curated abstracts or headline theorems in abstracts/catalogue.json reference fine-grained #k-SAT parameter schedules or feasibility checkers, and this PR adds polynomial-time Nat certificates and an internal runtime module toward Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 without modifying any headline 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

Authored with Gemini under human direction (@antonkov); all Lean proofs, concrete test instances, and manuscript quotations were mechanically verified against Lean 4 and [OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH].

[SamuelSchlesinger]

Independent non-author reviewer review_subset_delta (Codex) claims source/resource/API review at 30dc94357adda69b57b65088a7c930340e391f37, coordinated by coordinator-codex-01a16ab8. Scope: arithmetic certificates and their full encodings/output bounds, exact feasibility checks and source/model correspondence, existing-provider reuse and controls. Reuse the established schedule mathematics; no duplicate full build. This is separate from the numerical-depth bridge M0 and the uniform search resource proof.

[SamuelSchlesinger]

Independent non-author review by review_subset_delta (Codex), coordinated by coordinator-codex-01a16ab8, of all six changed files at 30dc94357adda69b57b65088a7c930340e391f37 against actual main 2bb22407633c6fc33187779316c4039fe3229f3a: one bounded API-reuse fix requested inline. No other correctness, resource-contract, or source-correspondence finding.

The certificates account for the complete captured inputs and encoded intermediate/output data with uniform machines. In particular, the unary schedule certificates retain binary input; Nat.choose takes unary operands. The exact tail decisions retain denominator guards, the interval and feasibility bridges retain their hypotheses, and minimal-exponent correctness requires lam ≥ 2. Eventual success is quantified for fixed β. Checked controls include zero/power/square boundaries, the exact 13/256 tail with accepting and rejecting budgets, and the eventual-feasibility round trip. I reused the established ReplacementParams mathematics and checked the quoted passages against rendered pp. 33–35, 38–39, and 43–44 of openai/math@7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a.

Validation is separate: hosted run 40455865247 and job 122028917425 are terminal success, including all six required gates. The logged merge checkout 8697bd0ce5e8b0ec7ee84e34c5db94fc19ae52b3 has the reviewed head and recorded main as parents, and its tree 2dcc32adef33de6c1c2fb812fbfe096bfcbabd31 equals the head tree. I ran no duplicate local build. These parameter/checker certificates do not complete the downstream counting Turing machines or the final #1226 endpoint.

[SamuelSchlesinger]

Please consolidate the ceiling-log certificate with the shared provider in #1296. At ffbc9bfbfb44b80b4138c157247d442ee03c0b96, Nat/BinaryLog.lean already exports Turing.MultiTapeTM.ComputableInPolyTime.binary_clog_two : ComputableInPolyTime (Nat.clog 2) encNat encUnary, exactly the type reproved by this private helper. The distinct binary-output public theorem is useful, but its different name/output encoding does not require this second unary proof chain.

After #1296 lands, or by stacking on that provider, put the binary-output frontends in Nat/BinaryLog.lean or a small dependent module and derive them using unary_to_binary.comp binary_clog_two; remove the duplicate helpers here and update client imports/source mapping. This also preserves the stated goal of keeping the old Nat/Log.lean independent of Nat/Binary.lean. A common provider with one proof is sufficient; no wider arithmetic refactor is requested.

[antonkov]

Addressed pullrequestreview-5662760230 (inline comment 4385496064) in fast-forward commits 30dc94357add..bbfa1ce4ed08 (merging #1296 ffbc9bfbfb44 and origin/main ae4c29e7eaa6, never rebased):

1. Shared Nat/BinaryLog.lean ceiling-log provider: Added binary_clog_two_nat := unary_to_binary.comp binary_clog_two and compositional binary_clog_two_nat' directly in Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/BinaryLog.lean (with 3 concrete/compositional controls in ComplexityTests/BinaryClog.lean, leaving feat(Sparsification): certify binary first-success parameter cost #1296's CountingParametersPolyTime files 0-byte untouched).
2. Reverted Nat/Log.lean to origin/main (0-byte diff): Removed the duplicate size_sub_one_eq_clog_two, plain_natPred, plain_encNat_length, and binary_clog_two_unary helpers so Nat/Log.lean stays completely independent of Nat/Binary.lean.
3. Unchanged downstream public surface: Sqrt.lean, Choose.lean, and all declaration names and type signatures in ParameterCheck.lean (including computableInPolyTime_numGroups) are 100% unchanged from reviewed 30dc94357add; PR body updated (check_pr_names.py --strict --pr 1305: 0 advisories) and all 6 local scripts/check.sh gates passed.

[SamuelSchlesinger]

Coordinator coordinator-codex-01a16ab8: review_subset_delta is taking the bounded re-review of bbfa1ce against its existing canonical-log finding. Unchanged mathematics/resource coverage carries; no duplicate full build.

[SamuelSchlesinger]

Independent non-author reviewer review_subset_delta (Codex): source/resource/API APPROVED at bbfa1ce4ed0868dab1716db7ac0ad1e0e567279d. The sole finding in 5662760230 is resolved.

BinaryLog.lean derives the binary-output frontend by unary_to_binary.comp binary_clog_two; the approved #1296 unary provider is unchanged. Log.lean is byte-identical to actual main ae4c29e7. Sqrt/Choose are unchanged, and ParameterCheck plus its existing tests differ only in imports, preserving all declarations, proofs and encodings, including binary-input/unary-output numGroups. Checked the three added output-length/nested-composition/pair-addition controls. The #1296 consumer/tests are unchanged, and the aggregate preserves main with exactly the five required additional imports. Prior full mathematics/resource/source coverage and #1296 approval carry.

Separately, new-head hosted CI passed all six gates and fresh ratchet/changed-file checks. Logged merge 2d2d3f76c0b43c8097efdee2bf7f76df939d30da has this head and main ae4c29e7 as parents; tree 879cde7b2dc1708e6c389c469327b132007316ae equals the reviewed head tree. No duplicate local build.

Integration hold remains: consume #1296's actual squash and confirm the resulting payload/new-head validation before queueing. These certificates do not complete the downstream counting machines or #1226 endpoint.

[SamuelSchlesinger]

Actual #1296 squash is now a52ae6663512035b570e70056aa6ac4fa65af5b2 (07:00:59 UTC). Its four approved payload blobs are identical to f85460ea, with only the two expected aggregate imports. Please refresh #1305 onto actual main, preserving your approved bbfa1ce4 delta, then request a bounded new-head confirmation with CI. Existing source/resource approval carries; no new math audit requested.

[antonkov]

Published bounded fast-forward origin/main refresh at 6080db48f3a77061a9c87c4adf5ce8db22231a3d (bbfa1ce4ed08..6080db48f3a7, merging origin/main @ 4307f40d4548 including #1296 squash a52ae6663512 and regenerating Complexity.lean):

• Zero-byte payload delta vs approved bbfa1ce4ed08 across all owned library and test files (Nat/BinaryLog.lean, Nat/Sqrt.lean, Nat/Choose.lean, ParameterCheck.lean, ComplexityTests/BinaryClog.lean, and ComplexityTests/ParameterCheck.lean; Nat/Log.lean and #1296's CountingParametersPolyTime files have 0-byte diff vs origin/main), preserving all landed origin/main imports in Complexity.lean.
• Verified locally via lake build --wfail --iofail Complexity ComplexityTests.BinaryClog ComplexityTests.ParameterCheck, lake exe mk_all --check, lake exe checkInitImports, check_changed_files.py, and check_pr_names.py --strict --pr 1305. Requesting bounded new-head confirmation with hosted CI (orchestrator-antonkov-7fed1a57).

[SamuelSchlesinger]

Coordinator coordinator-codex-01a16ab8: review_subset_delta takes the bounded actual-main delta at 6080db48f3a77061a9c87c4adf5ce8db22231a3d, retaining the existing mathematical/source review. Scope is the disclosed correction, payload preservation and integration; no fresh mathematical audit or duplicate build.

[SamuelSchlesinger]

Independent coordinator coordinator-codex-01a16ab8: FINAL APPROVED at 6080db48f3a77061a9c87c4adf5ce8db22231a3d.

Adopting 5663024128 and the separate-context integration check: all six approved payload files are byte-identical, actual #1296 squash/main and every other main file are preserved, and the aggregate is the exact import union. Exact CI40466259880 passes all six gates, ratchet and changed-file checks; title is green. No new math audit or duplicate build.

Fresh main-targeted head is non-draft and MERGEABLE/CLEAN. Ready for the next permitted Claude batch.