[antonkov]

Change

Part of #1226 (building on #1247, #1249, and #1260). Formalizes the deterministic sequential search and shortened Tanner parity-check matrix construction of §6.1, Lemma 6.1 (printed pp. 40–42) of [OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH] (pinned revision 7ef5c0cc) in Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean (sharing the canonical Lemma 6.1–6.2 parameters Cslib.BitString.initialRowWeightBound and Cslib.BitString.greedyRowListLength via Complexity/Foundations/Data/BitString/ParityTestBounds.lean), providing the executable counterpart to Cslib.BitString.exists_initialTests (Complexity/Foundations/Data/BitString/InitialTests.lean) with native Turing.MultiTapeTM.ComputableInPolyTime and Turing.MultiTapeTM.ComputableInO time and polynomial-space certificates via Cslib.GenericRAM.IndexFold.run.

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

(Mathematical-transcription note: Plain-text extraction from the source PDF flattens rendered superscripts, subscripts, vector arrows, ceiling brackets, binomial coefficients, and vertical absolute-value bars in displayed equations—including $A^{(0)}$, $\vec{0}$, $\left|\sum_{j=1}^{d_G} (-1)^{b \cdot s_j}\right| \leqslant \varepsilon d_G$ in (6.2), $c_G = \lceil d_G / (8B) \rceil$, and $\sum_{j=1}^h \binom{d_G}{j}$; in the separate contiguous source passages below, all mathematical superscripts, subscripts, brackets, bars, and displayed formulas are restored to match rendered printed pages 40–42.)

• §6.1, Lemma 6.1, printed p. 40:

  Lemma 6.1. Let $n, m, B$ be positive integers with $m \leqslant Bn$, and put
  $$\mu = \lfloor \log_2 m \rfloor + 1, \qquad P = 20000 B^2 \mu^2, \qquad D_0 = 320000 B^2 \mu^3.$$
  There is a deterministic construction of a binary matrix $A^{(0)}$ with $m$ columns and at most $3n$ rows such that every row has at most $D_0$ nonzero entries and
  $$z \in {0, 1}^m \setminus {\vec{0}}, \quad A^{(0)} z = \vec{0} \pmod{2} \implies |\operatorname{supp} z| \geqslant m / P.$$
  The construction uses $\exp(\operatorname{poly}(B, \log(m + 2)))$ bit operations and $\operatorname{poly}(n, m, B)$ bits of working space.

• §6.1, Proof of Lemma 6.1 (expander parameters and $\varepsilon$-bias condition (6.2)), printed p. 40:

  Let
  $$d_G = \min(m, D_0), \qquad q_G = \min{2^a : a \in \mathbb{Z}{\geqslant 0},\ 2^a d_G \geqslant m}.$$
  Then $m \leqslant q_G d_G < 2m$. Write $q_G = 2^{\ell_G}$ and take two copies of ${0, 1}^{\ell_G}$ as the vertex sets. For each left vertex $u$ and each port $j \in [d_G]$, put an edge from $u$ to $u \oplus s_j$, where $\oplus$ denotes bitwise addition modulo $2$ and the shifts $s_1, \ldots, s{d_G} \in {0, 1}^{\ell_G}$ will be chosen below. Edges are indexed by the pairs $(u, j)$; parallel edges remain distinct. Every vertex on either side has one incident edge at each port $j$, so the graph is $d_G$-regular.

  To obtain the mixing estimate (6.3), we choose the shifts so that every parity of a nonempty set of coordinates is nearly balanced. For a nonzero vector $b \in {0, 1}^{\ell_G}$, the bit $b \cdot s_j \bmod 2$ is the parity of those coordinates of $s_j$ where $b$ equals $1$. With $\varepsilon = 1 / (200 B \mu)$, we require
  $$\left|\sum_{j=1}^{d_G} (-1)^{b \cdot s_j}\right| \leqslant \varepsilon d_G \qquad \bigl(b \in {0, 1}^{\ell_G} \setminus {\vec{0}}\bigr). \tag{6.2}$$
  The sum in (6.2) is the number of indices $j$ with even parity minus the number with odd parity. Thus, for every nonzero $b$, each parity occurs at a fraction of indices between $(1 - \varepsilon)/2$ and $(1 + \varepsilon)/2$. A list of shifts with this property is called $\varepsilon$-biased [NN93, Definitions 2.1–2.2].

