[antonkov]

Change

Part of #1226 (building on #1253, #1262, #1294, #1301, and #1308). Formalizes the executable neutral-singleton scope augmentation and the deterministic polynomial-time Lemma 4.7 replacement-design builder from §4.6 (Lemma 4.7, printed pp. 33–34) and §§5.3, 5.5 (printed pp. 37–38) of [OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH] (pinned revision 7ef5c0cc), assembling Complexity/Computability/PolyTime/LinearAlgebra/ExchangeReplacement.lean (#1308) and Complexity/Computability/PolyTime/LinearAlgebra/CopyPlacement.lean (#1301) over supplied balanced schedules, together with plain Turing.MultiTapeTM.ComputableInPolyTime certificates and semantic bridges to Cslib.BitString.withNeutralScope and Cslib.LinearAlgebra.ReplacementDesign, in Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean.

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

(Mathematical-transcription note: Plain-text extraction from the source PDF flattens rendered superscripts, subscripts, over-accents, calligraphic symbols, and displayed equations such as $(I_f){f \in \mathcal{F}}$, $M = \sum_f |I_f|$, $D = r^{2Q}$, $\Pr[W \notin \mathcal{I}] \leqslant \tau / (rb)$, $C^{\mathcal{B}}$, $c{\mathcal{B}}$, $\mathcal{A}\ell$, $\vec{P}{f,v}(0) = \delta_v$, $C_{t,g}$, and $\sum_{g=1}^r c_{t,g} \leqslant 2\tau n$; in the contiguous source passages below, all mathematical superscripts, subscripts, accents, calligraphic fonts, and displayed equations are restored to match rendered printed pages 33–34 and 37–38.)

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

  Lemma 4.7. Let $n, b, w \geqslant 1$ be integers, and let $(I_f)_{f \in \mathcal{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 $\mathcal{I} = {A_0, \ldots, A_0 + R - 1} \subseteq {0, \ldots, Q}$ satisfies
  $$\Pr[W \notin \mathcal{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, |\mathcal{F}|, D, Q, r, b, w)$ bit operations.

  Proof. Lemma 4.1 constructs $C^{\mathcal{B}}$ with $c_{\mathcal{B}} \leqslant \tau D/(rb)$. Lemmas 4.2 and 4.3 give the auxiliary polynomial rows. Lemma 4.5 chooses the variable and factor groups with $hD \leqslant 2M$ and $|S_{t,g}| \leqslant 2n/r$. The maps in (4.14) and (4.15) then give rows with $\vec{P}{f,v}(0) = \delta_v$, degree at most $R - 1 \leqslant R$, and the required kernel implication. Every row of $C{t,g}$ has absolute row sum at most $D$, and (4.16) gives $\sum_{g=1}^r c_{t,g} \leqslant 2\tau n$ for each $t \in [Q]$. Lemma 4.6 supplies the common denominator and coefficient bounds. Together, the constructions take $\operatorname{poly}(n, M, |\mathcal{F}|, D, Q, r, b, w)$ bit operations, and the resulting arrays occupy $\operatorname{poly}(n, M, |\mathcal{F}|, D, Q, r, b, w)$ bits. $\square$

• §5.3, neutral-singleton scope augmentation, printed p. 37:

  Within a factor, every occurrence of $X_v$ uses the same replacement form; different factors may use different forms for $X_v$. Even if each factor receives its own independent inputs, $L_i$ has degree at most $k$ in those inputs. Lemma 5.2 bounds the input degree of the product in $\mathcal{A}\ell$ by $d = k(m{\mathrm{test}} + 2(\ell - 1))$. Thus the product satisfies precisely the degree hypothesis (3.2) of the common routine. Adding factors equal to one with scope ${v}$ ensures that all declared variables occur in the construction.

• §5.5, Proof of Theorem 2.2 (neutral singleton factors), printed p. 38:

  Let $\mathcal{P}$ be the supplied polynomial system. An empty list of equations gives $2^n$ common zeros; a constant equation $1 = 0$ gives none. Discard equations $0 = 0$. Include a neutral factor equal to one with scope ${v}$ for each declared variable $v$, and write
  $$M = \sum_{f \in \mathcal{F}} |I_f|$$
  for the total number of factor–variable incidences.

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

1. Executable neutral-singleton scope augmentation and agreement with Cslib.BitString.withNeutralScope (Cslib.LinearAlgebra.withNeutralScopesList, Cslib.LinearAlgebra.listScopeFamily, Cslib.LinearAlgebra.withNeutralScopesIndexEquiv):
   • Cslib.LinearAlgebra.withNeutralScopesList appends the $n_{\mathrm{free}}$ singleton scopes $[0], \dots, [n_{\mathrm{free}} - 1]$ to an executable scope list (Cslib.LinearAlgebra.length_withNeutralScopesList), while Cslib.LinearAlgebra.listScopeFamily extracts the semantic Fin-indexed scope family (Cslib.LinearAlgebra.mem_listScopeFamily, Cslib.LinearAlgebra.card_listScopeFamily_le).
   • Via Cslib.LinearAlgebra.withNeutralScopesIndexEquiv (Cslib.LinearAlgebra.val_withNeutralScopesIndexEquiv_inl, Cslib.LinearAlgebra.val_withNeutralScopesIndexEquiv_inr), proves exact scope-family agreement Cslib.LinearAlgebra.listScopeFamily_withNeutralScopesList with Cslib.BitString.withNeutralScope, plus variable-incidence increment Cslib.LinearAlgebra.varIncidence_listScopeFamily_withNeutralScopesList and total-incidence increment Cslib.LinearAlgebra.totalIncidence_listScopeFamily_withNeutralScopesList.
2. Canonical scope incidences and executable Lemma 4.5 schedule balance (Cslib.LinearAlgebra.canonicalScopeVars, Cslib.LinearAlgebra.scopeIncidencesList, Cslib.LinearAlgebra.scopeIncidenceEquivFin, Cslib.LinearAlgebra.BalancedSchedule):
   • Cslib.LinearAlgebra.canonicalScopeVars (Cslib.LinearAlgebra.mem_canonicalScopeVars, Cslib.LinearAlgebra.nodup_canonicalScopeVars, Cslib.LinearAlgebra.canonicalScopeVars_isEmpty_iff) and Cslib.LinearAlgebra.scopeIncidencesList (Cslib.LinearAlgebra.mem_scopeIncidencesList, Cslib.LinearAlgebra.nodup_scopeIncidencesList, Cslib.LinearAlgebra.length_scopeIncidencesList) enumerate factor–variable incidences canonically in List.Nodup order, establishing a bijection Cslib.LinearAlgebra.scopeIncidenceEquivFin with Cslib.BalancedSchedules.ScopeIncidence via Cslib.LinearAlgebra.finToScopeIncidence (Cslib.LinearAlgebra.bijective_finToScopeIncidence, Cslib.LinearAlgebra.finToScopeIncidence_scopeIncidenceEquivFin, Cslib.LinearAlgebra.scopeIncidenceEquivFin_finToScopeIncidence, Cslib.LinearAlgebra.getElem_scopeIncidencesList_equiv, Cslib.LinearAlgebra.val_scopeIncidenceEquivFin_eq_idxOf).
   • Cslib.LinearAlgebra.normalizeScheduleWord, Cslib.LinearAlgebra.normalizeVarSchedules, and Cslib.LinearAlgebra.normalizeScopeSchedules (Cslib.LinearAlgebra.length_normalizeScheduleWord, Cslib.LinearAlgebra.length_normalizeVarSchedules, Cslib.LinearAlgebra.length_normalizeScopeSchedules) normalize supplied variable/factor schedule lists to length-$Q$ words over ${0, \dots, \max(r, 1) - 1}$ with empty in-range scopes normalized to all-$0$ words, inducing typed assignments Cslib.LinearAlgebra.varAssignOfList and Cslib.LinearAlgebra.factorAssignOfList (Cslib.LinearAlgebra.val_varAssignOfList, Cslib.LinearAlgebra.val_factorAssignOfList, Cslib.LinearAlgebra.factorAssignOfList_of_empty) and packed auxiliary incidence labels Cslib.LinearAlgebra.incidenceLabelsList (Cslib.LinearAlgebra.length_incidenceLabelsList, Cslib.LinearAlgebra.incidenceLabelsList_eq_ofFn).
   • Cslib.LinearAlgebra.BalancedSchedule expresses Lemma 4.5's occupancy bounds $c_u \cdot r^{2Q} \le 2M$ and $|S_{t,g}| \cdot r \le 2 n_{\mathrm{free}}$, with pure list equivalence Cslib.LinearAlgebra.balancedSchedule_iff_exec (supporting decide verification) and non-vacuous schedule existence Cslib.LinearAlgebra.exists_balancedSchedule_of_scopes from Cslib.BalancedSchedules.exists_balanced_schedules_of_scopes.
3. Bundled Lemma 4.7 design data and executable constructor (Cslib.LinearAlgebra.ReplacementDesignData, Cslib.LinearAlgebra.buildReplacementDesignData, Cslib.LinearAlgebra.ReplacementDesignData.lookupReplacementRow):
   • Cslib.LinearAlgebra.ReplacementDesignData (encoded on multi-tape Turing machines via Cslib.LinearAlgebra.ReplacementDesignTuple, Cslib.LinearAlgebra.ReplacementDesignData.equivTuple, Cslib.LinearAlgebra.encReplacementDesignTuple, and Cslib.LinearAlgebra.encReplacementDesignData) bundles the step-and-group variable partitions, normalized factor schedules, canonical incidences, copy count $h = \lfloor 2M / r^{2Q} \rfloor$, copy placements, pulled-back integer measurement matrix $\widehat{C}$, group-restricted integer measurement matrices $C_{t,g} = \widehat{C}|{S{t,g}}$, cleared common denominator $d_{\mathrm{den}} = (R - 1)! Q!$, and per-incidence $n_{\mathrm{free}} \times R$ cleared replacement-row tables.
   • Cslib.LinearAlgebra.buildReplacementDesignData assembles Cslib.LinearAlgebra.auxMeasurementRowsBounded, Cslib.LinearAlgebra.auxReplacementTableBounded, Cslib.LinearAlgebra.commonDenom, Cslib.LinearAlgebra.CopyPlacement.fiberRanks, Cslib.LinearAlgebra.CopyPlacement.varGroupList, Cslib.LinearAlgebra.CopyPlacement.pullbackMeasurementMatrix, Cslib.LinearAlgebra.CopyPlacement.restrictGroupColumns, and Cslib.LinearAlgebra.CopyPlacement.pullbackReplacementRow, while Cslib.LinearAlgebra.ReplacementDesignData.lookupReplacementRow retrieves the $n_{\mathrm{free}} \times R$ table for any factor–variable pair $(f, v)$.
4. Plain polynomial-time certificates (Turing.MultiTapeTM.ComputableInPolyTime):
   • Proves @[fun_prop] plain Turing.MultiTapeTM.ComputableInPolyTime certificates for neutral-singleton augmentation (Cslib.LinearAlgebra.computableInPolyTime_withNeutralScopesListWithInput, Cslib.LinearAlgebra.computableInPolyTime_withNeutralScopesList), schedule and incidence preprocessing (Cslib.LinearAlgebra.computableInPolyTime_scopeIncidencesList, Cslib.LinearAlgebra.computableInPolyTime_normalizeVarSchedules, Cslib.LinearAlgebra.computableInPolyTime_normalizeScopeSchedules, Cslib.LinearAlgebra.computableInPolyTime_incidenceLabelsList), all nine Cslib.LinearAlgebra.ReplacementDesignData field projections (Cslib.LinearAlgebra.computableInPolyTime_varGroups, Cslib.LinearAlgebra.computableInPolyTime_factorGroups, Cslib.LinearAlgebra.computableInPolyTime_incidences, Cslib.LinearAlgebra.computableInPolyTime_copyCount, Cslib.LinearAlgebra.computableInPolyTime_placements, Cslib.LinearAlgebra.computableInPolyTime_measurementMatrix, Cslib.LinearAlgebra.computableInPolyTime_groupMeasurementMatrices, Cslib.LinearAlgebra.computableInPolyTime_denom, Cslib.LinearAlgebra.computableInPolyTime_replacementRows), Cslib.LinearAlgebra.computableInPolyTime_buildReplacementDesignData (from unary numerical/size parameters $(n_{\mathrm{free}}, D_{\mathrm{cap}}, Q, r, A_0, R)$ and list-encoded scopes and schedules, bounding the copy count $h \le 2M$ in unary via Turing.MultiTapeTM.ComputableInPolyTime.binary_min_unary'), and Cslib.LinearAlgebra.computableInPolyTime_lookupReplacementRow, with zero new public Tidy declarations.
5. Semantic bridge to Cslib.LinearAlgebra.ReplacementDesign (Cslib.LinearAlgebra.constructedReplacementDesign, Cslib.LinearAlgebra.ReplacementDesignData.Refines, Cslib.LinearAlgebra.buildReplacementDesignData_spec):
   • From Cslib.LinearAlgebra.fiberBound_of_balancedSchedule and Cslib.LinearAlgebra.placeFinOfBalanced, Cslib.LinearAlgebra.constructedReplacementDesign builds a concrete Cslib.LinearAlgebra.ReplacementDesign over Cslib.LinearAlgebra.listScopeFamily under Lemma 4.7's numerical, interval, binomial-tail, and Cslib.LinearAlgebra.BalancedSchedule hypotheses.
   • Cslib.LinearAlgebra.ReplacementDesignData.Refines and Cslib.LinearAlgebra.buildReplacementDesignData_spec (packaged existentially in Cslib.LinearAlgebra.exists_replacementDesign_of_buildReplacementDesignData and specialized to neutral-padded scopes with $b = b_0 + 1$ in Cslib.LinearAlgebra.exists_replacementDesign_withNeutralScopesList) prove exact agreement across copy count, cleared denominator, List.Nodup variable-group lists of size $\le 2 n_{\mathrm{free}} / r$, factor group schedules, per-incidence Cslib.IsTableShape $n_{\mathrm{free}} \times R$ polynomial coefficient tables (Polynomial.ofCoeffList equal to Cslib.LinearAlgebra.varReplacementRowScaledInt), global $\mathbb{Q}$-kernel equivalence of $\widehat{C}$, and restricted-kernel evaluation annihilation at Cslib.LinearAlgebra.nodePoint from $C_{t,g}$.

Deviations / Non-claims

• Parameterizes Cslib.LinearAlgebra.buildReplacementDesignData over supplied schedule lists $(\mathrm{schedVar}, \mathrm{schedScope})$ together with the semantic hypothesis Cslib.LinearAlgebra.BalancedSchedule (whose non-vacuity under Lemma 4.7's size hypotheses is proved in Cslib.LinearAlgebra.exists_balancedSchedule_of_scopes); the executable polynomial-time conditional-expectation greedy loop of Lemma 4.5 (§4.4) is formalized in a separate slice of Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 (feat(PolyTime): add greedy slot-score arithmetic and streaming candidate selector #1327 and follow-up), while the Lemma 4.8 parameter schedule (§4.7) landed in feat(PolyTime/FineGrained): add polytime parameter schedule and exact feasibility checks #1305.

• Following Cslib.LinearAlgebra.ReplacementDesign (Complexity/Foundations/LinearAlgebra/ReplacementDesign.lean), 0-based indices Fin r and Fin Q represent $[r]$ and $[Q]$, so empty scopes normalize to all-$0$ schedule words (List.replicate Q 0) corresponding to $d_f(t) = 1 \in [r]$ in 1-based manuscript indexing, and the semantic bridge requires only $1 \le r$, $1 \le R$, $1 \le Q$, $0 \le \tau$, $M \le b n_{\mathrm{free}}$, and $\forall a < R - 1,\ A_0 + a \le Q$ (along with $r^{2Q} \le D_{\mathrm{cap}}$ so the bounded auxiliary tables coincide with the full $D = r^{2Q}$ tables).

• Existing notions considered:

  • Cslib.BitString.withNeutralFactors, Cslib.BitString.withNeutralScope, Cslib.BitString.varIncidence, Cslib.BitString.totalIncidence, Cslib.BitString.varIncidence_withNeutralFactors, Cslib.BitString.totalIncidence_withNeutralFactors, and Cslib.BitString.totalIncidence_withNeutralFactors_le (Complexity/Foundations/BooleanAnalysis/SparseBranching.lean, feat(BooleanAnalysis): univariate parity-product specialization and heavy-variable branch reduction (#1226) #1253), together with Cslib.LinearAlgebra.ReplacementDesign (Complexity/Foundations/LinearAlgebra/ReplacementDesign.lean, feat(LinearAlgebra): add Lemma 4.1 binomial row counts and Lemma 4.7 replacement design #1262) and Complexity/Foundations/BooleanAnalysis/SparseReplacementDesign.lean (feat(BooleanAnalysis): ReplacementDesign specialization of cleared parity zero counting #1294): reused directly as the semantic target of Cslib.LinearAlgebra.withNeutralScopesList and Cslib.LinearAlgebra.buildReplacementDesignData rather than duplicating scope-incidence or replacement-design structures.
  • Cslib.LinearAlgebra.encodeAuxDigits, Cslib.LinearAlgebra.encodeAuxLabel, Cslib.LinearAlgebra.decodeAuxLabel, Cslib.LinearAlgebra.commonDenom, Cslib.LinearAlgebra.auxMeasurementRowsBounded, and Cslib.LinearAlgebra.auxReplacementTableBounded (Complexity/Computability/PolyTime/LinearAlgebra/ExchangeReplacement.lean, feat(PolyTime/LinearAlgebra): add Vandermonde auxiliary rows and exchange replacement #1308), together with Cslib.LinearAlgebra.CopyPlacement.fiberRanks, Cslib.LinearAlgebra.CopyPlacement.varGroupList, Cslib.LinearAlgebra.CopyPlacement.pullbackMeasurementMatrix, Cslib.LinearAlgebra.CopyPlacement.restrictGroupColumns, and Cslib.LinearAlgebra.CopyPlacement.pullbackReplacementRow (Complexity/Computability/PolyTime/LinearAlgebra/CopyPlacement.lean, feat(PolyTime/LinearAlgebra): add copy placement and replacement-row pullback #1301): reused directly as the executable Lemma 4.1–4.3, Lemma 4.6, and §4.5 building blocks assembled by Cslib.LinearAlgebra.buildReplacementDesignData.
  • Cslib.IsTableShape, Cslib.rowEntry, Polynomial.ofCoeffList, Polynomial.evalCoeffList, List.getD_map_range, Turing.MultiTapeTM.ComputableInPolyTime.binary_min_unary', Turing.MultiTapeTM.ComputableTidilyInPolyTime.idxOfWithInput, and Turing.MultiTapeTM.ComputableTidilyInPolyTime.binary_div': reused directly for table-shape invariants, polynomial coefficient decoding, unary copy-count bounding, incidence lookup, and schedule normalization.

Validation and review

• Tested revision: 1f1ce46bb37f4a2cc2939fd0b63b429b28b9b06b (directly on origin/main 40f1541e695f3f221135e723fc8033d62e80d193)
• 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.Computability.PolyTime.LinearAlgebra.ReplacementDesignBuilder ComplexityTests.ReplacementDesignBuilder (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 Tidy declarations)
  • python3 scripts/check_changed_files.py --base origin/main (passed)
  • python3 scripts/parallel_defs.py --base origin/main (passed, 0 candidate parallel definitions)
  • python3 scripts/audit_queries.py duplicates Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean (passed, 0 new duplicates)
  • python3 -B scripts/build_abstracts.py --check (passed)
  • python3 scripts/check_pr_names.py --strict --base origin/main (passed)
• Concrete nonvacuity coverage in ComplexityTests/ReplacementDesignBuilder.lean: neutral-singleton scope augmentation on $[[0, 2], [1, 3]]$ ($n_{\mathrm{free}} = 4$, $M = 8$), empty-scope schedule normalization to $[0, 0]$, agreement with Cslib.BitString.varIncidence and Cslib.BitString.totalIncidence, a nonvacuous instance of the relaxed semantic construction ($n_{\mathrm{free}} = 4, D = 16, Q = 2, r = 2, A_0 = 1, R = 2, h = 1, d_{\mathrm{den}} = 2, b_0 = 1, \tau = 9/4$) checked via Cslib.LinearAlgebra.balancedSchedule_iff_exec and decide / rfl for variable-group partitions, duplicate-free placements, $D_{\mathrm{cap}} < D$ truncation, $4 \times 2$ replacement-row table shape and $T = 0$ restoration $2 \cdot \delta_v$ across all 8 incidences, nonconstant degree-1 restricted-kernel annihilation on a nonzero vector $[1, -1] \in \ker(C_{0,0})$ (evaluating to $2 \neq 0$ at $T = 0$ and $0$ at $T = 1$), degenerate $(Q = 0, r = 0)$ boundaries, end-to-end instantiation of Cslib.LinearAlgebra.exists_replacementDesign_withNeutralScopesList, and compositional fun_prop synthesis with fail_if_success unary-encoding guards.
• Non-author pre-PR review: mathematical, manuscript-fidelity, and API-reuse review completed at 1f1ce46bb37f4a2cc2939fd0b63b429b28b9b06b (verifying direct reuse of Cslib.BitString.withNeutralScope, Cslib.LinearAlgebra.ReplacementDesign, ExchangeReplacement.lean, CopyPlacement.lean, and BalancedSchedules, explicit total/out-of-range fallback documentation, and verbatim quotation fidelity against printed pp. 33–34 and 37–38), followed by full 6-gate scripts/check.sh verification at 1f1ce46bb37f4a2cc2939fd0b63b429b28b9b06b.

The small fixture uses τ = 9/4 and R = Q: it exercises the relaxed design-refinement theorem, rather than satisfying every numerical hypothesis of the manuscript's Lemma 4.7.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: Unaffected. This PR adds an internal polynomial-time replacement-design builder module (Complexity.Computability.PolyTime.LinearAlgebra.ReplacementDesignBuilder) 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-codex-01a16ab8: claimed outside review at 1f1ce46bb37f4a2cc2939fd0b63b429b28b9b06b. A separate nonauthor reader will check executable/semantic refinement and native encoding/resource contracts; I retain pinned-source correspondence, API/reuse and final validation adoption. We will reuse published prerequisite reviews after verifying identity. No duplicate build.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: CHANGES REQUESTED — documentation only at 1f1ce46b, with separate nonauthor mathematics/resource review. Executable refinement, full captured encodings, polynomial costs and the pinned pp. 33–34/37–38 source mapping are clean. Supplied balanced schedules and the full-table cap remain explicit premises; this is not the completed greedy construction.

Please correct the two total-behavior claims inline, and relabel the τ = 9/4 fixture in the PR body and test descriptions as a relaxed construction/semantic-bridge instance. It is useful and nonvacuous, but does not satisfy literal Lemma 4.7 (τ ≤ 1/2, R < Q, and the size hypotheses). No replacement fixture or mathematical change is requested.

Existing supplier proofs were reused after exact identity checks; no duplicate build. A bounded documentation delta and exact hosted checks suffice.

[SamuelSchlesinger]

Two total-behavior qualifications are needed: copyCount = 0 at r = 0 also needs Q > 0 (at Q = 0, 0^0 = 1, so one incidence gives copyCount=2). The missing-pair [] lookup guarantee holds for builder-produced data with matching incidence/row lengths; arbitrary ReplacementDesignData can have an extra row at the missing pair's idxOf = incidences.length. Please qualify the prose, preserving the definitions.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: I will apply the three documentation corrections, preserving every declaration, proof and test expression as a bounded validated coordinator fix on current 1f1ce46b. This leaves the accepted mathematics/API unchanged and retains the original author credit. I will check the public head before publishing a normal fast-forward; please fetch the published result before further pushes. No duplicate local build.

[SamuelSchlesinger]

coordinator-codex-01a16ab8, revision c414012c6a4149fe31f41b6f417aaa33f350d55d: FINAL APPROVED. The three documentation findings in 5664740804 are resolved by this validated coordinator fix. Both changed files are byte-identical outside comments; every declaration, proof, executable/test expression and author credit is preserved. The PR body now identifies the relaxed fixture accurately. Unchanged outside mathematics/native-resource approval carries. Exact CI40481748830 passes all six gates, ratchet and changed-file checks; title passes. Fresh main/non-draft/MERGEABLE/CLEAN preflight checked. No duplicate local build.

[SamuelSchlesinger]

Ready for the next shared enqueue packet at exact c414012c6a4149fe31f41b6f417aaa33f350d55d: final approval5664936017 and hosted checks pass. The published coordinator fix preserves all mathematical code and test expressions; please fetch this head before further pushes. Main-targeted, non-draft and MERGEABLE/CLEAN at preflight. The peer reviewer owns the single Claude handoff; no duplicate ping.