[antonkov]

Change

Part of #1226 (building on #1239, #1242, and #1266). Formalizes the executable mixed-radix auxiliary-label encoding, cleared common denominator $d_{\mathrm{den}} = (R - 1)!Q!$, ${0, 1, -1}$ block measurement matrix $C^B$, 1D swap-orbit dynamic program for $(R - 1)!M_0$ and cleared replacement polynomial rows $d_{\mathrm{den}}\vec{P}_u(T)$, Lemma 4.6 coefficient magnitude and bit-length bounds, and plain multi-tape Turing.MultiTapeTM.ComputableInPolyTime certificates from §§4.1–4.3 and §4.6 (Lemmas 4.1, 4.3, 4.6, and 4.7, printed pp. 27–29, 33–34) of [OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH] (pinned revision 7ef5c0cc), bridged to the Fin-indexed specification in Complexity/Foundations/LinearAlgebra/ExchangeReplacement.lean, in Complexity/Computability/PolyTime/LinearAlgebra/ExchangeReplacement.lean.

Source statements ([OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH], printed pp. 27–29, 33–34)

(Mathematical-transcription note: Plain-text extraction from the source PDF flattens rendered superscripts, subscripts, vector arrows, set-membership negations, and displayed equations such as $B = ([r]^Q)^2$, $D = |B| = r^{2Q}$, $C^B \in {0, 1, -1}^{[c_B] \times B}$, $\varphi_{u,y}(T)$, $\vec{P}u(T)$, $C{t,g}^B$, $S_{t,g}^B$, $\widetilde{\xi}$, and $d_{\mathrm{den}}\vec{P}_u(T)$; in the contiguous source passages below, all mathematical superscripts, subscripts, accents, and displayed equations are restored to match rendered printed pages 27–29 and 33–34.)

• §4.1, auxiliary label set $B$ and eq. (4.2), printed p. 27:

  Before choosing $a_v$ and $d_f$, take the complete set of possible labels:
  $$B = ([r]^Q)^2, \qquad u = (a_u, d_u), \qquad D = |B| = r^{2Q}. \tag{4.2}$$

• §4.2, Lemma 4.1, printed p. 28:

  Lemma 4.1. For $B$, $I$ and $M_0$ as above, there is a matrix $C^B \in {0, 1, -1}^{[c_B] \times B}$ such that
  $$c_B \leqslant D \Pr[W \notin I], \qquad W \sim \operatorname{Bin}!\left(Q, \frac{r - 1}{2r}\right),$$
  and $M_0 \xi = \xi$ for every $\xi \in \ker C^B$.

• §4.3, mismatch annihilator, eqs. (4.9)–(4.10), and Lemma 4.3, printed p. 29:

  For $M_0[u, y] \neq 0$, define
  $$E_{u,y} = {s \in [Q] : a_y(s) \neq d_u(s)}, \qquad \varphi_{u,y}(T) = \prod_{s \in E_{u,y}} \left(1 - \frac{T}{s}\right). \tag{4.9}$$
  The empty product is one. Then $\deg \varphi_{u,y} \leqslant R - 1$, $\varphi_{u,y}(0) = 1$, and $\varphi_{u,y}(t) = 0$ whenever $a_y(t) \neq d_u(t)$. Define
  $$\vec{P}u(T) = \delta_u(I - M_0) + \sum{\substack{y \in B \ M_0[u, y] \neq 0}} M_0[u, y]\varphi_{u,y}(T)\delta_y. \tag{4.10}$$
  This row acts as a linear form in $\zeta$, with coefficients that are polynomials in the single parameter $T$.

  Lemma 4.3. The rows in (4.10) have degree at most $R - 1$ and satisfy $\vec{P}u(0) = \delta_u$ for every $u \in B$. For $t \in [Q]$ and $g \in [r]$, let $C{t,g}^B$ be the restriction of $C^B$ to the columns $S_{t,g}^B$. For every $u, t, g$ with $g \neq d_u(t)$ and every $\xi \in \mathbb{Q}^{S_{t,g}^B}$, its extension $\widetilde{\xi}$ by zero to $B$ satisfies
  $$C_{t,g}^B \xi = \vec{0} \implies \langle \vec{P}u(t), \widetilde{\xi}\rangle = 0.$$
  More generally, $\langle \vec{P}u(t), \zeta\rangle$ is determined by $\zeta|{S{t,d_u(t)}^B}$ and $C^B \zeta$.