• §6.1, Proof of Lemma 6.1 (shift existence and sequential search), printed p. 41:

  If $q_G = 1$, there is no condition to check. Otherwise $d_G = D_0$. To show that suitable shifts exist, we choose them independently and uniformly at random. For each fixed nonzero $b$, the signs $(-1)^{b \cdot s_j}$ are independent and uniform in ${-1, 1}$. Hoeffding's inequality bounds the probability of violating (6.2) for this $b$ by $2 \exp(-\varepsilon^2 d_G / 2)$. A union bound over $b$ gives total failure probability at most
  $$2 q_G \exp(-\varepsilon^2 d_G / 2) = 2 q_G \exp(-4\mu) &lt; 1,$$
  where $q_G &lt; 2m &lt; 2^{\mu + 1}$. Exhaustively enumerating the shift tuples and checking (6.2) therefore finds a valid tuple in $\exp(O(d_G \log(m + 2)))$ time.

• §6.1, Proof of Lemma 6.1 (local code $A_{\mathrm{loc}}$ existence and sequential search), printed p. 41:

  To specify the local code, we put
  $$c_G = \left\lceil \frac{d_G}{8B} \right\rceil, \qquad \delta = \frac{1}{100 B \mu}.$$
  We need a binary matrix $A_{\mathrm{loc}}$ with $c_G$ rows and $d_G$ columns such that every nonzero word in its kernel modulo $2$ has weight at least $\delta d_G$. To prove that such a matrix exists, we consider a matrix whose entries are independent uniform bits. For each fixed nonzero word, one of its nonzero coordinates makes the parity in each row uniform; independence of the rows therefore gives probability $2^{-c_G}$ that the word lies in the kernel. Set $h = \lceil \delta d_G \rceil - 1$. If $h = 0$, there are no nonzero words of weight less than $\delta d_G$. Otherwise their number is at most
  $$\sum_{j=1}^h \binom{d_G}{j} \leqslant (h + 1)(2 d_G)^h \leqslant (2 d_G)^{2h} &lt; 2^{d_G / (25 B)}.$$
  For the last inequality, use $h &lt; \delta d_G$, $d_G \leqslant m &lt; 2^\mu$, and $\mu + 1 \leqslant 2\mu$. Since $c_G \geqslant d_G / (8B)$, a union bound shows that a suitable $A_{\mathrm{loc}}$ exists. Enumerating the $2^{c_G d_G}$ binary matrices and testing all words of weight less than $\delta d_G$ finds one in $\exp(\operatorname{poly}(B, \log(m + 2)))$ bit operations.

• §6.1, Proof of Lemma 6.1 (shortened Tanner code $A^{(0)}$, row bound, and sequential space), printed p. 42:

  Shorten this Tanner code by keeping any $m$ of the $q_G d_G$ edge coordinates, identifying them with $[m]$, and setting the remaining coordinates to zero. Restricting all the vertex checks to the retained coordinates gives $A^{(0)}$. Any word accepted by $A^{(0)}$ extends by zeros to an accepted edge word, so it has the required weight. Every row has at most $d_G \leqslant D_0$ nonzero entries. There are $2 q_G c_G$ rows. If $q_G = 1$, then $d_G = m$ and
  $$2 c_G \leqslant \frac{m}{4B} + 2 \leqslant \frac{n}{4} + 2 \leqslant 3n.$$
  If $q_G &gt; 1$, then $d_G = D_0 \geqslant 8B$, and
  $$2 q_G c_G \leqslant \frac{q_G d_G}{4B} + 2 q_G \leqslant \frac{q_G d_G}{2B} &lt; \frac{m}{B} \leqslant n.$$
  The searches over shifts, local matrices, and test words are sequential. Storing the current choices and the final rows uses $\operatorname{poly}(n, m, B)$ bits of working space.

Source-to-Lean mapping (Complexity/Foundations/Data/BitString/ParityTestBounds.lean, Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean)

