Univariate parity-product specialization and heavy-variable branch reduction

This module completes the algebraic and combinatorial infrastructure of Sections 5.3 and 5.5 (Proof of Theorem 2.2) of OpenAI, The Exponential Time Hypothesis is False (pp. 37–39), building on Complexity.Foundations.BooleanAnalysis.SparseEquations and Complexity.Foundations.Data.Polynomial.ParityAmplifierDegree:

1. Univariate $H(T)$ and coordinatewise $H_s(T) = [V^s] H(T)$ specialization (§5.3, eq. 5.5): When each variable $v \in \iota$ in equation $i \in I$ is replaced by a univariate polynomial $q_{x, i, v}(T) \in R[T]$ of degree at most $R_{\mathrm{deg}}$ that restores the Boolean input $\mathrm{bitVal}(x_v)$ at $T = 0$, the substituted equation polynomial Cslib.BitString.univariateMonomialSumPoly has natDegree ≤ k * R_deg and evaluates to monomialSum R (P i) x at $T = 0$. Summing the parity-factor product over $x \in \{0, 1\}^\iota$ yields Cslib.BitString.univariateParityProduct, whose $V^s$-coordinate polynomials Cslib.BitString.univariateParityCoord ($s < \ell$) and truncated sum Cslib.BitString.univariateParityTruncatedSum have natDegree at most (k * R_deg) * (#I + 2 * (ℓ - 1)) (Cslib.BitString.natDegree_univariateParityCoord_le, Cslib.BitString.natDegree_univariateParityTruncatedSum_le). For integer-coefficient replacements q : (ι → Bool) → κ → ι → ℤ[X], evaluating at $T = 0$ is congruent to commonZeroCount I P modulo $2^\ell$ when 1 ≤ ℓ (Cslib.BitString.eval_zero_univariateParityTruncatedSum_modEq_commonZeroCount) and recovers commonZeroCount I P via (· % 2 ^ ℓ) when Fintype.card ι < ℓ (Cslib.BitString.emod_eval_zero_univariateParityTruncatedSum_eq_commonZeroCount). Note that generic-ring degree and evaluation transport over R[X] does not by itself close modular recovery for rational replacement rows ℚ[X]; bridging rational replacement rows with nonzero cleared denominators to integer modular recovery is a separate follow-up milestone (as in #1248).
2. Free-variable branch relabeling (§5.5, Proof of Theorem 2.2): After branching on a subset $S \subseteq \iota$ of heavy variables, every restricted equation restrictMonomials S b (P i) is supported on univ \ S. Transporting along an equivalence e : ↥(univ \ S) ≃ ι' (such as Fin n' with $n' = n - |S|$) via Cslib.BitString.relabelRestrictedMonomials preserves degree bounds #M ≤ k, never increases monomial counts, bounds every free variable's equation incidence by b₀ when $S$ is the heavy-variable set and ∀ i ∈ I, equationScope (P i) ⊆ V (Cslib.BitString.varIncidence_relabelRestrictedMonomials_heavyVars_le), and decomposes commonZeroCount I P additively as the sum of commonZeroCount on the relabeled free-variable cube ι' → Bool (Cslib.BitString.commonZeroCount_eq_sum_relabelRestrictedMonomials).
3. Neutral variable-coverage scopes and Theorem 2.2 threshold bounds (§5.5): Adjoining a singleton neutral scope {v} for each declared variable $v \in \iota'$ via Cslib.BitString.withNeutralFactors and Cslib.BitString.withNeutralScope increments each variable's incidence by 1, ensuring positive variable incidence (1 ≤ varIncidence), total incidence $M' \ge n'$ (Cslib.BitString.card_le_totalIncidence_withNeutralFactors), and light-variable incidence at most $b_0 + 1$. Finally, when 1 ≤ b₀, 1 ≤ s, ∀ i ∈ F, scope i ⊆ V, and totalIncidence F scope * s ≤ b₀ * #V (which holds both for the manuscript's threshold paperHeavyThreshold M n s = ⌈M / n⌉ * s and for the combined-ceiling variant heavyThreshold M n s = ⌈M * s / n⌉ when 1 ≤ n), the heavy-variable set has size at most #V / s, at most 2 ^ (Fintype.card ι / s) branches, and leaves #(V \ heavyVars V F scope b₀) ≥ #V - #V / s ≥ #V / 2 free variables when 2 ≤ s.

Main definitions

• Cslib.BitString.univariateMonomialPoly, Cslib.BitString.univariateMonomialSumPoly: univariate polynomial replacement in a monomial and a sparse polynomial equation.
• Cslib.BitString.univariateParityProduct, Cslib.BitString.univariateParityCoord, Cslib.BitString.univariateParityTruncatedSum: the cube-summed bivariate polynomial $H(T, V)$, its $V^s$-coordinate polynomials $[V^s] H(T)$, and its truncated sum $S_\ell(H(T))$.
• Cslib.BitString.relabelMonomials, Cslib.BitString.relabelRestrictedMonomials: relabeling monomial families and restricted branch equations onto a free-variable index type ι'.
• Cslib.BitString.withNeutralFactors, Cslib.BitString.withNeutralScope: adjoining neutral singleton scopes {v} for every variable $v \in \iota'$.
• Cslib.BitString.paperHeavyThreshold, Cslib.BitString.heavyThreshold: the manuscript's heavy-variable threshold $\lceil M / n \rceil s$ and the combined-ceiling variant $\lceil M s / n \rceil$.
• Cslib.BitString.branchPrecision: the shared modular precision $\ell = n + 1$ used across the unrestricted system and all free-variable branches.

Main results

• Cslib.BitString.natDegree_univariateParityCoord_le and Cslib.BitString.natDegree_univariateParityTruncatedSum_le: equation (5.5) degree bound $\deg_T \le (k R_{\mathrm{deg}})(m_{\mathrm{test}} + 2(\ell - 1))$.
• Cslib.BitString.eval_zero_univariateParityTruncatedSum_modEq_commonZeroCount and Cslib.BitString.emod_eval_zero_univariateParityTruncatedSum_eq_commonZeroCount: equation (5.5) congruence (for 1 ≤ ℓ) and exact recovery (for Fintype.card ι < ℓ) of commonZeroCount at $T = 0$ under integer-coefficient replacements.
• Cslib.BitString.commonZeroCount_eq_sum_relabelRestrictedMonomials: additive branch decomposition of commonZeroCount into commonZeroCount over the relabeled free-variable cube ι' → Bool.
• Cslib.BitString.varIncidence_relabelRestrictedMonomials_heavyVars_le: post-branching free-variable incidence bound $\le b_0$ on ι'.
• Cslib.BitString.card_le_totalIncidence_withNeutralFactors: neutral scopes guarantee $M' \ge n'$.
• Cslib.BitString.card_heavyVars_le_card_div and Cslib.BitString.card_sdiff_heavyVars_ge_half: $|S| \le n / s$ and $n' \ge n / 2$ for $s \ge 2$, $b_0 \ge 1$, and scope coverage.
• Cslib.BitString.commonZeroCount_eq_sum_branch_emod_eval_zero and Cslib.BitString.natDegree_univariateParityTruncatedSum_branch_le: §5.5 shared-precision $\ell = n + 1$ branch recovery and linear degree bound $\deg_T \le (k R_{\mathrm{deg}})((2 c + 4) n')$ when $m_{\mathrm{test}} \le c n$ and $n \le 2 n'$.

References

• OpenAI, The Exponential Time Hypothesis is False (Sections 5.3 and 5.5)

Section 1: Univariate replacement forms and degree / restoration lemmas (§5.3)

noncomputable def Cslib.BitString.univariateMonomialPoly {ι : Type u_1} (R : Type u_5) [CommSemiring R] (q : ι → Polynomial R) (M : Finset ι) : Polynomial R

Replacing each variable v ∈ M by a univariate polynomial q v : Polynomial R in a monomial M.

noncomputable def Cslib.BitString.univariateMonomialSumPoly {ι : Type u_1} (R : Type u_5) [CommSemiring R] (q : ι → Polynomial R) (𝓜 : Finset (Finset ι)) : Polynomial R

Replacing each variable v by q v : Polynomial R in a sparse polynomial 𝓜.

theorem Cslib.BitString.eval_univariateMonomialPoly {ι : Type u_1} {R : Type u_4} [CommSemiring R] (q : ι → Polynomial R) (M : Finset ι) (t : R) : Polynomial.eval t (univariateMonomialPoly R q M) = ∏ v ∈ M, Polynomial.eval t (q v)

Pointwise evaluation of univariateMonomialPoly R q M at t : R.

theorem Cslib.BitString.eval_univariateMonomialSumPoly {ι : Type u_1} {R : Type u_4} [CommSemiring R] (q : ι → Polynomial R) (𝓜 : Finset (Finset ι)) (t : R) : Polynomial.eval t (univariateMonomialSumPoly R q 𝓜) = ∑ M ∈ 𝓜, ∏ v ∈ M, Polynomial.eval t (q v)

Pointwise evaluation of univariateMonomialSumPoly R q 𝓜 at t : R.

theorem Cslib.BitString.eval_zero_univariateMonomialSumPoly {ι : Type u_1} {R : Type u_4} [CommRing R] {q : ι → Polynomial R} {𝓜 : Finset (Finset ι)} {x : ι → Bool} (hq0 : ∀ M ∈ 𝓜, ∀ v ∈ M, Polynomial.eval 0 (q v) = bitVal R (x v)) : Polynomial.eval 0 (univariateMonomialSumPoly R q 𝓜) = monomialSum R 𝓜 x

Restoration at T = 0: if every q v (v ∈ M) evaluates at 0 to bitVal R (x v), then univariateMonomialSumPoly R q 𝓜 evaluates at 0 to monomialSum R 𝓜 x.

theorem Cslib.BitString.natDegree_univariateMonomialPoly_le {ι : Type u_1} {R : Type u_4} [CommSemiring R] {q : ι → Polynomial R} {M : Finset ι} {k d₀ : ℕ} (hk : M.card ≤ k) (hd : ∀ v ∈ M, (q v).natDegree ≤ d₀) : (univariateMonomialPoly R q M).natDegree ≤ k * d₀

If #M ≤ k and every q v (v ∈ M) has natDegree ≤ d₀, then univariateMonomialPoly R q M has natDegree ≤ k * d₀.

theorem Cslib.BitString.natDegree_univariateMonomialSumPoly_le {ι : Type u_1} {R : Type u_4} [CommSemiring R] {q : ι → Polynomial R} {𝓜 : Finset (Finset ι)} {k d₀ : ℕ} (hk : ∀ M ∈ 𝓜, M.card ≤ k) (hd : ∀ M ∈ 𝓜, ∀ v ∈ M, (q v).natDegree ≤ d₀) : (univariateMonomialSumPoly R q 𝓜).natDegree ≤ k * d₀

If every monomial M ∈ 𝓜 has #M ≤ k and every q v has natDegree ≤ d₀, then univariateMonomialSumPoly R q 𝓜 has natDegree ≤ k * d₀.

Section 2: Cube-summed univariate polynomial $H(T)$ and equation (5.5)

noncomputable def Cslib.BitString.univariateParityProduct {ι : Type u_1} {κ : Type u_3} {R : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (ℓ : ℕ) (q : (ι → Bool) → κ → ι → Polynomial R) : Polynomial (Polynomial R)

§5.3 (H(T) in R[T][V]): the cube sum over x : ι → Bool of the product of parity factors evaluated at the univariate replacement forms q x i : ι → Polynomial R.

noncomputable def Cslib.BitString.univariateParityCoord {ι : Type u_1} {κ : Type u_3} {R : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (ℓ : ℕ) (q : (ι → Bool) → κ → ι → Polynomial R) (s : ℕ) : Polynomial R

§5.3 ([V ^ s] H(T)): the s-th V-coefficient polynomial of univariateParityProduct in R[T].

noncomputable def Cslib.BitString.univariateParityTruncatedSum {ι : Type u_1} {κ : Type u_3} {R : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (ℓ : ℕ) (q : (ι → Bool) → κ → ι → Polynomial R) : Polynomial R

§5.3 (S_ℓ(H(T))): the sum of the first ℓ V-coefficient polynomials of univariateParityProduct in R[T].

theorem Cslib.BitString.univariateParityTruncatedSum_eq_sum_coord {ι : Type u_1} {κ : Type u_3} {R : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (ℓ : ℕ) (q : (ι → Bool) → κ → ι → Polynomial R) : univariateParityTruncatedSum I P ℓ q = ∑ s ∈ Finset.range ℓ, univariateParityCoord I P ℓ q s

univariateParityTruncatedSum is the sum of univariateParityCoord I P ℓ q s for s ∈ range ℓ.

theorem Cslib.BitString.univariateParityCoord_eq_sum {ι : Type u_1} {κ : Type u_3} {R : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (ℓ : ℕ) (q : (ι → Bool) → κ → ι → Polynomial R) (s : ℕ) : univariateParityCoord I P ℓ q s = ∑ x : ι → Bool, (∏ i ∈ I, Polynomial.parityFactor ℓ (univariateMonomialSumPoly R (q x i) (P i))).coeff s

univariateParityCoord expands as the cube sum of the V ^ s-coefficients of each x-term.

theorem Cslib.BitString.univariateParityTruncatedSum_eq_sum {ι : Type u_1} {κ : Type u_3} {R : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (ℓ : ℕ) (q : (ι → Bool) → κ → ι → Polynomial R) : univariateParityTruncatedSum I P ℓ q = ∑ x : ι → Bool, Polynomial.sumCoeffsBelow ℓ (∏ i ∈ I, Polynomial.parityFactor ℓ (univariateMonomialSumPoly R (q x i) (P i)))

univariateParityTruncatedSum expands as the cube sum of sumCoeffsBelow ℓ of each x-term.

theorem Cslib.BitString.natDegree_univariateParityCoord_le {ι : Type u_1} {κ : Type u_3} {R : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (ℓ : ℕ) (q : (ι → Bool) → κ → ι → Polynomial R) {k R_deg : ℕ} (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hq : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (q x i v).natDegree ≤ R_deg) {s : ℕ} (hs : s < ℓ) : (univariateParityCoord I P ℓ q s).natDegree ≤ k * R_deg * (I.card + 2 * (ℓ - 1))

§5.3, eq. (5.5a) (coordinatewise degree bound $\deg_T [V^s] H(T) \le k R_{\mathrm{deg}} (\#I + 2(\ell - 1))$): if every equation has degree at most k and every replacement polynomial q x i v has natDegree ≤ R_deg, then for s < ℓ, univariateParityCoord I P ℓ q s has natDegree ≤ (k * R_deg) * (#I + 2 * (ℓ - 1)).

theorem Cslib.BitString.natDegree_univariateParityTruncatedSum_le {ι : Type u_1} {κ : Type u_3} {R : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (ℓ : ℕ) (q : (ι → Bool) → κ → ι → Polynomial R) {k R_deg : ℕ} (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hq : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (q x i v).natDegree ≤ R_deg) : (univariateParityTruncatedSum I P ℓ q).natDegree ≤ k * R_deg * (I.card + 2 * (ℓ - 1))

§5.3, eq. (5.5a) ($\deg_T S_\ell(H(T)) \le k R_{\mathrm{deg}} (\#I + 2(\ell - 1))$): if every equation has degree at most k and every replacement polynomial q x i v has natDegree ≤ R_deg, then univariateParityTruncatedSum I P ℓ q has natDegree ≤ (k * R_deg) * (#I + 2 * (ℓ - 1)).

theorem Cslib.BitString.eval_zero_univariateParityTruncatedSum {ι : Type u_1} {κ : Type u_3} {R : Type u_4} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (ℓ : ℕ) (q : (ι → Bool) → κ → ι → Polynomial R) (hq0 : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.eval 0 (q x i v) = bitVal R (x v)) : Polynomial.eval 0 (univariateParityTruncatedSum I P ℓ q) = ∑ x : ι → Bool, Polynomial.sumCoeffsBelow ℓ (∏ i ∈ I, Polynomial.parityFactor ℓ (monomialSum R (P i) x))

§5.3, eq. (5.5b) (evaluation restoration at T = 0): when every replacement polynomial q x i v restores bitVal R (x v) at T = 0, evaluating univariateParityTruncatedSum at 0 yields the cube sum of truncated parity-factor products at monomialSum R (P i) x.

theorem Cslib.BitString.eval_zero_univariateParityTruncatedSum_modEq_commonZeroCount {ι : Type u_1} {κ : Type u_3} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (q : (ι → Bool) → κ → ι → Polynomial ℤ) (hq0 : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.eval 0 (q x i v) = bitVal ℤ (x v)) : Polynomial.eval 0 (univariateParityTruncatedSum I P ℓ q) ≡ ↑(commonZeroCount I P) [ZMOD 2 ^ ℓ]

§5.3, eq. (5.5b) ($S_\ell(H(0)) \equiv N(\mathcal{P}) \pmod{2^\ell}$): when every integer replacement polynomial q x i v restores bitVal ℤ (x v) at T = 0, (univariateParityTruncatedSum I P ℓ q).eval 0 ≡ commonZeroCount I P [ZMOD 2 ^ ℓ].

theorem Cslib.BitString.emod_eval_zero_univariateParityTruncatedSum_eq_commonZeroCount {ι : Type u_1} {κ : Type u_3} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {ℓ : ℕ} (hℓ : Fintype.card ι < ℓ) (q : (ι → Bool) → κ → ι → Polynomial ℤ) (hq0 : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.eval 0 (q x i v) = bitVal ℤ (x v)) : Polynomial.eval 0 (univariateParityTruncatedSum I P ℓ q) % 2 ^ ℓ = ↑(commonZeroCount I P)

§5.3, eq. (5.5b) (exact recovery of $N(\mathcal{P})$ from $S_\ell(H(0)) \bmod 2^\ell$): when Fintype.card ι < ℓ and every replacement polynomial q x i v restores bitVal ℤ (x v) at T = 0, the least nonnegative residue of (univariateParityTruncatedSum I P ℓ q).eval 0 modulo 2 ^ ℓ equals commonZeroCount I P.

Section 3: Free-variable branch relabeling (§5.5, Proof of Theorem 2.2)

def Cslib.BitString.relabelMonomials {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι'] (f : ι → ι') (𝓜 : Finset (Finset ι)) : Finset (Finset ι')

Relabeling every monomial M ∈ 𝓜 along a map f : ι → ι'.

def Cslib.BitString.relabelRestrictedMonomials {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq ι'] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (b : ι → Bool) (𝓜 : Finset (Finset ι)) : Finset (Finset ι')

Relabeling a restricted branch equation restrictMonomials S b 𝓜 (whose monomials are subsets of univ \ S) across an equivalence e : ↥(univ \ S) ≃ ι' onto a free-variable index type ι'.

def Cslib.BitString.extendFreeAssignment {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [DecidableEq ι] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (y : ι' → Bool) (v : ι) : Bool

Extending a free-variable assignment y : ι' → Bool by false on S to obtain a canonical representative in subproblemAssignments S.

def Cslib.BitString.restrictToFreeVars {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [DecidableEq ι] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (z : ι → Bool) (w : ι') : Bool

Restricting an assignment z : ι → Bool to ι' along e : ↥(univ \ S) ≃ ι'.

@[simp]

theorem Cslib.BitString.restrictToFreeVars_extendFreeAssignment {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [DecidableEq ι] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (y : ι' → Bool) : restrictToFreeVars S e (extendFreeAssignment S e y) = y

theorem Cslib.BitString.extendFreeAssignment_mem_subproblemAssignments {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [DecidableEq ι] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (y : ι' → Bool) : extendFreeAssignment S e y ∈ subproblemAssignments S

theorem Cslib.BitString.extendFreeAssignment_restrictToFreeVars {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [DecidableEq ι] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') {z : ι → Bool} (hz : z ∈ subproblemAssignments S) : extendFreeAssignment S e (restrictToFreeVars S e z) = z

theorem Cslib.BitString.card_mem_relabelRestrictedMonomials_le {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq ι'] {S : Finset ι} {e : ↥(Finset.univ \ S) ≃ ι'} {b : ι → Bool} {𝓜 : Finset (Finset ι)} {k : ℕ} (hk : ∀ M ∈ 𝓜, M.card ≤ k) (M' : Finset ι') : M' ∈ relabelRestrictedMonomials S e b 𝓜 → M'.card ≤ k

Every monomial in relabelRestrictedMonomials S e b 𝓜 has degree at most k when every monomial in 𝓜 has degree at most k.

theorem Cslib.BitString.card_relabelRestrictedMonomials_le {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq ι'] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (b : ι → Bool) (𝓜 : Finset (Finset ι)) : (relabelRestrictedMonomials S e b 𝓜).card ≤ 𝓜.card

relabelRestrictedMonomials never increases the number of monomials.

theorem Cslib.BitString.monomialSum_relabelRestrictedMonomials {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq ι'] (R : Type u_5) [CommRing R] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (b : ι → Bool) (𝓜 : Finset (Finset ι)) (y : ι' → Bool) : monomialSum R (relabelRestrictedMonomials S e b 𝓜) y = monomialSum R (restrictMonomials S b 𝓜) (extendFreeAssignment S e y)

Evaluating relabelRestrictedMonomials S e b 𝓜 at y : ι' → Bool in any commutative ring R agrees with evaluating restrictMonomials S b 𝓜 at extendFreeAssignment S e y.

theorem Cslib.BitString.commonZeroCount_eq_sum_relabelRestrictedMonomials {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (I : Finset κ) (P : κ → Finset (Finset ι)) : commonZeroCount I P = ∑ b ∈ branchAssignments S, commonZeroCount I fun (i : κ) => relabelRestrictedMonomials S e b (P i)

§5.5–5.6 (Theorem 2.2 additive branch decomposition on the relabeled free-variable cube ι' → Bool): for any branch variable set S and equivalence e : ↥(univ \ S) ≃ ι', the common-zero count commonZeroCount I P equals the sum over b ∈ branchAssignments S of commonZeroCount of the relabeled restricted equations on ι' → Bool.

theorem Cslib.BitString.equationScope_relabelRestrictedMonomials_subset {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq ι'] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (b : ι → Bool) (𝓜 : Finset (Finset ι)) : equationScope (relabelRestrictedMonomials S e b 𝓜) ⊆ Finset.image (⇑e) (Finset.subtype (fun (x : ι) => x ∈ Finset.univ \ S) (equationScope 𝓜 \ S))

The variable scope of relabelRestrictedMonomials S e b 𝓜 is contained in the image under e of (equationScope 𝓜 \ S).subtype (· ∈ univ \ S).

theorem Cslib.BitString.varIncidence_relabelRestrictedMonomials_heavyVars_le {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [DecidableEq ι'] (F I : Finset κ) (P : κ → Finset (Finset ι)) (b₀ : ℕ) (hIF : I ⊆ F) (e : ↥(Finset.univ \ heavyVars Finset.univ F (fun (i : κ) => equationScope (P i)) b₀) ≃ ι') (b : ι → Bool) (w : ι') : varIncidence I (fun (i : κ) => equationScope (relabelRestrictedMonomials (heavyVars Finset.univ F (fun (i : κ) => equationScope (P i)) b₀) e b (P i))) w ≤ b₀

§5.5–5.6 (free-variable incidence bound on ι' after branching on heavyVars): for S = heavyVars univ F (fun i => equationScope (P i)) b₀ and I ⊆ F, every variable w : ι' has incidence at most b₀ in the relabeled restricted system.

Section 4: Neutral variable-coverage scopes and Theorem 2.2 threshold bounds (§5.5)

def Cslib.BitString.withNeutralFactors {ι' : Type u_2} {κ : Type u_3} [Fintype ι'] (I : Finset κ) : Finset (κ ⊕ ι')

§5.5 (neutral variable-coverage factor index set): adjoins one neutral factor Sum.inr v for each declared variable v : ι' to the equation index set I.

def Cslib.BitString.withNeutralScope {ι' : Type u_2} {κ : Type u_3} (scope : κ → Finset ι') : κ ⊕ ι' → Finset ι'

§5.5 (neutral variable-coverage scopes): retains scope i for Sum.inl i and assigns the singleton scope {v} to each neutral factor Sum.inr v.

theorem Cslib.BitString.varIncidence_withNeutralFactors {ι' : Type u_2} {κ : Type u_3} [Fintype ι'] [DecidableEq ι'] (I : Finset κ) (scope : κ → Finset ι') (v : ι') : varIncidence (withNeutralFactors I) (withNeutralScope scope) v = varIncidence I scope v + 1

Adjoining neutral singleton scopes increments the incidence of every variable v : ι' by exactly 1.

theorem Cslib.BitString.one_le_varIncidence_withNeutralFactors {ι' : Type u_2} {κ : Type u_3} [Fintype ι'] [DecidableEq ι'] (I : Finset κ) (scope : κ → Finset ι') (v : ι') : 1 ≤ varIncidence (withNeutralFactors I) (withNeutralScope scope) v

Every declared variable v : ι' has incidence at least 1 after adjoining neutral scopes.

theorem Cslib.BitString.varIncidence_withNeutralFactors_le {ι' : Type u_2} {κ : Type u_3} [Fintype ι'] [DecidableEq ι'] {I : Finset κ} {scope : κ → Finset ι'} {v : ι'} {b₀ : ℕ} (hv : varIncidence I scope v ≤ b₀) : varIncidence (withNeutralFactors I) (withNeutralScope scope) v ≤ b₀ + 1

If varIncidence I scope v ≤ b₀, then after adjoining neutral scopes the variable incidence is at most b₀ + 1.

theorem Cslib.BitString.totalIncidence_withNeutralFactors {ι' : Type u_2} {κ : Type u_3} [Fintype ι'] (I : Finset κ) (scope : κ → Finset ι') : totalIncidence (withNeutralFactors I) (withNeutralScope scope) = totalIncidence I scope + Fintype.card ι'

Adjoining neutral singleton scopes adds Fintype.card ι' to totalIncidence.

theorem Cslib.BitString.card_le_totalIncidence_withNeutralFactors {ι' : Type u_2} {κ : Type u_3} [Fintype ι'] (I : Finset κ) (scope : κ → Finset ι') : Fintype.card ι' ≤ totalIncidence (withNeutralFactors I) (withNeutralScope scope)

§5.5 ($M' \ge n'$): after adjoining neutral singleton scopes, the total incidence is at least Fintype.card ι'.

def Cslib.BitString.paperHeavyThreshold (M n s : ℕ) : ℕ

§5.5 (manuscript heavy-variable threshold $b_0 = \lceil M / n \rceil s$, p. 38): the product ((M + n - 1) / n) * s of the integer ceiling ⌈M / n⌉ and s.

def Cslib.BitString.heavyThreshold (M n s : ℕ) : ℕ

Combined-ceiling variant ⌈M * s / n⌉ = (M * s + n - 1) / n of the heavy-variable threshold.

theorem Cslib.BitString.mul_le_heavyThreshold_mul {M n s : ℕ} (hn : 1 ≤ n) : M * s ≤ heavyThreshold M n s * n

When 1 ≤ n, M * s ≤ heavyThreshold M n s * n.

theorem Cslib.BitString.mul_le_paperHeavyThreshold_mul {M n s : ℕ} (hn : 1 ≤ n) : M * s ≤ paperHeavyThreshold M n s * n

When 1 ≤ n, M * s ≤ paperHeavyThreshold M n s * n.

theorem Cslib.BitString.card_heavyVars_le_card_div {ι : Type u_1} {κ : Type u_3} [DecidableEq ι] (V : Finset ι) (F : Finset κ) (scope : κ → Finset ι) {b₀ s : ℕ} (hb₀ : 1 ≤ b₀) (hs : 1 ≤ s) (hV : ∀ i ∈ F, scope i ⊆ V) (hM : totalIncidence F scope * s ≤ b₀ * V.card) : (heavyVars V F scope b₀).card ≤ V.card / s

§5.5 ($|S| \le n / s$): whenever totalIncidence F scope * s ≤ b₀ * #V, 1 ≤ b₀, 1 ≤ s, and ∀ i ∈ F, scope i ⊆ V, the heavy-variable set heavyVars V F scope b₀ has cardinality at most #V / s.

theorem Cslib.BitString.card_branchAssignments_heavyVars_le_two_pow_div {ι : Type u_1} {κ : Type u_3} [Fintype ι] [DecidableEq ι] (F : Finset κ) (scope : κ → Finset ι) {b₀ s : ℕ} (hb₀ : 1 ≤ b₀) (hs : 1 ≤ s) (hM : totalIncidence F scope * s ≤ b₀ * Fintype.card ι) : (branchAssignments (heavyVars Finset.univ F scope b₀)).card ≤ 2 ^ (Fintype.card ι / s)

§5.5 ($2^{|S|} \le 2^{n / s}$): under totalIncidence F scope * s ≤ b₀ * Fintype.card ι, 1 ≤ b₀, and 1 ≤ s, there are at most 2 ^ (Fintype.card ι / s) heavy-variable branches.

theorem Cslib.BitString.card_sdiff_heavyVars_ge {ι : Type u_1} {κ : Type u_3} [DecidableEq ι] (V : Finset ι) (F : Finset κ) (scope : κ → Finset ι) {b₀ s : ℕ} (hb₀ : 1 ≤ b₀) (hs : 1 ≤ s) (hV : ∀ i ∈ F, scope i ⊆ V) (hM : totalIncidence F scope * s ≤ b₀ * V.card) : V.card - V.card / s ≤ (V \ heavyVars V F scope b₀).card

§5.5 ($n' = n - |S| \ge n - n / s$): under totalIncidence F scope * s ≤ b₀ * #V, 1 ≤ b₀, 1 ≤ s, and ∀ i ∈ F, scope i ⊆ V, the set V \ heavyVars V F scope b₀ of free variables has cardinality at least #V - #V / s.

theorem Cslib.BitString.card_sdiff_heavyVars_ge_half {ι : Type u_1} {κ : Type u_3} [DecidableEq ι] (V : Finset ι) (F : Finset κ) (scope : κ → Finset ι) {b₀ s : ℕ} (hb₀ : 1 ≤ b₀) (hs : 2 ≤ s) (hV : ∀ i ∈ F, scope i ⊆ V) (hM : totalIncidence F scope * s ≤ b₀ * V.card) : V.card ≤ 2 * (V \ heavyVars V F scope b₀).card ∧ V.card / 2 ≤ (V \ heavyVars V F scope b₀).card

§5.5 ($n' \ge n / 2$ for $s \ge 2$): when 2 ≤ s, 1 ≤ b₀, ∀ i ∈ F, scope i ⊆ V, and totalIncidence F scope * s ≤ b₀ * #V, at least half of the variables in V remain free after removing heavyVars V F scope b₀: #V ≤ 2 * #(V \ heavyVars V F scope b₀) and #V / 2 ≤ #(V \ heavyVars V F scope b₀).

def Cslib.BitString.branchPrecision (n : ℕ) : ℕ

§5.1 & §5.5 ($\ell = n + 1$): the shared modular precision n + 1 used for both the unrestricted system on n variables and every free-variable branch.

theorem Cslib.BitString.emod_eval_zero_univariateParityTruncatedSum_branch_eq {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype ι'] [DecidableEq ι] [DecidableEq ι'] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (I : Finset κ) (P : κ → Finset (Finset ι)) (b : ι → Bool) (q : (ι' → Bool) → κ → ι' → Polynomial ℤ) (hq0 : ∀ (x : ι' → Bool), ∀ i ∈ I, ∀ M ∈ relabelRestrictedMonomials S e b (P i), ∀ v ∈ M, Polynomial.eval 0 (q x i v) = bitVal ℤ (x v)) : Polynomial.eval 0 (univariateParityTruncatedSum I (fun (i : κ) => relabelRestrictedMonomials S e b (P i)) (branchPrecision (Fintype.card ι)) q) % 2 ^ branchPrecision (Fintype.card ι) = ↑(commonZeroCount I fun (i : κ) => relabelRestrictedMonomials S e b (P i))

§5.5 (exact branch recovery at original precision $\ell = n + 1$): on any branch (S, b) relabeled along e : ↥(univ \ S) ≃ ι', evaluating univariateParityTruncatedSum at T = 0 with the original precision branchPrecision (Fintype.card ι) = n + 1 and taking the remainder modulo 2 ^ branchPrecision (Fintype.card ι) yields the exact branch common-zero count.

theorem Cslib.BitString.commonZeroCount_eq_sum_branch_emod_eval_zero {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype ι'] [DecidableEq ι] [DecidableEq ι'] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (I : Finset κ) (P : κ → Finset (Finset ι)) (q : (ι → Bool) → (ι' → Bool) → κ → ι' → Polynomial ℤ) (hq0 : ∀ b ∈ branchAssignments S, ∀ (x : ι' → Bool), ∀ i ∈ I, ∀ M ∈ relabelRestrictedMonomials S e b (P i), ∀ v ∈ M, Polynomial.eval 0 (q b x i v) = bitVal ℤ (x v)) : ↑(commonZeroCount I P) = ∑ b ∈ branchAssignments S, Polynomial.eval 0 (univariateParityTruncatedSum I (fun (i : κ) => relabelRestrictedMonomials S e b (P i)) (branchPrecision (Fintype.card ι)) (q b)) % 2 ^ branchPrecision (Fintype.card ι)

§5.5 (Theorem 2.2 branch-summed modular recovery): summing the per-branch T = 0 remainders modulo 2 ^ branchPrecision (Fintype.card ι) across all b ∈ branchAssignments S recovers the exact unrestricted count (commonZeroCount I P : ℤ).

theorem Cslib.BitString.branchEquationBudget_le {m c n n' : ℕ} (hm : m ≤ c * n) (hn : n ≤ 2 * n') : m + 2 * (branchPrecision n - 1) ≤ (2 * c + 4) * n'

§5.5 ($m_{\mathrm{test}} + 2(\ell - 1) \le (2c + 4)n'$ when $n \le 2n'$): when m ≤ c * n and n ≤ 2 * n', the equation-plus-precision factor m + 2 * (branchPrecision n - 1) is at most (2 * c + 4) * n'.

theorem Cslib.BitString.natDegree_univariateParityTruncatedSum_branch_le {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_4} [CommRing R] [Fintype ι] [Fintype ι'] [DecidableEq ι] [DecidableEq ι'] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (I : Finset κ) (P : κ → Finset (Finset ι)) (b : ι → Bool) (q : (ι' → Bool) → κ → ι' → Polynomial R) {k R_deg c : ℕ} (hm : I.card ≤ c * Fintype.card ι) (hn : Fintype.card ι ≤ 2 * Fintype.card ι') (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hdeg : ∀ (x : ι' → Bool), ∀ i ∈ I, ∀ M ∈ relabelRestrictedMonomials S e b (P i), ∀ v ∈ M, (q x i v).natDegree ≤ R_deg) : (univariateParityTruncatedSum I (fun (i : κ) => relabelRestrictedMonomials S e b (P i)) (branchPrecision (Fintype.card ι)) q).natDegree ≤ k * R_deg * ((2 * c + 4) * Fintype.card ι')

§5.5 ($d_H = O_{k, c}(n' R)$ per-branch degree bound): on any branch (S, b) relabeled along e : ↥(univ \ S) ≃ ι', if #I ≤ c * Fintype.card ι, Fintype.card ι ≤ 2 * Fintype.card ι', every monomial in the unrestricted system P has degree at most k, and every branch replacement polynomial q x i v has natDegree ≤ R_deg, then univariateParityTruncatedSum at precision branchPrecision (Fintype.card ι) has natDegree at most (k * R_deg) * ((2 * c + 4) * Fintype.card ι').