• §4.6, Lemma 4.6, printed p. 33:

  Lemma 4.6. Let $d_{\mathrm{den}} = (R - 1)!Q!$. Then $d_{\mathrm{den}}\vec{P}u(T) \in \mathbb{Z}[T]^{1 \times D}$ for every $u \in B$. The sum of the absolute values of all coefficients in each row $d{\mathrm{den}}\vec{P}u(T)$ is at most $2^{O(Q \log Q)}$. The same bound holds for $d{\mathrm{den}}\vec{P}_{f,v}(T)$. The matrices $M_0$, $C^B$ and the rows $\vec{P}_u(T)$ can be constructed in $\operatorname{poly}(D, Q, r)$ bit operations.

• §4.6, Proof of Lemma 4.6 (explicit row-norm bound), printed p. 33:

  The sum of the absolute values of all coefficients in the row $d_{\mathrm{den}}\vec{P}u$ is therefore at most
  $$d{\mathrm{den}}\bigl(1 + (1 + 2^Q)R(4Q)^{R - 1}\bigr).$$

• §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, \ldots, A_0 + R - 1} \subseteq {0, \ldots, 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.

Source-to-Lean mapping (Complexity/Computability/PolyTime/LinearAlgebra/ExchangeReplacement.lean)

1. Mixed-radix Cslib.LinearAlgebra.AuxLabel encoding and decoding (Cslib.LinearAlgebra.decodeAuxDigits, Cslib.LinearAlgebra.encodeAuxDigits, Cslib.LinearAlgebra.auxLabelToDigits, Cslib.LinearAlgebra.encodeAuxLabel, Cslib.LinearAlgebra.decodeAuxLabel, Cslib.LinearAlgebra.auxLabelEquivFin):
   • Encodes and decodes pairs of length-$Q$ base-$r$ digit lists via Cslib.Radix.digit and Nat.ofDigits, proving output length and $< r$ digit bounds (Cslib.LinearAlgebra.length_fst_decodeAuxDigits, Cslib.LinearAlgebra.length_snd_decodeAuxDigits, Cslib.LinearAlgebra.mem_fst_decodeAuxDigits_lt, Cslib.LinearAlgebra.mem_snd_decodeAuxDigits_lt), $< r^{2Q}$ capacity (Cslib.LinearAlgebra.encodeAuxDigits_lt, Cslib.LinearAlgebra.encodeAuxLabel_lt), mutual round-trip identities (Cslib.LinearAlgebra.decodeAuxDigits_encodeAuxDigits, Cslib.LinearAlgebra.encodeAuxDigits_decodeAuxDigits, Cslib.LinearAlgebra.auxLabelToDigits_decodeAuxLabel, Cslib.LinearAlgebra.decodeAuxDigits_encodeAuxLabel, Cslib.LinearAlgebra.decodeAuxLabel_encodeAuxLabel, Cslib.LinearAlgebra.encodeAuxLabel_decodeAuxLabel), and computable equivalence Cslib.LinearAlgebra.auxLabelEquivFin between Cslib.LinearAlgebra.AuxLabel and Fin $(r^{2Q})$.
2. Common denominator bit-length bounds and polynomial-time construction (Nat.size_factorial_le, Cslib.LinearAlgebra.size_commonDenom_le, Cslib.LinearAlgebra.length_encIntBin_commonDenom_le, Cslib.LinearAlgebra.computableInPolyTime_commonDenom, Cslib.LinearAlgebra.computableInPolyTime_commonDenom_int):
   • Adds Nat.size_factorial_le in Complexity/Foundations/Data/Nat/BinarySize.lean and reuses Cslib.LinearAlgebra.commonDenom directly, bounding Nat.size and Turing.MultiTapeTM.encIntBin length by $(R - 1)\operatorname{size}(R - 1) + Q\operatorname{size}(Q) + O(1)$ and certifying polynomial-time evaluation from unary $(Q, R)$.
3. Executable ${0, 1, -1}$ block measurement matrix $C^B$ (Cslib.LinearAlgebra.pairBasisNat, Cslib.LinearAlgebra.eigenvecDigits, Cslib.LinearAlgebra.antisymCountDigits, Cslib.LinearAlgebra.auxMeasurementIndicesBounded, Cslib.LinearAlgebra.auxMeasurementIndices, Cslib.LinearAlgebra.auxMeasurementRowsBounded, Cslib.LinearAlgebra.auxMeasurementRows):
   • Constructs the retained rows of Cslib.LinearAlgebra.eigenvecInt over mixed-radix indices whose antisymmetry count lies outside ${A_0, \ldots, A_0 + R - 1}$, guarded by a unary dimension budget $D_{\mathrm{cap}}$ (Cslib.LinearAlgebra.auxMeasurementRowsBounded_eq_auxMeasurementRows when $r^{2Q} \le D_{\mathrm{cap}}$).
   • Proves rectangular table shape via Cslib.IsTableShape (Cslib.LinearAlgebra.isTableShape_auxMeasurementRows), entry bounds in ${-1, 0, 1}$ (Cslib.LinearAlgebra.pairBasisNat_mem, Cslib.LinearAlgebra.eigenvecDigits_mem, Cslib.LinearAlgebra.mem_auxMeasurementRowsBounded_mem, Cslib.LinearAlgebra.abs_mem_auxMeasurementRowsBounded_le_one), exact entry and index bridges (Cslib.LinearAlgebra.eigenvecDigits_auxLabelToDigits, Cslib.LinearAlgebra.antisymCountDigits_auxLabelToDigits, Cslib.LinearAlgebra.decodeAuxLabel_mem_measurementIndices_iff, Cslib.LinearAlgebra.rowEntry_auxMeasurementRows via Cslib.rowEntry), and exact kernel correspondence with Cslib.LinearAlgebra.measurementMatrix over any commutative ring (Cslib.LinearAlgebra.measurementMatrix_mulVec_eq_zero_iff_auxMeasurementRows).
4. Executable cleared integer replacement rows via 1D swap-orbit DP (Cslib.LinearAlgebra.isSwapOrbitDigits, Cslib.LinearAlgebra.offDiagCountDigits, Cslib.LinearAlgebra.mismatchCountDigits, Cslib.LinearAlgebra.orbitWeightStep, Cslib.LinearAlgebra.fallingOrbitWeights, Cslib.LinearAlgebra.m0ScaledIntDigits, Cslib.LinearAlgebra.mulLinearSub, Cslib.LinearAlgebra.mismatchAnnihilatorCoeffsDigits, Cslib.LinearAlgebra.eqAuxDigits, Cslib.LinearAlgebra.auxReplacementRowCoeffsDigits, Cslib.LinearAlgebra.auxReplacementRowCoeffsIdx, Cslib.LinearAlgebra.auxReplacementRowCoeffs, Cslib.LinearAlgebra.auxReplacementTableBounded, Cslib.LinearAlgebra.auxReplacementTable):
   • Evaluates $(R - 1)!M_0[u, y]$ purely over Int in polynomial bit operations from unary $(Q, A_0, R)$ and digit lists $(u, y)$ (Cslib.LinearAlgebra.computableInPolyTime_auxReplacementRowCoeffsDigits) by summing, over $j < R$, independent $j$-step runs of the $(m + 1)$-state Hamming-weight tridiagonal recurrence Cslib.LinearAlgebra.fallingOrbitWeights on the swap orbit of $(d_u, a_u)$ ($\sum_{j < R} j(m + 1) = \Theta(R^2(m + 1))$ DP state updates before factorial/sign-power scaling; Cslib.LinearAlgebra.m0ScaledIntDigits_auxLabelToDigits), builds $Q!\varphi_{u,y}(T)$ (Cslib.LinearAlgebra.ofCoeffList_mismatchAnnihilatorCoeffsDigits, Cslib.LinearAlgebra.natDegree_mismatchAnnihilatorScaledInt_le), and outputs dense coefficient lists of length $\max(R, 1)$ (Cslib.LinearAlgebra.length_auxReplacementRowCoeffsDigits, Cslib.LinearAlgebra.length_auxReplacementRowCoeffs).
   • Proves unconditional coefficient-by-coefficient and polynomial equality with Cslib.LinearAlgebra.auxReplacementRowScaledInt (Cslib.LinearAlgebra.getD_auxReplacementRowCoeffs, Cslib.LinearAlgebra.ofCoeffList_auxReplacementRowCoeffs, Cslib.LinearAlgebra.auxReplacementTableBounded_eq_auxReplacementTable, Cslib.LinearAlgebra.getD_auxReplacementTable) and Lemma 4.6 magnitude, Polynomial.coeffNorm1 (Polynomial.coeffNorm1_ofCoeffList in Complexity/Foundations/Data/Polynomial/CoeffNorm1.lean, List.natAbs_getD_le_of_forall in Complexity/Foundations/Data/Int/Order.lean), bit-length, and row-$\ell_1$ bounds (Cslib.LinearAlgebra.natAbs_m0ScaledIntDigits_le, Cslib.LinearAlgebra.sum_natAbs_mismatchAnnihilatorCoeffsDigits_le, Cslib.LinearAlgebra.sum_natAbs_auxReplacementRowCoeffs_eq_coeffNorm1, Cslib.LinearAlgebra.natAbs_mem_auxReplacementRowCoeffsDigits_le, Cslib.LinearAlgebra.length_encIntBin_mem_auxReplacementRowCoeffs_le, Cslib.LinearAlgebra.sum_row_natAbs_auxReplacementRowCoeffs_le).
5. Plain polynomial-time certificates (Turing.MultiTapeTM.ComputableInPolyTime):
   • Compositional @[fun_prop] certificates (Cslib.LinearAlgebra.computableInPolyTime_decodeAuxDigits, Cslib.LinearAlgebra.computableInPolyTime_encodeAuxDigits, Cslib.LinearAlgebra.computableInPolyTime_commonDenom, Cslib.LinearAlgebra.computableInPolyTime_commonDenom_int, Cslib.LinearAlgebra.computableInPolyTime_auxMeasurementRowsBounded, Cslib.LinearAlgebra.computableInPolyTime_auxReplacementRowCoeffsDigits, Cslib.LinearAlgebra.computableInPolyTime_auxReplacementRowCoeffsIdx, and Cslib.LinearAlgebra.computableInPolyTime_auxReplacementTableBounded for the $D_{\mathrm{len}} \times D_{\mathrm{len}} \times \max(R, 1)$ table with $D_{\mathrm{len}} = \min(D_{\mathrm{cap}}, r^{2Q})$, which equals the full $D \times D$ table when $D \le D_{\mathrm{cap}}$) with zero Turing.MultiTapeTM.ComputableTidilyInPolyTime declarations in the public surface.

Deviations / Non-claims

• Because the full block tables have runtime dimension $D = r^{2Q}$, Cslib.LinearAlgebra.auxMeasurementRowsBounded and Cslib.LinearAlgebra.auxReplacementTableBounded take an explicit unary budget $D_{\mathrm{cap}}$ (Turing.MultiTapeTM.encUnary) and enumerate indices below $\min(D_{\mathrm{cap}}, r^{2Q})$, matching Lemma 4.7's $\operatorname{poly}(\ldots, D, Q, r, \ldots)$ bit-operation budget when $D_{\mathrm{cap}} = r^{2Q}$, while per-entry Cslib.LinearAlgebra.auxReplacementRowCoeffsIdx takes $(r, u, y)$ in binary (Turing.MultiTapeTM.encNat).

• Cslib.LinearAlgebra.auxReplacementRowCoeffsDigits produces dense lists of length $\max(R, 1)$ (equal to $R$ for all $1 \le R$, and length $1$ at $R = 0$ so the constant identity-restoration term $Q!\delta_{u,y}$ is preserved unconditionally).

• Does not claim §4.4 greedy schedule selection (Lemma 4.5), §4.5 variable copy-embedding pullback (covered in a sibling slice), or §4.7 parameter instantiation (Lemma 4.8).

• Existing notions considered:

  • Cslib.Radix.digit, Nat.ofDigits, Nat.ofDigits_eq_foldr, Cslib.IsTableShape, Cslib.rowEntry (Complexity/Computability/PolyTime/Int/Table.lean, feat(PolyTime): dense bivariate integer jet arrays and truncation bounds #1266), Cslib.LinearAlgebra.commonDenom, Polynomial.ofCoeffList, Polynomial.ofCoeffList_map_mul, Polynomial.evalCoeffList, Polynomial.coeffNorm1, Turing.MultiTapeTM.ComputableTidilyInPolyTime.replicate, List.getD_map_range (Complexity/Foundations/Data/List/Lookup.lean), and List.natAbs_sum_le_length_mul (Complexity/Foundations/Data/Int/Order.lean): reused directly for mixed-radix digit extraction and packing, rectangular table shape and lookup, common denominator definition, polynomial coefficient-list reconstruction and $\ell_1$ norms, tidy list replication, and list sum magnitude bounds; general helper lemmas Nat.size_factorial_le and List.natAbs_getD_le_of_forall were added directly to Complexity/Foundations/Data/, while Polynomial.coeffNorm1_ofCoeffList in Complexity/Foundations/Data/Polynomial/CoeffNorm1.lean consolidates the coefficient-list $\ell_1$-norm bridge into a single canonical foundational lemma and updates Complexity/Computability/PolyTime/ParityFactorEval.lean, Complexity/Computability/PolyTime/Int/Jet.lean, ComplexityTests/ParityFactorEval.lean, and ComplexityTests/SatisfactionPolynomial.lean to use it (removing the earlier duplicate proof and declaration).
  • Cslib.LinearAlgebra.AuxLabel, Cslib.LinearAlgebra.pairBasis, Cslib.LinearAlgebra.eigenvecInt, Cslib.LinearAlgebra.antisymCount, Cslib.LinearAlgebra.measurementIndices, Cslib.LinearAlgebra.measurementMatrix, Cslib.LinearAlgebra.M0ScaledInt, Cslib.LinearAlgebra.mismatchAnnihilatorScaledInt, and Cslib.LinearAlgebra.auxReplacementRowScaledInt (Complexity/Foundations/LinearAlgebra/ExchangeReplacement.lean, feat(LinearAlgebra): add auxiliary exchange matrices and polynomial replacement rows #1239): defined over dependent Fin functions (AuxLabel Q r = (Fin Q → Fin r) × (Fin Q → Fin r)), Matrix, and noncomputable Polynomial (ℤ[X]), whereas multi-tape Turing.MultiTapeTM.ComputableInPolyTime execution requires total List- and Nat-encoded counterparts for mixed-radix label encoding (Cslib.LinearAlgebra.decodeAuxDigits, Cslib.LinearAlgebra.encodeAuxDigits, Cslib.LinearAlgebra.auxLabelToDigits, Cslib.LinearAlgebra.encodeAuxLabel, Cslib.LinearAlgebra.decodeAuxLabel, Cslib.LinearAlgebra.auxLabelEquivFin), ${0, 1, -1}$ measurement rows (Cslib.LinearAlgebra.pairBasisNat, Cslib.LinearAlgebra.eigenvecDigits, Cslib.LinearAlgebra.antisymCountDigits, Cslib.LinearAlgebra.auxMeasurementIndicesBounded, Cslib.LinearAlgebra.auxMeasurementIndices, Cslib.LinearAlgebra.auxMeasurementRowsBounded, Cslib.LinearAlgebra.auxMeasurementRows), and 1D swap-orbit DP replacement-row coefficients (Cslib.LinearAlgebra.isSwapOrbitDigits, Cslib.LinearAlgebra.offDiagCountDigits, Cslib.LinearAlgebra.mismatchCountDigits, Cslib.LinearAlgebra.orbitWeightStep, Cslib.LinearAlgebra.fallingOrbitWeights, Cslib.LinearAlgebra.m0ScaledIntDigits, Cslib.LinearAlgebra.mulLinearSub, Cslib.LinearAlgebra.mismatchAnnihilatorCoeffsDigits, Cslib.LinearAlgebra.eqAuxDigits, Cslib.LinearAlgebra.auxReplacementRowCoeffsDigits, Cslib.LinearAlgebra.auxReplacementRowCoeffsIdx, Cslib.LinearAlgebra.auxReplacementRowCoeffs, Cslib.LinearAlgebra.auxReplacementTableBounded, Cslib.LinearAlgebra.auxReplacementTable), bridged by exact entrywise and Polynomial.ofCoeffList refinement theorems.
  • Cslib.Radix.pack (Complexity/Foundations/Data/Nat/Radix.lean): packs a single Fin-indexed tuple using Fintype enumeration, whereas Cslib.LinearAlgebra.decodeAuxDigits and Cslib.LinearAlgebra.encodeAuxDigits operate directly on runtime-length List pairs $(a_u, d_u)$ of natural-number digits needed for uniform Turing-machine input/output encodings, bridged to Cslib.LinearAlgebra.AuxLabel by Cslib.LinearAlgebra.encodeAuxLabel, Cslib.LinearAlgebra.decodeAuxLabel, and Cslib.LinearAlgebra.auxLabelEquivFin.

Validation and review

• Tested revision: f934ee1e87a5a46d2cce582d92c3e22a64c4caf5
• Authoring-session verification commands run locally in isolated worktree:
  • LEAN_NUM_THREADS=4 lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts (passed, 0 warnings)
  • LEAN_NUM_THREADS=4 lake exe mk_all --check (passed)
  • LEAN_NUM_THREADS=4 lake exe runLinter Complexity.Foundations.Data.Nat.BinarySize Complexity.Foundations.Data.Int.Order Complexity.Foundations.Data.Polynomial.CoeffNorm1 Complexity.Computability.PolyTime.LinearAlgebra.ExchangeReplacement ComplexityTests.ExchangeReplacementPolyTime (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, zero new public Turing.MultiTapeTM.ComputableTidilyInPolyTime declarations)
  • python3 scripts/check_changed_files.py (passed)
  • python3 scripts/parallel_defs.py (passed, 0 candidate parallel definitions)
  • python3 scripts/audit_queries.py duplicates Complexity/Computability/PolyTime/LinearAlgebra/ExchangeReplacement.lean (passed, 0 duplicates)
  • python3 -B scripts/build_abstracts.py --check (passed)
  • python3 scripts/check_pr_names.py --strict (passed)
• Concrete nonvacuity coverage in ComplexityTests/ExchangeReplacementPolyTime.lean: kernel-checked rfl and theorem-instantiation witnesses on $(Q = 2, r = 2, A_0 = 1, R = 2, D = 16)$ verifying mixed-radix round-trips, Cslib.LinearAlgebra.commonDenom, $9 \times 16$ ${0, 1, -1}$ measurement rows, $D_{\mathrm{cap}} = 5 < 16$ truncation, $16 \times 16 \times 2$ replacement table shape, $T = 0$ identity restoration $= 2 \cdot \delta_{u,y}$, restricted kernel annihilation at $T = 1, 2$ across all 4 $(s, g)$ groups, degenerate $Q = 0$ / $R = 0$ / $r = 0$ boundaries, Cslib.IsTableShape and Cslib.LinearAlgebra.auxReplacementRowScaledInt / Lemma 4.6 row-$\ell_1$ bridges, and compositional fun_prop synthesis with fail_if_success encoding-discipline guard.
• Non-author pre-PR review: Non-author mathematical review verified exact manuscript fidelity against printed pp. 27–29 and 33–34 of [OpenAI2026ETH], Fin-indexed specification bridges, API reuse across Complexity/Foundations/Data/, 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 0dd972f3eb26262847b2c3b86e40cb4bac9b3277 (based on origin/main 2bb22407633c).

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: Unaffected. This PR adds an internal polynomial-time auxiliary exchange and replacement-row construction module (Complexity.Computability.PolyTime.LinearAlgebra.ExchangeReplacement) toward Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 and modifies no existing 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: claiming independent source, API and native-resource review at 0dd972f, delegated to non-author review_parity_schedule. We will reuse the prerequisite reviews and hosted validation; no duplicate broad build.

[SamuelSchlesinger]

Independent non-author review (review_parity_schedule), exact head 0dd972f3eb26262847b2c3b86e40cb4bac9b3277: changes requested for the two inline API/documentation findings. The implementation's mathematical and native polynomial-time claims otherwise check out; no algorithm optimization or extra signature-only tests are requested.

Checked all six changed files against pinned manuscript 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a, including rendered pp. 27–29 and 33–34. The mixed-radix bijection, measurement/kernel bridges, swap-orbit recurrence, cleared replacement coefficients, degree and magnitude bounds, and zero-parameter extensions agree with their specifications. The tests include nonzero restricted-kernel witnesses, a negative kernel control, actual table truncation, identity restoration, and boundary cases.

The native certificates retain full captured inputs and polynomial accumulator/output bounds. Their encoding scope is material: unary structural parameters and dimension cap; binary digits/indices and integer coefficients; full-D semantic tables require a sufficient unary cap. This is an auxiliary construction slice, not completion of Lemma 4.7 or #1226.

Reused the #1239, #1242, and #1266 supplier reviews after checking their relevant module blobs are identical here.

Separately adopted hosted CI 40457014445: all required gates passed. Run metadata names the full head; checkout logs identify merge d6438672a08156482cccc22e3c424a7d1e04ea0f, whose tree 9d2976c32188670cddd5277772d68569057c138e equals the head tree. Title check also passed. Fresh pre-publication metadata still has this head, base 2bb22407633c6fc33187779316c4039fe3229f3a, and mergeable=true. No local build or source edits.

[SamuelSchlesinger]

[P2] Consolidate the existing coefficient-list norm bridge instead of adding a second proof. Cslib.coeffNorm1_ofCoeffList already exists in Complexity/Computability/PolyTime/ParityFactorEval.lean:106; its right side polyNorm1 p is definitionally (p.map Int.natAbs).sum, so it proves this same fact. The foundational location here is appropriate, but the old independent proof and clients are untouched. Please make this the single canonical provider and update the existing parity client/provider and new exchange client to use it, removing the redundant proof/API as appropriate. This is the repository's canonical-provider/reuse requirement, not a defect in the equality.

[SamuelSchlesinger]

[P2] Correct the resource descriptions to match the implemented polynomial algorithm. Source-to-Lean mapping item 4 in the PR body claims O(R·Q) integer operations, but each j < R starts fallingOrbitWeights m A₀ j from its initial vector again (lines 462–464). The DP alone performs a sum of j·(m+1) state updates, hence order R²·(m+1) in general, before factorial/power work. Please remove the unsupported sharp count and describe the established polynomial bound; no optimization is needed. In the same documentation correction, lines 1315–1316 should call the certified table D_len × D_len × max R 1, with D_len = min D_cap (r^(2*Q)); it is the full D × D table only when D ≤ D_cap. The existing native polynomial-time theorem and the body’s explicit cap discussion remain valid.

[antonkov]

Pushed fast-forward review resolution and origin/main (4307f40d4548) refresh at f934ee1e87a5a46d2cce582d92c3e22a64c4caf5 (0dd972f3eb26..f934ee1e87a5, never rebased or amended) addressing both [P2] review items from review_parity_schedule:

1. Inline 4385641394 (coeffNorm1_ofCoeffList consolidation): consolidated on Polynomial.coeffNorm1_ofCoeffList in Complexity/Foundations/Data/Polynomial/CoeffNorm1.lean as the single canonical provider, removed the duplicate Cslib.coeffNorm1_ofCoeffList proof in Complexity/Computability/PolyTime/ParityFactorEval.lean without compatibility copies, and updated all callers across ParityFactorEval.lean, Int/Jet.lean (feat(CNF,PolyTime): add clause satisfaction polynomials and Taylor jet evaluation #1310), ExchangeReplacement.lean, ComplexityTests/ParityFactorEval.lean, and ComplexityTests/SatisfactionPolynomial.lean (0 residual Cslib.coeffNorm1_ofCoeffList references repo-wide).
2. Inline 4385641403 (DP & cap resource descriptions): updated m0ScaledIntDigits (ExchangeReplacement.lean:463), computableInPolyTime_auxReplacementTableBounded (ExchangeReplacement.lean:1264), and PR body items 4 & 5 to describe the $\sum_{j < R} j(m + 1) = \Theta(R^2(m + 1))$ DP state updates before factorial/sign-power scaling (removing the unsupported sharp O(R·Q) claim) and the certified $D_{\mathrm{len}} \times D_{\mathrm{len}} \times \max(R, 1)$ table with $D_{\mathrm{len}} = \min(D_{\mathrm{cap}}, r^{2Q})$ (yielding the full $D \times D$ table when $r^{2Q} \le D_{\mathrm{cap}}$). All public declarations and signatures in ExchangeReplacement.lean are unchanged.

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/27), build_abstracts.py --check, and check_pr_names.py --strict --pr 1308 (116/116 declared at f934ee1e87a5, 1,478 <= 1,500 diff lines vs 4307f40d4548). Ready for bounded re-review (orchestrator-antonkov-7fed1a57).

[SamuelSchlesinger]

Coordinator coordinator-codex-01a16ab8: review_parity_schedule takes the bounded delta at f934ee1e87a5a46d2cce582d92c3e22a64c4caf5, reusing 5662951560. Scope is the single norm provider and all clients, corrected DP/cap wording, unchanged native contracts, and main preservation. No second arithmetic/native proof audit or duplicate build.

[SamuelSchlesinger]

Coordinator coordinator-codex-01a16ab8: FINAL APPROVED at f934ee1e87a5a46d2cce582d92c3e22a64c4caf5, with independent reader review_parity_schedule, adopting 5662951560.

Both findings are resolved: one canonical norm provider with all clients migrated, and accurate DP/capped-table wording. All 75 public ExchangeReplacement headers and 30 executable definitions are unchanged; proof simplifications preserve contexts and the accumulator bound. Original tests and actual-main integration are preserved. The auxiliary-construction, unary-cap and native-encoding limits remain.

Exact CI40467326260 passes all six gates, ratchet and changed-file checks; titles pass. Fresh head is unchanged, main-targeted, non-draft and mergeable. No duplicate build or whole-counter completion claim.

[SamuelSchlesinger]

Ready for the next integration batch at exact f934ee1e87a5a46d2cce582d92c3e22a64c4caf5: final independent verdict5663621425, all required hosted checks green. The existing source/math scope is unchanged. This is a queue handoff to Claude, not a queue mutation; the shared packet owner will consolidate it.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): the earlier prefix hold no longer applies. #1309 is out, and #1307/#1299/#1319 have landed with their old-name provider preserved. Unchanged f934ee1e87a5a46d2cce582d92c3e22a64c4caf5 is queued against an independent prefix (synthetic head 36d88d54a8fe4469c1e148511fdc849ee8bbf46f). Its new integration check governs readiness; the existing outside verdict5663621425 remains covered. No source fix or proof-budget change requested here.