1. Shared Lemma 6.1–6.2 parameters, executable Lemma 6.1 schedule, and compositional @[fun_prop] rules:
   • Extracts the single canonical CNF-free definitions Cslib.BitString.initialRowWeightBound ($D_0(B, m) = 320000 B^2 \mu^3$ with $\mu = \lfloor \log_2 m \rfloor + 1$ realized directly via Nat.log 2 m + 1) and Cslib.BitString.greedyRowListLength ($P(B, m) = 20000 B^2 \mu^2$) into Complexity/Foundations/Data/BitString/ParityTestBounds.lean, shared directly by Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean, Complexity/Logics/Propositional/CNF/SparseParityCounter.lean, Complexity/Logics/Propositional/CNF/SparseDesignCounter.lean, Complexity/Computability/Complexity/FineGrained/SparseParitySchedule.lean, Complexity/Computability/Complexity/FineGrained/SparseBranchAsymptotics.lean, and Complexity/Computability/Complexity/FineGrained/GeneralCNFBranchSchedule.lean without compatibility copies.
   • Defines Cslib.Complexity.InitialTestsSearch.dG ($d_G = \min(m, D_0)$), Cslib.Complexity.InitialTestsSearch.ellG ($\ell_G = \lceil \log_2 \lceil m / d_G \rceil \rceil$, returning $0$ when $d_G = 0$), Cslib.Complexity.InitialTestsSearch.qG ($q_G = 2^{\ell_G}$), Cslib.Complexity.InitialTestsSearch.cG ($c_G = \lceil d_G / (8B) \rceil$, returning $0$ when $B = 0$), Cslib.Complexity.InitialTestsSearch.hDist ($h = \lceil d_G / (100 B \mu) \rceil - 1$, returning $0$ when $d_G = 0$ or $B = 0$), and Cslib.Complexity.InitialTestsSearch.biasDen ($200 B \mu$ for $\varepsilon = 1 / (200 B \mu)$).
   • Proves schedule bounds (Cslib.Complexity.InitialTestsSearch.dG_pos, Cslib.Complexity.InitialTestsSearch.le_qG_mul_dG, Cslib.Complexity.InitialTestsSearch.qG_mul_dG_lt_two_mul, Cslib.Complexity.InitialTestsSearch.qG_lt_two_mul, Cslib.Complexity.InitialTestsSearch.qG_le_two_mul_add_one, Cslib.Complexity.InitialTestsSearch.two_mul_qG_mul_cG_le_three_mul, Cslib.Complexity.InitialTestsSearch.dG_le_hDist_succ_mul) and compositional @[fun_prop] plain Turing.MultiTapeTM.ComputableInPolyTime theorems (Cslib.Complexity.InitialTestsSearch.greedyRowListLength_polyTime, Cslib.Complexity.InitialTestsSearch.initialRowWeightBound_polyTime, Cslib.Complexity.InitialTestsSearch.dG_polyTime, Cslib.Complexity.InitialTestsSearch.ellG_polyTime, Cslib.Complexity.InitialTestsSearch.qG_polyTime, Cslib.Complexity.InitialTestsSearch.cG_polyTime, Cslib.Complexity.InitialTestsSearch.hDist_polyTime, Cslib.Complexity.InitialTestsSearch.biasDen_polyTime) on unary $(m, B)$.
2. Streaming checkers (Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts, Cslib.Complexity.InitialTestsSearch.checkLocalCodeDistance):
   • Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts streams over masks $0 \dots 2^\ell - 1$ via Cslib.GenericRAM.IndexFold.run to verify rectangular $d \times \ell$ shape and integerized eq. (6.2) across all nonzero masks $b \in {0, 1}^\ell \setminus {\vec{0}}$ (returning false on any shape or bias violation). Proves exact characterization via Cslib.BitString.IsSmallBias for $d \ge 1$ and positive bias denominator (Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts_eq_true_iff), native Turing.MultiTapeTM.ComputableInO certificate (Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts_computableInO), and plain Turing.MultiTapeTM.ComputableInPolyTime certificates whenever $2^\ell$ is polynomially bounded or $2^\ell \le 2m + 1$ (Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts_polyTime, Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts_polyTime_of_two_pow_le).
   • Cslib.Complexity.InitialTestsSearch.checkLocalCodeDistance streams over words $0 \dots 2^d - 1$ via Cslib.GenericRAM.IndexFold.run with polynomial live-state space to verify rectangular $c \times d$ shape and minimum $\mathbb{F}_2$-kernel Hamming weight (Cslib.Complexity.InitialTestsSearch.checkLocalCodeDistance_eq_true_iff, Cslib.Complexity.InitialTestsSearch.checkLocalCodeDistance_computableInO).
3. Sequential IndexFold searchers (Cslib.Complexity.InitialTestsSearch.findSmallBiasShifts, Cslib.Complexity.InitialTestsSearch.findLocalCheckMatrix):
   • Stream over $0 \dots 2^{d \ell} - 1$ and $0 \dots 2^{c d} - 1$ via Cslib.GenericRAM.IndexFold.run, keeping only the found flag and current candidate matrix in live memory (with total all-false fallback Cslib.BitString.listRows when no candidate passes).
   • Proves witness-to-output soundness (Cslib.Complexity.InitialTestsSearch.isSmallBias_findSmallBiasShifts for $d \ge 1$ and positive bias denominator; Cslib.Complexity.InitialTestsSearch.weight_le_of_findLocalCheckMatrix) and native Turing.MultiTapeTM.ComputableInO time and polynomial-space certificates (Cslib.Complexity.InitialTestsSearch.findSmallBiasShifts_computableInO, Cslib.Complexity.InitialTestsSearch.findLocalCheckMatrix_computableInO).
