Instantiating cleared parity-polynomial specialization with Section 4 replacement designs

This module connects the Section 4 algebraic replacement design construction (Complexity.Foundations.LinearAlgebra.ReplacementDesign) directly to the Section 5.3–5.5 and Appendix B.2–B.3 cleared-denominator parity-polynomial zero-counting pipeline (Complexity.Foundations.BooleanAnalysis.SparseClearedSpecialization) of OpenAI, The Exponential Time Hypothesis is False (printed pp. 32–34, 37–39, 48–50):

1. Neutral singleton scope augmentation (§5.3 & §5.5, pp. 37–38): Reusing withNeutralFactors and withNeutralScope from Complexity.Foundations.BooleanAnalysis.SparseBranching on scope = fun i => equationScope (P i) adjoins one singleton scope {v} (Sum.inr v) per variable v : Fin n to the equation scopes equationScope (P i) (Sum.inl i). Combined with totalIncidence_withNeutralFactors (M = (∑ i, #(equationScope (P i))) + n ≥ n) and varIncidence_withNeutralFactors_le (varIncidence ≤ b₀ + 1), we prove card_withNeutralScope_le, totalIncidence_withNeutralFactors_le, and exists_replacementDesign_withNeutralScope: Lemma 4.7 (exists_replacementDesign) applies to withNeutralScope (fun i => equationScope (P i)) whenever equation variable occurrences are bounded by b₀, equation scopes have size at most w ≥ 1, and the numerical balance (2 * (b₀ + 1 + w) * (r ^ (2 * Q)) ^ 2 ≤ (∑ i, #(equationScope (P i))) + n, 2 * Q * r ^ 2 ≤ n), interval (∀ a < R - 1, A₀ + a ≤ Q), and binomial-tail (binomTailProb Q r A₀ R ≤ τ / (r * (b₀ + 1))) hypotheses hold for b = b₀ + 1.

2. Univariate polynomial replacement rows from a ReplacementDesign (§5.3–5.4, pp. 37–38): For any D : ReplacementDesign scope Q r A₀ R τ, incidence e : ScopeIncidence scope, and Boolean assignment x : Fin n → Bool, evalVarReplacementRowPoly D e x : ℚ[X] and its scaled integer counterpart evalVarReplacementRowScaledIntPoly D e x : ℤ[X] evaluate D's replacement rows on the {0, 1} vector fun u => bitVal _ (x u). Using D's fields from Definition 3.1 and Lemma 4.6, we prove:

   • (evalVarReplacementRowScaledIntPoly D e x).map (Int.castRingHom ℚ) = C (commonDenom Q R : ℚ) * evalVarReplacementRowPoly D e x,
   • (evalVarReplacementRowPoly D e x).eval 0 = bitVal ℚ (x (scopeVarOf scope e)) and (evalVarReplacementRowScaledIntPoly D e x).eval 0 = (commonDenom Q R : ℤ) * bitVal ℤ (x (scopeVarOf scope e)),
   • natDegree ≤ R - 1 for both polynomials,
   • (evalVarReplacementRowScaledIntPoly D e x).coeffNorm1 ≤ designRowNormBound Q R, where designRowNormBound Q R = commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (4 * Q) ^ (R - 1)), and
   • at each evaluation node nodePoint t (t : Fin Q), (evalVarReplacementRowPoly D e x).eval (nodePoint t) depends only on x restricted to the assigned variable group varGroup D.varAssign t (D.factorAssign (scopeFactorOf scope e) t) and the full measurement vector (varMeasurementMatrix Q r A₀ R ℚ D.place (scopeVarOf scope)).mulVec (fun u => bitVal ℚ (x u)).

3. Concrete §5.3–5.5 degree, locality, norm, and exact modular zero-counting theorems: Packaging these replacement rows into designReplacementMap D emb and designReplacementScaledIntMap D emb (for any factor embedding emb : κ → F, falling back to the constant Boolean value outside scope (emb i)) discharges all clearing, degree, $T = 0$ evaluation, and coeffNorm1 premises of SparseClearedSpecialization unconditionally, and preserves node-point group-and-measurement locality on covered scopes (eval_nodePoint_designReplacementMap_eq_of_eq_on_varGroup, eval_univariateMonomialSumPoly_designReplacementMap_nodePoint_eq). This yields concrete ReplacementDesign specializations of:

   • the equation (5.5) degree bound (k * (R - 1)) * (#I + 2 * (ℓ - 1)) (strengthening the manuscript's coarser k * R * (#I + 2 * (ℓ - 1)) display on p. 37 using natDegree ≤ R - 1 from Lemma 4.3 and its variable-row transfer in §4.5 (4.14); natDegree_univariateClearedParityCoord_design_le, natDegree_univariateClearedParityTruncatedSum_design_le),
   • the rational homogenization identity $\tilde{H}_s(T) = \Omega [V^s] H(T)$ over ℚ[X] (map_univariateClearedParityCoord_design),
   • the Appendix B.2 coordinate ℓ₁-norm bound (coeffNorm1_univariateClearedParityCoord_design_le),
   • exact integer division and modulo-2 ^ ℓ recovery of commonZeroCount I P when n < ℓ and ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k, including Cramer's rule determinant recovery (under D_H ≠ 0 and the Cramer numerator identity hcramer : ∀ s ∈ range ℓ, N_H s = D_H * (univariateClearedParityCoord ... s).eval 0) and §5.5 heavy-variable branch summation at shared precision branchPrecision n = n + 1 (emod_sum_ediv_eval_zero_clearedParityCoord_design_eq_commonZeroCount, emod_ediv_eval_zero_clearedParityTruncatedSum_design_eq_commonZeroCount, emod_sum_cramer_ediv_design_eq_commonZeroCount, commonZeroCount_eq_sum_branch_emod_ediv_design).

Main definitions

• Cslib.BitString.designRowNormBound: the Lemma 4.6 row ℓ₁-norm bound commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (4 * Q) ^ (R - 1)).
• Cslib.BitString.evalVarReplacementRowPoly, Cslib.BitString.evalVarReplacementRowScaledIntPoly: univariate rational and scaled integer replacement polynomials evaluated on a Boolean assignment x : Fin n → Bool.
• Cslib.BitString.designReplacementMap, Cslib.BitString.designReplacementScaledIntMap: equation-indexed rational and scaled integer replacement polynomial families associated to a ReplacementDesign.

Main results

• Cslib.BitString.card_withNeutralScope_le, Cslib.BitString.totalIncidence_withNeutralFactors_le, Cslib.BitString.exists_replacementDesign_withNeutralScope: scope-width bound, total-incidence upper bound, and Lemma 4.7 existence for withNeutralScope.
• Cslib.BitString.map_evalVarReplacementRowScaledIntPoly, Cslib.BitString.eval_zero_evalVarReplacementRowPoly, Cslib.BitString.eval_zero_evalVarReplacementRowScaledIntPoly, Cslib.BitString.natDegree_evalVarReplacementRowScaledIntPoly_le, Cslib.BitString.coeffNorm1_evalVarReplacementRowScaledIntPoly_le, Cslib.BitString.eval_evalVarReplacementRowPoly_nodePoint_eq_of_eq_on_varGroup, Cslib.BitString.eval_nodePoint_designReplacementMap_eq_of_eq_on_varGroup, Cslib.BitString.eval_univariateMonomialSumPoly_designReplacementMap_nodePoint_eq: Definition 3.1 and Lemma 4.6 properties of evalVarReplacementRowPoly, evalVarReplacementRowScaledIntPoly, and designReplacementMap.
• Cslib.BitString.natDegree_univariateClearedParityCoord_design_le, Cslib.BitString.natDegree_univariateClearedParityTruncatedSum_design_le, Cslib.BitString.map_univariateClearedParityCoord_design, Cslib.BitString.coeffNorm1_univariateClearedParityCoord_design_le: concrete ReplacementDesign degree, homogenization, and ℓ₁-norm bounds.
• Cslib.BitString.emod_sum_ediv_eval_zero_clearedParityCoord_design_eq_commonZeroCount, Cslib.BitString.emod_ediv_eval_zero_clearedParityTruncatedSum_design_eq_commonZeroCount, Cslib.BitString.emod_sum_cramer_ediv_design_eq_commonZeroCount, Cslib.BitString.commonZeroCount_eq_sum_branch_emod_ediv_design: exact integer division recovery of commonZeroCount from ReplacementDesigns on a single system and summed across heavy-variable branches.

References

• OpenAI, The Exponential Time Hypothesis is False (Sections 4.5–4.6, 5.3–5.5, and Appendix B.2–B.3, pp. 32–34, 37–39, 48–50)

1. Neutral singleton scope augmentation via withNeutralScope (§5.3 & §5.5, pp. 37–38)

@[simp]

theorem Cslib.BitString.withNeutralFactors_univ {κ : Type u_1} [Fintype κ] {ι' : Type u_2} [Fintype ι'] : withNeutralFactors Finset.univ = Finset.univ

withNeutralFactors (univ : Finset κ) is (univ : Finset (κ ⊕ ι')).

theorem Cslib.BitString.card_withNeutralScope_le {κ : Type u_1} {ι' : Type u_2} {scope : κ → Finset ι'} {w : ℕ} (hw1 : 1 ≤ w) (hw : ∀ (i : κ), (scope i).card ≤ w) (f : κ ⊕ ι') : (withNeutralScope scope f).card ≤ w

If 1 ≤ w and every scope scope i has size at most w, then every scope in withNeutralScope scope has size at most w.

theorem Cslib.BitString.totalIncidence_withNeutralFactors_le {κ : Type u_1} {ι' : Type u_2} [Fintype ι'] [DecidableEq ι'] {I : Finset κ} {scope : κ → Finset ι'} {b₀ : ℕ} (hb : ∀ (v : ι'), varIncidence I scope v ≤ b₀) : totalIncidence (withNeutralFactors I) (withNeutralScope scope) ≤ (b₀ + 1) * Fintype.card ι'

If every variable v : ι' has varIncidence I scope v ≤ b₀, then the total incidence after adjoining neutral singleton scopes is at most (b₀ + 1) * Fintype.card ι'.

theorem Cslib.BitString.exists_replacementDesign_withNeutralScope {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} [Fintype κ] (scope : κ → Finset (Fin n)) {b₀ w : ℕ} (hn : 1 ≤ n) (hw_pos : 1 ≤ w) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ : 0 ≤ τ) (hI : ∀ a < R - 1, A₀ + a ≤ Q) (hb : ∀ (v : Fin n), varIncidence Finset.univ scope v ≤ b₀) (hw : ∀ (i : κ), (scope i).card ≤ w) (hincidenceSize : 2 * (b₀ + 1 + w) * (r ^ (2 * Q)) ^ 2 ≤ totalIncidence Finset.univ scope + n) (hgroupSize : 2 * Q * r ^ 2 ≤ n) (htail : LinearAlgebra.binomTailProb Q r A₀ R ≤ τ / (↑r * ↑(b₀ + 1))) : Nonempty (LinearAlgebra.ReplacementDesign (withNeutralScope scope) Q r A₀ R τ)

Lemma 4.7 for neutral-singleton augmented scopes (withNeutralScope, §5.5, pp. 38–39): when every variable belongs to at most b₀ scopes of scope : κ → Finset (Fin n) and every scope i has size at most w (1 ≤ w), the augmented scope family withNeutralScope scope satisfies 1 ≤ b₀ + 1 and M ≤ (b₀ + 1) * n automatically, and admits a Section 4 ReplacementDesign under the numerical balance (2 * (b₀ + 1 + w) * (r ^ (2 * Q)) ^ 2 ≤ totalIncidence univ scope + n, 2 * Q * r ^ 2 ≤ n), interval (∀ a < R - 1, A₀ + a ≤ Q), and binomial-tail (binomTailProb Q r A₀ R ≤ τ / (r * (b₀ + 1))) hypotheses for b = b₀ + 1.

2. Univariate replacement polynomials from a ReplacementDesign (§5.3–5.4, pp. 37–38)

def Cslib.BitString.designRowNormBound (Q R : ℕ) : ℕ

The explicit Lemma 4.6 ℓ₁ coefficient norm bound commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (4 * Q) ^ (R - 1)) for scaled integer replacement rows (printed p. 33).

theorem Cslib.BitString.commonDenom_le_designRowNormBound (Q R : ℕ) : LinearAlgebra.commonDenom Q R ≤ designRowNormBound Q R

commonDenom Q R ≤ designRowNormBound Q R.

theorem Cslib.BitString.designRowNormBound_pos (Q R : ℕ) : 0 < designRowNormBound Q R

0 < designRowNormBound Q R.

theorem Cslib.BitString.commonDenom_intCast_ne_zero (Q R : ℕ) : ↑(LinearAlgebra.commonDenom Q R) ≠ 0

(commonDenom Q R : ℤ) ≠ 0.

noncomputable def Cslib.BitString.evalVarReplacementRowPoly {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (x : Fin n → Bool) : Polynomial ℚ

The univariate rational replacement polynomial ⟨P⃗_e(T), x⟩ ∈ ℚ[X] for incidence e : ScopeIncidence scope and Boolean assignment x : Fin n → Bool (§5.3, p. 37).

noncomputable def Cslib.BitString.evalVarReplacementRowScaledIntPoly {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (x : Fin n → Bool) : Polynomial ℤ

The univariate scaled integer replacement polynomial d_den · ⟨P⃗_e(T), x⟩ ∈ ℤ[X] for incidence e : ScopeIncidence scope and Boolean assignment x : Fin n → Bool (§5.4 & Lemma 4.6, pp. 33, 37–38).

theorem Cslib.BitString.eval_evalVarReplacementRowPoly {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (x : Fin n → Bool) (t : ℚ) : Polynomial.eval t (evalVarReplacementRowPoly D e x) = LinearAlgebra.evalVarReplacementRow Q r A₀ R D.place (BalancedSchedules.scopeVarOf scope) e t fun (u : Fin n) => bitVal ℚ (x u)

Evaluating evalVarReplacementRowPoly D e x at t : ℚ agrees with evalVarReplacementRow Q r A₀ R D.place (scopeVarOf scope) e t (fun u => bitVal ℚ (x u)).

theorem Cslib.BitString.eval_zero_evalVarReplacementRowPoly {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (x : Fin n → Bool) : Polynomial.eval 0 (evalVarReplacementRowPoly D e x) = bitVal ℚ (x (BalancedSchedules.scopeVarOf scope e))

At T = 0, evalVarReplacementRowPoly D e x evaluates to bitVal ℚ (x (scopeVarOf scope e)) (Definition 3.1 (4), p. 22).

theorem Cslib.BitString.map_evalVarReplacementRowScaledIntPoly {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (x : Fin n → Bool) : Polynomial.map (Int.castRingHom ℚ) (evalVarReplacementRowScaledIntPoly D e x) = Polynomial.C ↑(LinearAlgebra.commonDenom Q R) * evalVarReplacementRowPoly D e x

Mapping evalVarReplacementRowScaledIntPoly D e x into ℚ[X] yields C (commonDenom Q R : ℚ) * evalVarReplacementRowPoly D e x (Definition 3.1 (5) & Lemma 4.6).

theorem Cslib.BitString.eval_zero_evalVarReplacementRowScaledIntPoly {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (x : Fin n → Bool) : Polynomial.eval 0 (evalVarReplacementRowScaledIntPoly D e x) = ↑(LinearAlgebra.commonDenom Q R) * bitVal ℤ (x (BalancedSchedules.scopeVarOf scope e))

At T = 0, evalVarReplacementRowScaledIntPoly D e x evaluates to (commonDenom Q R : ℤ) * bitVal ℤ (x (scopeVarOf scope e)).

theorem Cslib.BitString.natDegree_evalVarReplacementRowPoly_le {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (x : Fin n → Bool) : (evalVarReplacementRowPoly D e x).natDegree ≤ R - 1

evalVarReplacementRowPoly D e x has natDegree ≤ R - 1 by Lemma 4.3 and its variable-row transfer in §4.5 (4.14).

theorem Cslib.BitString.natDegree_evalVarReplacementRowScaledIntPoly_le {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (x : Fin n → Bool) : (evalVarReplacementRowScaledIntPoly D e x).natDegree ≤ R - 1

evalVarReplacementRowScaledIntPoly D e x has natDegree ≤ R - 1.

theorem Cslib.BitString.coeffNorm1_evalVarReplacementRowScaledIntPoly_le {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (x : Fin n → Bool) : (evalVarReplacementRowScaledIntPoly D e x).coeffNorm1 ≤ designRowNormBound Q R

Lemma 4.6 row ℓ₁-norm bound on Boolean inputs: (evalVarReplacementRowScaledIntPoly D e x).coeffNorm1 ≤ designRowNormBound Q R.

theorem Cslib.BitString.eval_evalVarReplacementRowPoly_nodePoint_eq_of_eq_on_varGroup {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (t : Fin Q) (x x' : Fin n → Bool) (hgrp : ∀ u ∈ LinearAlgebra.varGroup D.varAssign t (D.factorAssign (BalancedSchedules.scopeFactorOf scope e) t), x u = x' u) (hmeas : ((LinearAlgebra.varMeasurementMatrix Q r A₀ R ℚ D.place (BalancedSchedules.scopeVarOf scope)).mulVec fun (u : Fin n) => bitVal ℚ (x u)) = (LinearAlgebra.varMeasurementMatrix Q r A₀ R ℚ D.place (BalancedSchedules.scopeVarOf scope)).mulVec fun (u : Fin n) => bitVal ℚ (x' u)) : Polynomial.eval (LinearAlgebra.nodePoint t) (evalVarReplacementRowPoly D e x) = Polynomial.eval (LinearAlgebra.nodePoint t) (evalVarReplacementRowPoly D e x')

Definition 3.1 (4) group-and-measurement locality at nodePoint t: at t : Fin Q, (evalVarReplacementRowPoly D e x).eval (nodePoint t) depends only on x restricted to varGroup D.varAssign t (D.factorAssign (scopeFactorOf scope e) t) and the measurement vector (varMeasurementMatrix Q r A₀ R ℚ D.place (scopeVarOf scope)).mulVec (fun u => bitVal ℚ (x u)).

3. Factor-indexed replacement families designReplacementMap and

designReplacementScaledIntMap (§5.3–5.4)

noncomputable def Cslib.BitString.designReplacementMap {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (x : Fin n → Bool) (i : κ) (v : Fin n) : Polynomial ℚ

The equation-indexed rational replacement family (Fin n → Bool) → κ → Fin n → ℚ[X] associated to a ReplacementDesign and factor embedding emb : κ → F, using evalVarReplacementRowPoly D ⟨emb i, ⟨v, hv⟩⟩ x for v ∈ scope (emb i) and the constant Boolean value C (bitVal ℚ (x v)) outside scope (emb i).

noncomputable def Cslib.BitString.designReplacementScaledIntMap {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (x : Fin n → Bool) (i : κ) (v : Fin n) : Polynomial ℤ

The equation-indexed scaled integer replacement family (Fin n → Bool) → κ → Fin n → ℤ[X] associated to a ReplacementDesign and factor embedding emb : κ → F, using evalVarReplacementRowScaledIntPoly D ⟨emb i, ⟨v, hv⟩⟩ x for v ∈ scope (emb i) and C ((commonDenom Q R : ℤ) * bitVal ℤ (x v)) outside scope (emb i).

theorem Cslib.BitString.designReplacementMap_of_mem {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (x : Fin n → Bool) {i : κ} {v : Fin n} (hv : v ∈ scope (emb i)) : designReplacementMap D emb x i v = evalVarReplacementRowPoly D ⟨emb i, ⟨v, hv⟩⟩ x

On hv : v ∈ scope (emb i), designReplacementMap D emb x i v is evalVarReplacementRowPoly D ⟨emb i, ⟨v, hv⟩⟩ x.

theorem Cslib.BitString.designReplacementScaledIntMap_of_mem {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (x : Fin n → Bool) {i : κ} {v : Fin n} (hv : v ∈ scope (emb i)) : designReplacementScaledIntMap D emb x i v = evalVarReplacementRowScaledIntPoly D ⟨emb i, ⟨v, hv⟩⟩ x

On hv : v ∈ scope (emb i), designReplacementScaledIntMap D emb x i v is evalVarReplacementRowScaledIntPoly D ⟨emb i, ⟨v, hv⟩⟩ x.

theorem Cslib.BitString.eval_nodePoint_designReplacementMap_eq_of_eq_on_varGroup {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) {i : κ} {v : Fin n} (hv : v ∈ scope (emb i)) (t : Fin Q) (x x' : Fin n → Bool) (hgrp : ∀ u ∈ LinearAlgebra.varGroup D.varAssign t (D.factorAssign (emb i) t), x u = x' u) (hmeas : ((LinearAlgebra.varMeasurementMatrix Q r A₀ R ℚ D.place (BalancedSchedules.scopeVarOf scope)).mulVec fun (u : Fin n) => bitVal ℚ (x u)) = (LinearAlgebra.varMeasurementMatrix Q r A₀ R ℚ D.place (BalancedSchedules.scopeVarOf scope)).mulVec fun (u : Fin n) => bitVal ℚ (x' u)) : Polynomial.eval (LinearAlgebra.nodePoint t) (designReplacementMap D emb x i v) = Polynomial.eval (LinearAlgebra.nodePoint t) (designReplacementMap D emb x' i v)

Definition 3.1 (4) scoped variable-level locality for designReplacementMap: when hv : v ∈ scope (emb i), (designReplacementMap D emb x i v).eval (nodePoint t) depends only on x restricted to varGroup D.varAssign t (D.factorAssign (emb i) t) and the full measurement vector (varMeasurementMatrix Q r A₀ R ℚ D.place (scopeVarOf scope)).mulVec (fun u => bitVal ℚ (x u)).

theorem Cslib.BitString.eval_univariateMonomialSumPoly_designReplacementMap_nodePoint_eq {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (P : κ → Finset (Finset (Fin n))) {i : κ} (hscope : equationScope (P i) ⊆ scope (emb i)) (t : Fin Q) (x x' : Fin n → Bool) (hgrp : ∀ u ∈ LinearAlgebra.varGroup D.varAssign t (D.factorAssign (emb i) t), x u = x' u) (hmeas : ((LinearAlgebra.varMeasurementMatrix Q r A₀ R ℚ D.place (BalancedSchedules.scopeVarOf scope)).mulVec fun (u : Fin n) => bitVal ℚ (x u)) = (LinearAlgebra.varMeasurementMatrix Q r A₀ R ℚ D.place (BalancedSchedules.scopeVarOf scope)).mulVec fun (u : Fin n) => bitVal ℚ (x' u)) : Polynomial.eval (LinearAlgebra.nodePoint t) (univariateMonomialSumPoly ℚ (designReplacementMap D emb x i) (P i)) = Polynomial.eval (LinearAlgebra.nodePoint t) (univariateMonomialSumPoly ℚ (designReplacementMap D emb x' i) (P i))

Definition 3.1 (4) & §5.3 factor-level locality for univariateMonomialSumPoly under scope coverage: when equationScope (P i) ⊆ scope (emb i) (for instance when scope = withNeutralScope (fun j => equationScope (P j)) and emb = Sum.inl), the substituted equation factor (univariateMonomialSumPoly ℚ (designReplacementMap D emb x i) (P i)).eval (nodePoint t) depends only on x restricted to varGroup D.varAssign t (D.factorAssign (emb i) t) and the full measurement vector (varMeasurementMatrix Q r A₀ R ℚ D.place (scopeVarOf scope)).mulVec (fun u => bitVal ℚ (x u)).

theorem Cslib.BitString.map_designReplacementScaledIntMap {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (x : Fin n → Bool) (i : κ) (v : Fin n) : Polynomial.map (Int.castRingHom ℚ) (designReplacementScaledIntMap D emb x i v) = Polynomial.C ↑(LinearAlgebra.commonDenom Q R) * designReplacementMap D emb x i v

Mapping designReplacementScaledIntMap D emb x i v into ℚ[X] yields C (commonDenom Q R : ℚ) * designReplacementMap D emb x i v.

theorem Cslib.BitString.eval_zero_designReplacementMap {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (x : Fin n → Bool) (i : κ) (v : Fin n) : Polynomial.eval 0 (designReplacementMap D emb x i v) = bitVal ℚ (x v)

At T = 0, designReplacementMap D emb x i v evaluates to bitVal ℚ (x v).

theorem Cslib.BitString.eval_zero_designReplacementScaledIntMap {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (x : Fin n → Bool) (i : κ) (v : Fin n) : Polynomial.eval 0 (designReplacementScaledIntMap D emb x i v) = ↑(LinearAlgebra.commonDenom Q R) * bitVal ℤ (x v)

At T = 0, designReplacementScaledIntMap D emb x i v evaluates to (commonDenom Q R : ℤ) * bitVal ℤ (x v).

theorem Cslib.BitString.natDegree_designReplacementMap_le {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (x : Fin n → Bool) (i : κ) (v : Fin n) : (designReplacementMap D emb x i v).natDegree ≤ R - 1

designReplacementMap D emb x i v has natDegree ≤ R - 1.

theorem Cslib.BitString.natDegree_designReplacementScaledIntMap_le {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (x : Fin n → Bool) (i : κ) (v : Fin n) : (designReplacementScaledIntMap D emb x i v).natDegree ≤ R - 1

designReplacementScaledIntMap D emb x i v has natDegree ≤ R - 1.

theorem Cslib.BitString.coeffNorm1_designReplacementScaledIntMap_le {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (x : Fin n → Bool) (i : κ) (v : Fin n) : (designReplacementScaledIntMap D emb x i v).coeffNorm1 ≤ designRowNormBound Q R

(designReplacementScaledIntMap D emb x i v).coeffNorm1 ≤ designRowNormBound Q R.

theorem Cslib.BitString.coeffNorm1_clearedMonomialSumPoly_designReplacementScaledIntMap_le {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (P : κ → Finset (Finset (Fin n))) (x : Fin n → Bool) {i : κ} {k : ℕ} (hk : ∀ M ∈ P i, M.card ≤ k) : (clearedMonomialSumPoly (↑(LinearAlgebra.commonDenom Q R)) k (designReplacementScaledIntMap D emb x i) (P i)).coeffNorm1 ≤ (P i).card * designRowNormBound Q R ^ k

Appendix B.2 Stage-1 ℓ₁-norm bound for designReplacementScaledIntMap: if every monomial M ∈ P i has #M ≤ k, then clearedMonomialSumPoly (commonDenom Q R : ℤ) k (designReplacementScaledIntMap D emb x i) (P i) has coeffNorm1 ≤ #(P i) * designRowNormBound Q R ^ k.

4. Concrete §5.3–5.5 degree, homogenization, ℓ₁-norm, and exact division recovery

theorems for ReplacementDesign

theorem Cslib.BitString.natDegree_univariateClearedParityCoord_design_le {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (I : Finset κ) (P : κ → Finset (Finset (Fin n))) {k ℓ s : ℕ} (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hs : s < ℓ) : (univariateClearedParityCoord I P (↑(LinearAlgebra.commonDenom Q R)) k ℓ (designReplacementScaledIntMap D emb) s).natDegree ≤ k * (R - 1) * (I.card + 2 * (ℓ - 1))

Equation (5.5) coordinate natDegree bound for ReplacementDesign (p. 37): for s < ℓ and ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k, the cleared coordinate polynomial univariateClearedParityCoord I P (commonDenom Q R : ℤ) k ℓ (designReplacementScaledIntMap D emb) s has natDegree ≤ (k * (R - 1)) * (#I + 2 * (ℓ - 1)) (strengthening the manuscript's coarser k * R * (#I + 2 * (ℓ - 1)) display in (5.5) via natDegree ≤ R - 1 from Lemma 4.3 and its variable-row transfer in §4.5 (4.14)).

theorem Cslib.BitString.natDegree_univariateClearedParityTruncatedSum_design_le {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (I : Finset κ) (P : κ → Finset (Finset (Fin n))) (k ℓ : ℕ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) : (univariateClearedParityTruncatedSum I P (↑(LinearAlgebra.commonDenom Q R)) k ℓ (designReplacementScaledIntMap D emb)).natDegree ≤ k * (R - 1) * (I.card + 2 * (ℓ - 1))

Equation (5.5) truncated-sum natDegree bound for ReplacementDesign (p. 37): when ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k, the cleared truncated sum univariateClearedParityTruncatedSum I P (commonDenom Q R : ℤ) k ℓ (designReplacementScaledIntMap D emb) has natDegree ≤ (k * (R - 1)) * (#I + 2 * (ℓ - 1)) (strengthening the manuscript's coarser k * R * (#I + 2 * (ℓ - 1)) display in (5.5) via natDegree ≤ R - 1 from Lemma 4.3 and its variable-row transfer in §4.5 (4.14)).

theorem Cslib.BitString.map_univariateClearedParityCoord_design {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (I : Finset κ) (P : κ → Finset (Finset (Fin n))) {k ℓ : ℕ} (hℓ : 1 ≤ ℓ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (s : ℕ) : Polynomial.map (Int.castRingHom ℚ) (univariateClearedParityCoord I P (↑(LinearAlgebra.commonDenom Q R)) k ℓ (designReplacementScaledIntMap D emb) s) = Polynomial.C ↑(clearedProductDenom (↑(LinearAlgebra.commonDenom Q R)) k ℓ I.card) * univariateParityCoord I P ℓ (designReplacementMap D emb) s

§5.4 & Appendix B.3 ($\tilde{H}_s(T) = \Omega [V^s] H(T)$ over ℚ[X] for ReplacementDesign): for 1 ≤ ℓ and ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k, mapping univariateClearedParityCoord I P (commonDenom Q R : ℤ) k ℓ (designReplacementScaledIntMap D emb) s into ℚ[X] equals C (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I : ℚ) times univariateParityCoord I P ℓ (designReplacementMap D emb) s.

theorem Cslib.BitString.coeffNorm1_univariateClearedParityCoord_design_le {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (I : Finset κ) (P : κ → Finset (Finset (Fin n))) (k ℓ : ℕ) {S_mon E_ℓ : ℕ} (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hS : ∀ i ∈ I, (P i).card ≤ S_mon) (hE : ∀ j < ℓ, (Polynomial.parityBaseDigit ℓ j).coeffNorm1 ≤ E_ℓ) (s : ℕ) : (univariateClearedParityCoord I P (↑(LinearAlgebra.commonDenom Q R)) k ℓ (designReplacementScaledIntMap D emb) s).coeffNorm1 ≤ 2 ^ n * (ℓ * E_ℓ * (S_mon * designRowNormBound Q R ^ k + LinearAlgebra.commonDenom Q R ^ k) ^ (2 * ℓ - 1)) ^ I.card

Appendix B.2 coordinate ℓ₁-norm bound for ReplacementDesign: if ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k, ∀ i ∈ I, #(P i) ≤ S_mon, and ∀ j < ℓ, (parityBaseDigit ℓ j).coeffNorm1 ≤ E_ℓ, then every coordinate polynomial univariateClearedParityCoord I P (commonDenom Q R : ℤ) k ℓ (designReplacementScaledIntMap D emb) s has coeffNorm1 at most 2 ^ n * (ℓ * E_ℓ * (S_mon * designRowNormBound Q R ^ k + commonDenom Q R ^ k) ^ (2 * ℓ - 1)) ^ #I.

theorem Cslib.BitString.emod_sum_ediv_eval_zero_clearedParityCoord_design_eq_commonZeroCount {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (I : Finset κ) (P : κ → Finset (Finset (Fin n))) {k ℓ : ℕ} (hℓ : n < ℓ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) : (∑ s ∈ Finset.range ℓ, Polynomial.eval 0 (univariateClearedParityCoord I P (↑(LinearAlgebra.commonDenom Q R)) k ℓ (designReplacementScaledIntMap D emb) s) / clearedProductDenom (↑(LinearAlgebra.commonDenom Q R)) k ℓ I.card) % 2 ^ ℓ = ↑(commonZeroCount I P)

§5.4 & Appendix B.3 (exact modular recovery of commonZeroCount from coordinate quotients for ReplacementDesign): when n < ℓ and ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k, summing the exact integer quotients (univariateClearedParityCoord I P (commonDenom Q R : ℤ) k ℓ (designReplacementScaledIntMap D emb) s).eval 0 / clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I over s ∈ range ℓ and reducing modulo 2 ^ ℓ recovers commonZeroCount I P.

theorem Cslib.BitString.emod_ediv_eval_zero_clearedParityTruncatedSum_design_eq_commonZeroCount {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (I : Finset κ) (P : κ → Finset (Finset (Fin n))) {k ℓ : ℕ} (hℓ : n < ℓ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) : Polynomial.eval 0 (univariateClearedParityTruncatedSum I P (↑(LinearAlgebra.commonDenom Q R)) k ℓ (designReplacementScaledIntMap D emb)) / clearedProductDenom (↑(LinearAlgebra.commonDenom Q R)) k ℓ I.card % 2 ^ ℓ = ↑(commonZeroCount I P)

§5.4 & Appendix B.3 (exact modular recovery of commonZeroCount from $S_\ell(\tilde{H})(0) / \Omega$ for ReplacementDesign): under the same hypotheses, dividing (univariateClearedParityTruncatedSum I P (commonDenom Q R : ℤ) k ℓ (designReplacementScaledIntMap D emb)).eval 0 by clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I and reducing modulo 2 ^ ℓ recovers commonZeroCount I P.

theorem Cslib.BitString.emod_sum_cramer_ediv_design_eq_commonZeroCount {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {scope : F → Finset (Fin n)} (D : LinearAlgebra.ReplacementDesign scope Q r A₀ R τ) (emb : κ → F) (I : Finset κ) (P : κ → Finset (Finset (Fin n))) {D_H : ℤ} (hDH : D_H ≠ 0) {k ℓ : ℕ} (hℓ : n < ℓ) (N_H : ℕ → ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hcramer : ∀ s ∈ Finset.range ℓ, N_H s = D_H * Polynomial.eval 0 (univariateClearedParityCoord I P (↑(LinearAlgebra.commonDenom Q R)) k ℓ (designReplacementScaledIntMap D emb) s)) : (∑ s ∈ Finset.range ℓ, N_H s / (clearedProductDenom (↑(LinearAlgebra.commonDenom Q R)) k ℓ I.card * D_H)) % 2 ^ ℓ = ↑(commonZeroCount I P)

Appendix B.3 (eq. B.1, Cramer's rule determinant exact division recovery for ReplacementDesign): if D_H ≠ 0, n < ℓ, ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k, and N_H s = D_H * (univariateClearedParityCoord I P (commonDenom Q R : ℤ) k ℓ (designReplacementScaledIntMap D emb) s).eval 0 for all s ∈ range ℓ, then summing the exact integer quotients N_H s / (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * D_H) over s ∈ range ℓ and reducing modulo 2 ^ ℓ recovers commonZeroCount I P.

theorem Cslib.BitString.commonZeroCount_eq_sum_branch_emod_ediv_design {κ : Type u_1} {n Q r A₀ R : ℕ} {τ : ℚ} {F : Type u_2} [Fintype F] {n' : ℕ} (S : Finset (Fin n)) (e : ↥(Finset.univ \ S) ≃ Fin n') (I : Finset κ) (P : κ → Finset (Finset (Fin n))) {k : ℕ} (scope : (Fin n → Bool) → F → Finset (Fin n')) (D : (b : Fin n → Bool) → LinearAlgebra.ReplacementDesign (scope b) Q r A₀ R τ) (emb : (Fin n → Bool) → κ → F) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) : ↑(commonZeroCount I P) = ∑ b ∈ branchAssignments S, Polynomial.eval 0 (univariateClearedParityTruncatedSum I (fun (i : κ) => relabelRestrictedMonomials S e b (P i)) (↑(LinearAlgebra.commonDenom Q R)) k (branchPrecision n) (designReplacementScaledIntMap (D b) (emb b))) / clearedProductDenom (↑(LinearAlgebra.commonDenom Q R)) k (branchPrecision n) I.card % 2 ^ branchPrecision n

§5.5 & Appendix B.3 (branch-summed exact integer division recovery from per-branch ReplacementDesigns at shared precision $\ell = n + 1$): given a heavy-variable subset S : Finset (Fin n), a relabeling e : ↥(univ \ S) ≃ Fin n' of the free variables, and a per-branch ReplacementDesign family D : (Fin n → Bool) → ReplacementDesign (scope b) Q r A₀ R τ (with factor embeddings emb b : κ → F), summing the branch modular residues at shared precision branchPrecision n = n + 1 across b ∈ branchAssignments S recovers commonZeroCount I P.