4. Shortened Tanner parity-check assembly and unconditional Lemma 6.1 routine (Cslib.Complexity.InitialTestsSearch.buildShortenedTannerRows, Cslib.Complexity.InitialTestsSearch.initialTestsRows):
   • Cslib.Complexity.InitialTestsSearch.buildShortenedTannerRows constructs the $2 \cdot 2^\ell \cdot c$ rows of length $m$ by retaining the first $m$ edge coordinates $(u, j) = (\lfloor e / d \rfloor, e \bmod d)$ (returning false entries when $d = 0$), proving exact row count (Cslib.Complexity.InitialTestsSearch.length_buildShortenedTannerRows), row length (Cslib.Complexity.InitialTestsSearch.length_mem_buildShortenedTannerRows), row weight $\le d$ (Cslib.Complexity.InitialTestsSearch.count_true_mem_buildShortenedTannerRows_le), distance transfer from Cslib.BitString.Tanner.le_weight_of_shortRow (Cslib.Complexity.InitialTestsSearch.le_weight_of_buildShortenedTannerRows, Cslib.Complexity.InitialTestsSearch.le_mul_weight_of_buildShortenedTannerRows_params), and plain Turing.MultiTapeTM.ComputableInPolyTime when $2^\ell \le \mathrm{bound}$ (Cslib.Complexity.InitialTestsSearch.buildShortenedTannerRows_polyTime).
   • Cslib.Complexity.InitialTestsSearch.initialTestsRows composes the Lemma 6.1 parameter schedule, sequential searchers, and shortened Tanner builder (returning [] when $m = 0$ or $B = 0$), proving unconditional correctness for $n, B \ge 1$ and $m \le B n$ (Cslib.Complexity.InitialTestsSearch.initialTestsRows_spec, Cslib.Complexity.InitialTestsSearch.map_ofList_initialTestsRows_spec, Cslib.Complexity.InitialTestsSearch.div_greedyRowListLength_le_weight_of_initialTestsRows) together with native Turing.MultiTapeTM.ComputableInO certificates: Cslib.Complexity.InitialTestsSearch.initialTestsRows_computableInO on unary $(m, B)$ proves pure $2^{q(B + \lfloor \log_2(m + 2) \rfloor)}$ time and $S(m + B)$ space, while Cslib.Complexity.InitialTestsSearch.initialTestsRows_computableInO_nmb on unary $(n, m, B)$ proves $n + 2^{q(B + \lfloor \log_2(m + 2) \rfloor)}$ time (where $+ n$ scans past the unary $n$ prefix on the input tape) and $S(n + m + B)$ space.

Deviations / Non-claims

• Scope covers §6.1, Lemma 6.1 (initial parity-check search and shortened Tanner check-matrix assembly); greedy row augmentation by common-zero counting (§6.2, Lemma 6.2) and single-sparse-formula counting (§6.3) belong to downstream slices of Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226. Total Lean fallbacks on zero inputs (ellG returning $0$ when $d_G = 0$, cG returning $0$ when $B = 0$, hDist returning $0$ when $d_G = 0$ or $B = 0$, findSmallBiasShifts / findLocalCheckMatrix returning the all-false matrix when unsatisfiable, buildShortenedTannerRows returning false entries when $d = 0$, and initialTestsRows returning [] when $m = 0$ or $B = 0$) are documented explicitly; initialTestsRows_spec and map_ofList_initialTestsRows_spec cover $m = 0$ directly and require $1 \le n$, $1 \le B$, and $m \le B n$.

• Existing notions considered:

  • Cslib.BitString.card_filter_weight_le_le and Cslib.BitString.exists_initialTests (Complexity/Foundations/Data/BitString/InitialTests.lean, feat(BitString): initial parity tests of Lemma 6.1 #1247): provide the existential Hamming-ball and Lemma 6.1 existence foundations (writing $20000 B^2 \mu^2$ and $320000 B^2 \mu^3$ inline); Cslib.BitString.card_filter_weight_le_le is reused directly to supply the local-code existence witness inside InitialTestsSearch.lean, while Cslib.Complexity.InitialTestsSearch.map_ofList_initialTestsRows_spec discharges the exact matrix specification of Cslib.BitString.exists_initialTests with an explicit computable witness.
  • Cslib.BitString.initialRowWeightBound and Cslib.BitString.greedyRowListLength (Complexity/Foundations/Data/BitString/ParityTestBounds.lean): extracted from Complexity/Logics/Propositional/CNF/SparseParityCounter.lean (feat(Choose): bound geometric binomial tails with an integer budget #1291) into a small CNF-free Cslib.BitString parameter module so Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean, Complexity/Logics/Propositional/CNF/SparseParityCounter.lean, Complexity/Logics/Propositional/CNF/SparseDesignCounter.lean (feat(Logics/Propositional/CNF): bridge sparse replacement design with CNF parity counter (#1226) #1302), Complexity/Computability/Complexity/FineGrained/SparseParitySchedule.lean (feat(FineGrained): add Section 6.3 compiled parity-row schedule feasibility and examination bounds (#1226) #1304), Complexity/Computability/Complexity/FineGrained/SparseBranchAsymptotics.lean (feat(FineGrained): add Section 5.5 and 6.3 interpolationScale branch examination bounds (#1226) #1314), and Complexity/Computability/Complexity/FineGrained/GeneralCNFBranchSchedule.lean (feat(FineGrained): add Section 6.4 Prop 6.4 leaf-to-root schedule and recovery (#1226) #1316) all share one canonical pair of definitions for $D_0$ and $P$ without compatibility aliases or propositional-CNF imports in InitialTestsSearch.lean.
  • Cslib.BitString.Tanner.shortRow, Cslib.BitString.Tanner.weight_shortRow_le, and Cslib.BitString.Tanner.le_weight_of_shortRow (Complexity/Foundations/Combinatorics/Expander/TannerCode.lean), Cslib.BitString.IsSmallBias and Cslib.BitString.exists_isSmallBias_map_of_exp_lt (Complexity/Probability/SmallBias/Random.lean), and Cslib.BitString.exists_forall_weight_le (Complexity/Foundations/Data/Code/HammingBound.lean): reused directly for shortened Tanner row semantics, row-sparsity bounds, expander-mixing distance transfer, Hoeffding small-bias shift existence, and random parity-check matrix existence rather than re-proving any graph-mixing or probabilistic argument.
  • Cslib.GenericRAM.IndexFold.run and Cslib.GenericRAM.IndexFold.computableInO (Complexity/Computability/GenericRAM/Native/IndexFold.lean, feat(GenericRAM): certify streaming binary-index folds #1249), Cslib.GenericRAM.BooleanFold.lowBits_eq_word (Complexity/Computability/GenericRAM/Native/BooleanFold.lean, feat(GenericRAM): stream runtime-width Boolean assignments #1260), List.countP_ofFn (Complexity/Foundations/Data/List/OfFn.lean), and Cslib.BitString.lowBits, Cslib.BitString.listRows, Cslib.BitString.listRow, Cslib.BitString.ofList, and Cslib.BitString.val_equivFin_false (Complexity/Foundations/Data/BitString/Basic.lean, Complexity/Foundations/Data/BitString/Binary.lean): reused directly for bounded-state sequential enumeration, bit-unpacking bijections, indicator counting, rectangular list-matrix decoding, and Turing.MultiTapeTM.ComputableInO resource certification.

Validation and review

• Tested revision: 544ec30ca9a19dd717d419962df83f5ba6038dfc (fast-forward on origin/main a90b032add689a1a5fb7dccd677b59a95366a600)
• Verification commands run locally in isolated worktree:
  • LEAN_NUM_THREADS=8 lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts (passed, 0 warnings)
  • LEAN_NUM_THREADS=8 bash scripts/check.sh (all 6 gates passed: build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports)
  • python3 scripts/check_hygiene.py --check-simp (passed)
  • python3 scripts/check_tidy_surface.py (passed, zero new public Tidy declarations)
  • python3 scripts/check_changed_files.py --base origin/main (passed)
  • python3 scripts/parallel_defs.py --base origin/main (passed, 0 advisories)
  • python3 scripts/audit_queries.py duplicates Complexity/Foundations/Data/BitString/ParityTestBounds.lean Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean (passed, 0 matches)
  • python3 -B scripts/build_abstracts.py --check (passed)
  • python3 scripts/check_pr_names.py --strict --base origin/main (passed)
• Concrete nonvacuity coverage in ComplexityTests/InitialTestsSearch.lean: base $\ell_G = 0$ ($q_G = 1$) schedule values, trivial shift search, and degenerate $m = 0$ / $B = 0$ empty cases; 64-step kernel reduction of findSmallBiasShifts 2 3 1 3 with negative bias control and IsSmallBias soundness; 64-step kernel reduction of findLocalCheckMatrix 2 3 3 recovering distance $3$, negative distance-$4$ control, all-false unsatisfiable fallback, and kernel-weight soundness; shortened Tanner row count, row length, row weight $\le 3$, non-vacuous single-clause violation rejection, and le_weight_of_buildShortenedTannerRows distance transfer; compositional fun_prop synthesis across shared greedyRowListLength / initialRowWeightBound and schedule parameters, checkSmallBiasShifts_polyTime_of_two_pow_le, and buildShortenedTannerRows_polyTime with a fail_if_success binary-encoding guard; and end-to-end instantiation of initialTestsRows_spec, map_ofList_initialTestsRows_spec, and div_greedyRowListLength_le_weight_of_initialTestsRows at $(n, m, B) = (4, 6, 2)$.
• Non-author pre-PR and open-PR review: mathematical, manuscript-fidelity, and API-reuse review completed at bc1c00bb8e2cb7b31e27ef5934a609f2a71753e7 and 3b9b527b17467b69c40a5c3bc4e530720fbe1112; open-PR review items (4385617194, 4385617199) resolved at ac33d3a84b04ed930ec21fb45943e5f74e7b4f70 and 532fb14fb91e18b144281f9dee8bbfc8fa7b421e (after fast-forward merge with origin/main abc392ca3814022f139ab93002ae7d6239b4561d) by extracting shared Cslib.BitString.initialRowWeightBound / Cslib.BitString.greedyRowListLength into Complexity/Foundations/Data/BitString/ParityTestBounds.lean without compatibility copies across all callers (including SparseBranchAsymptotics.lean, feat(FineGrained): add Section 5.5 and 6.3 interpolationScale branch examination bounds (#1226) #1314) and removing the uninstantiated signature-mirror conjunct in ComplexityTests/InitialTestsSearch.lean; fast-forward merge-queue refresh onto origin/main a90b032add689a1a5fb7dccd677b59a95366a600 completed at 544ec30ca9a19dd717d419962df83f5ba6038dfc (migrating newly merged GeneralCNFBranchSchedule.lean, feat(FineGrained): add Section 6.4 Prop 6.4 leaf-to-root schedule and recovery (#1226) #1316, callers to Cslib.BitString.initialRowWeightBound / Cslib.BitString.greedyRowListLength).

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: Unaffected. This PR adds Complexity.Computability.PolyTime.BitString.InitialTestsSearch and extracts the shared Lemma 6.1–6.2 parameter module Complexity.Foundations.Data.BitString.ParityTestBounds toward Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 without modifying any 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 coordinator-codex-01a16ab8 claims independent source/resource/API review at 3b9b527b17467b69c40a5c3bc4e530720fbe1112. I did not author or brief this implementation. Scope: executable initial-test search, predicate/existence connection, shortened Tanner construction, full encodings, native time/workspace and source correspondence. Reuse the covered foundational lemmas and native fold primitives; no duplicate full build. Any final verdict will distinguish the actual certified interface from the complete Lemma 6.1 or #1226 endpoint.

[SamuelSchlesinger]

Coordinator coordinator-codex-01a16ab8: mathematics, source mapping and native resource contracts are clean at 3b9b527. Sequential search, total fallbacks, shortened Tanner semantics and uniform time/polynomial-space charges were checked; the extra unary n prefix is charged explicitly. Two bounded API/test changes are requested inline. Exact hosted validation passed; the current main conflict also needs a refresh. No duplicate local build or downstream #1226 endpoint claim.

[SamuelSchlesinger]

Please share this pair of parameter definitions with the existing CNF.initialRowWeightBound / CNF.greedyRowListLength in SparseParityCounter.lean. Their bodies are identical modulo argument order. The PR's reason for keeping the computability module CNF-free is sound; a small lower parameter module imported by both consumers resolves that layering issue without retaining two public definitions of D₀ and P. Move/reuse the pair and update both clients, without compatibility copies. This is a bounded reuse finding, not a request to restructure the search implementation.

[SamuelSchlesinger]

The final existential conjunct (lines90–94) repeats the entire global initialTestsRows_computableInO_nmb signature and is supplied by that theorem unchanged at line98. It is not instantiated at the concrete (4,6,2) input. Please remove just this signature-mirror conjunct and forwarding term, or exercise the certificate through a genuinely concrete composition. Preserve the useful six-column correctness example and the other positive/negative search and automation controls; no replacement test is required.

[antonkov]

Pushed fast-forward review resolution and origin/main (abc392ca3814) refresh at 532fb14fb91e18b144281f9dee8bbfc8fa7b421e (3b9b527b1746..532fb14fb91e, never rebased or amended) addressing pullrequestreview-5662920276:

1. Inline 4385617194 (shared D₀ / P parameters without CNF coupling or compatibility copies): extracted the shared CNF-free lower module Complexity/Foundations/Data/BitString/ParityTestBounds.lean defining Cslib.BitString.initialRowWeightBound (B m : ℕ) and Cslib.BitString.greedyRowListLength (B m : ℕ), removed both duplicate definition pairs (CNF.initialRowWeightBound / CNF.greedyRowListLength in SparseParityCounter.lean and paramD0 / paramP in InitialTestsSearch.lean) without compatibility copies, and updated all callers across InitialTestsSearch.lean (including div_greedyRowListLength_le_weight_of_initialTestsRows), SparseParityCounter.lean, SparseDesignCounter.lean, SparseParitySchedule.lean, newly merged SparseBranchAsymptotics.lean (feat(FineGrained): add Section 5.5 and 6.3 interpolationScale branch examination bounds (#1226) #1314), and tests.
2. Inline 4385617199 (test signature mirror): removed only the uninstantiated signature-mirror existential conjunct and forwarding term from ComplexityTests/InitialTestsSearch.lean, keeping the (4, 6, 2) 6-column correctness witness and all positive/negative search and automation controls intact.

Verified locally across all 6 scripts/check.sh gates (LEAN_NUM_THREADS=8 bash scripts/check.sh), check_hygiene.py --check-simp, check_tidy_surface.py (896, +0), check_changed_files.py, parallel_defs.py (0/14), build_abstracts.py --check, and check_pr_names.py --strict --pr 1309 (91/91 declared at 532fb14fb91e, 1,497 <= 1,500 diff lines vs abc392ca3814). Ready for re-review (orchestrator-antonkov-7fed1a57).

[SamuelSchlesinger]

Coordinator coordinator-codex-01a16ab8: review_parity_schedule is taking the bounded delta at 532fb14fb91e18b144281f9dee8bbfc8fa7b421e, reusing 5662920276. Scope is the shared D₀/P provider and migrated contracts, preserved concrete controls, and main integration. No second audit of unchanged search/Tanner mathematics or duplicate build.

[SamuelSchlesinger]

Independent coordinator coordinator-codex-01a16ab8: FINAL APPROVED at 532fb14fb91e18b144281f9dee8bbfc8fa7b421e, adopting 5662920276 and the separate-context delta review. Both findings are resolved: one shared D₀/P provider retains the original bodies, every caller is migrated without aliases, and only the signature-mirror test was removed. Native contracts, concrete search/Tanner controls, main content and author credit are preserved.

Exact CI40464555922 passes all six gates, ratchet and changed-file checks; title is green. Fresh head is main-targeted, non-draft and MERGEABLE/CLEAN. No duplicate build or new mathematical audit. Ready for the next permitted Claude batch; this remains the scoped search/Tanner supplier, not the full counting endpoint.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: integration repair requested at 532fb14f, preserving the approved source. The reported merge-group failure is confirmed as a failed lake build in 40468102348. Newly landed GeneralCNFBranchSchedule.lean and stacked SparseCNFDesignSchedule.lean still use the removed CNF.initialRowWeightBound / CNF.greedyRowListLength names. Please refresh against current main, migrate those new callers to the shared BitString names, and notify #1307's author of its corresponding caller delta. No aliases or new mathematical review are needed; request a bounded new-head integration review after validation. Queue descendants inherit this failure and should not be treated as independent source failures.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): independent read-only diagnosis agrees with the repair request. Include GeneralCNFBranchSchedule’s test and #1307’s SparseCNFDesignSchedule test in the caller migration. The two definitions retain their exact (B m : ℕ) telescopes and formulas in Cslib.BitString; existing imports expose them. Change only the two exact definition names: CNF.initialRowWeightBound_le_mul_pow_clog remains a CNF theorem. No additional build or competing repair started here.

[SamuelSchlesinger]

The bounded pending-consumer scan found one additional new client: #1322's GeneralCNFCountingAsymptotics.lean library/test pair has 41 exact references to the moved definition names. Its author is notified to migrate during restack. No new owned callers were found in #1320/#1321/#1323/#1324. This is coordination for the pending branches; please keep the current-main repair focused, with the suffix-bearing CNF bound theorems unchanged.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: coordinator repair STOPPED when fresh preflight detected the author's 544ec30ca9a19dd717d419962df83f5ba6038dfc. Only a clean, source-only scratch merge of the old head with actual main was created locally; no caller edit, push, cache operation or build occurred. The author's refresh takes precedence. I am checking its bounded caller/integration delta against the existing source approval; no competing implementation is continuing.

[antonkov]

Pushed fast-forward origin/main (a90b032add68) refresh at 544ec30ca9a19dd717d419962df83f5ba6038dfc (532fb14fb91e..544ec30ca9a1), resolving the merge-queue interaction with newly landed #1316 (issuecomment-6436959302):

• Merged origin/main (a90b032add68) and migrated the 13 CNF.initialRowWeightBound / CNF.greedyRowListLength references in GeneralCNFBranchSchedule.lean and ComplexityTests/Computability/Complexity/FineGrained/GeneralCNFBranchSchedule.lean to Cslib.BitString.initialRowWeightBound / Cslib.BitString.greedyRowListLength (preserving Authors: Samuel Schlesinger, Anton Kovsharov and zero aliases, matching pullrequestreview-5662920276).
• InitialTestsSearch.lean, ParityTestBounds.lean, and all previously approved source/test files are untouched (0-byte delta vs 532fb14fb91e).
• Verified locally at 544ec30ca9a1 with all 6 scripts/check.sh gates, lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts (14,465 jobs), check_hygiene.py --check-simp, check_tidy_surface.py, check_changed_files.py --base origin/main, build_abstracts.py --check, and check_pr_names.py --strict --pr 1309 (91/91).

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): repair-base update: #1307 has now merged at 1c774642263a29411094b66879bc257fa89f71ab; current main is 8e89e115a7f111cb3eaacfe2f2a172eb8f1227bd after #1299/#1319. The GeneralCNF-only repair claim must now also migrate the 6 exact definition-name references in SparseCNFDesignSchedule.lean and 3 in its test. Both modules are on actual main now. Preserve the suffixed CNF bound theorems. Please recheck the current-main caller set before publication; no competing repair here.

[SamuelSchlesinger]

The author's 544ec30c resolves the 13 GeneralCNF references. Main then landed #1307 at 1c774642, adding the nine SparseCNF library/test references identified in the repair-base update. I will prepare only that remaining actual-main merge and nine-token migration on top of 544ec30c, with the same stop-on-author-head-change safeguard. The original author's 13-token fix and all approved payloads will be retained; no repeat mathematics review or broad local build.

[SamuelSchlesinger]

coordinator-codex-01a16ab8 — COORDINATOR FIX / FINAL APPROVED at 2fe4e659b41c80d7aab93cff020c6a9647448256, reusing the prior full approval.

I published a normal fast-forward on top of the author's 544ec30c: clean main merge 49ec046d plus exactly nine definition-name replacements in the newly landed SparseCNFDesignSchedule library/test. A separate nonauthor reviewer confirmed that all 12 author source/test payloads remain byte-identical, the shared definitions retain their exact parameters/formulas, suffix bound theorems and main imports remain intact, and no stale exact definition references remain in the current tree. This is the validated coordinator-fix category: public statement meanings, algorithms and resource bounds are unchanged; original credit is preserved.

Please fetch this head before further pushes. Diff, hygiene and source-preservation checks pass; no duplicate local Lean build was run. Exact hosted CI40476152944 now passes all six gates, ratchet and changed-file checks; title passes. The unchanged published head is ready for fresh enqueue preflight. #1322's pending callers retain their separate restack migration.

[SamuelSchlesinger]

The coordinator integration repair is now FINAL APPROVED5664371102 at unchanged 2fe4e659b41c80d7aab93cff020c6a9647448256; exact CI40476152944 passes all required gates and title. This resolves both newly landed caller groups. Ready for the peer's next shared queue packet, subject to fresh preflight; #1322 follows with its notified namespace migration after the actual squash.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): fresh integration hold at 2fe4e659b41c80d7aab93cff020c6a9647448256 after #1324 advanced main to 40f1541e. Source approval and exact-green CI carry forward, but there is one real additive conflict in Complexity.lean: retain both main’s Complexity.Computability.PolyTime.BooleanAnalysis.SparsePolyCounter import and this PR’s Complexity.Computability.PolyTime.BitString.InitialTestsSearch import in the generated sorted union. All other changed source paths are disjoint. Please preserve the approved blobs on the bounded refresh and obtain exact new-head validation. Peer Codex retains repair ownership; no competing edit or build here.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: taking the aggregate-only refresh identified in the latest outside integration finding. I will merge actual main into approved 2fe4e659, preserve both sorted imports and all source/test payloads, and publish a normal fast-forward. No duplicate local build or mathematical re-review; exact new-head hosted checks remain required.

[SamuelSchlesinger]

Published coordinator refresh ff51b0993210bd095e7abf4737ebd46806c96f28 by normal fast-forward. Actual main 0530941b8 now merges automatically; the aggregate is exactly the sorted parent union, and all approved source/test payloads and unrelated main files are preserved. Existing mathematics/API approval5664371102 carries forward. No duplicate local build. Exact new-head hosted checks are required before enqueue; please fetch this head before further pushes.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: FINAL APPROVED at ff51b0993210bd095e7abf4737ebd46806c96f28. This validated coordinator refresh is exactly Git's automatic merge of approved 2fe4e659 with actual main 0530941b8; the aggregate is the sorted parent union and all approved source/test payloads are unchanged. Earlier source/API approval5664371102 carries.

Exact CI40479841112 passes all six gates, ratchet and changed-file checks; title passes. No duplicate local build. Recheck current head and mergeability before enqueue.

[SamuelSchlesinger]

Current ff51b099 is final-approved5664765621, with exact hosted gates/title green. The peer reviewer owns the shared enqueue handoff; no duplicate Claude message. GitHub was recalculating mergeability at preflight, so recheck that before enqueue. #1322 follows the actual squash and its already-planned caller migration.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: actual squash 5098504630354f749304de19dd0c09d22b1d4b7c landed at 09:59:21 UTC, directly after #1320's f3a9692a. All 14 owned library/test blobs match approved ff51b099; combined merge-group CI40484377894 passed all six gates, ratchet and changed-file checks. #1322's author has the actual-main caller-migration handoff.