Sparse polynomial equations over 𝔽₂, common-zero counting, and heavy-variable branching

A sparse degree-k polynomial over 𝔽₂ on the Boolean cube ι → Bool is represented by a finite family 𝓜 : Finset (Finset ι) of monomials M ⊆ ι of size at most k, evaluated in any commutative ring R via Cslib.BitString.monomialSum R 𝓜 x = ∑ M ∈ 𝓜, monomial R M x and lifted to MvPolynomial ι R via Cslib.BitString.monomialSumPoly R 𝓜.

Over ZMod 2, monomialSum (ZMod 2) 𝓜 x = 0 holds if and only if the integer evaluation monomialSum ℤ 𝓜 x is even (Cslib.BitString.monomialSum_zmod_two_eq_zero_iff_even). Consequently, the number of common zeros Cslib.BitString.commonZeroCount I P of a system {P i}_{i ∈ I} of polynomial equations over 𝔽₂ equals the sum over the Boolean cube of the product of evenness indicators of their integer evaluations (Cslib.BitString.sum_prod_even_monomialSum_eq_commonZeroCount).

Combining this identity with the Beigel–Tarui parity-amplifying polynomials and shared-V truncation from Complexity.Foundations.Data.Polynomial.ParityAmplifier Toda, Arora and Barak, Section 17.4:

• Substituting any family of polynomials q : ι → MvPolynomial σ R of total degree at most d₀ into monomialSumPoly R (P i) of degree at most k produces a lifted polynomial of total degree at most k * d₀ (Cslib.BitString.totalDegree_eval₂_monomialSumPoly_le), so the truncated shared-V product S_ℓ(∏ i ∈ I, B_i(V)) has total degree at most (k * d₀) * (#I + 2 * (ℓ - 1)) (Cslib.BitString.totalDegree_sumCoeffsBelow_prod_parityFactor_eval₂_le).
• Summing the truncated product over x : ι → Bool recovers commonZeroCount I P modulo 2 ^ ℓ (Cslib.BitString.sum_sumCoeffsBelow_prod_parityFactor_modEq_commonZeroCount), and recovers commonZeroCount I P on the nose via (· % 2 ^ ℓ) whenever Fintype.card ι < ℓ (Cslib.BitString.emod_sum_sumCoeffsBelow_prod_parityFactor_eq_commonZeroCount).

Finally, for any system of equations with variable scopes scope : κ → Finset ι contained in a candidate variable set V (∀ i ∈ F, scope i ⊆ V) and positive incidence threshold 1 ≤ b₀, the set Cslib.BitString.heavyVars V F scope b₀ of variables in V appearing in more than b₀ scopes has cardinality at most totalIncidence F scope / b₀ (Cslib.BitString.card_heavyVars_le_div), while every remaining variable in V \ heavyVars V F scope b₀ (and in any post-branching restricted equation scope when ∀ i ∈ I, equationScope (P i) ⊆ V) has incidence at most b₀. Branching on all 2 ^ #S assignments to a variable subset S and simplifying each equation via Cslib.BitString.restrictMonomials preserves degree bounds, never increases the number of monomials per equation, and decomposes commonZeroCount additively across the branches (Cslib.BitString.commonZeroCount_eq_sum_branches).

Main definitions

• Cslib.BitString.monomialSum: evaluation ∑ M ∈ 𝓜, monomial R M x of a family of monomials.
• Cslib.BitString.monomialPoly, Cslib.BitString.monomialSumPoly: formal multilinear polynomial lifts in MvPolynomial ι R.
• Cslib.BitString.IsCommonZero, Cslib.BitString.commonZeroCount: common zeros of a system of 𝔽₂ polynomial equations on ι → Bool and their count.
• Cslib.BitString.varIncidence, Cslib.BitString.totalIncidence, Cslib.BitString.heavyVars: variable-equation incidence counts and heavy-variable set above threshold b₀.
• Cslib.BitString.patchAssignment, Cslib.BitString.restrictMonomials: patching a branch assignment on S and reducing a monomial family modulo 2 after specializing S.
• Cslib.BitString.parityBaseDigitCleared, Cslib.BitString.hPolyCleared, Cslib.BitString.parityFactorCleared, Cslib.BitString.clearedMonomialPoly, Cslib.BitString.clearedMonomialSumPoly: cleared-denominator parity factors and degree-k homogenized monomial sums from §5.4 and Appendix B.2.

Main results

• Cslib.BitString.monomialSum_zmod_two_eq_zero_iff_even: 𝔽₂ vanishing iff even ℤ evaluation.
• Cslib.BitString.sum_prod_even_monomialSum_eq_commonZeroCount: equation (5.1) expressing commonZeroCount as the cube sum of products of evenness indicators.
• Cslib.BitString.totalDegree_sumCoeffsBelow_prod_parityFactor_eval₂_le: total-degree bound (k * d₀) * (#I + 2 * (ℓ - 1)) for the truncated product under degree-d₀ replacements.
• Cslib.BitString.emod_sum_sumCoeffsBelow_prod_parityFactor_eq_commonZeroCount: exact recovery of commonZeroCount modulo 2 ^ ℓ when Fintype.card ι < ℓ.
• Cslib.BitString.card_heavyVars_le_div and Cslib.BitString.varIncidence_sdiff_heavyVars_le: heavy-variable cardinality bound and light-variable incidence bound.
• Cslib.BitString.monomialSum_zmod_two_restrictMonomials and Cslib.BitString.commonZeroCount_eq_sum_branches: exact 𝔽₂ specialization and additive branch decomposition of commonZeroCount.
• Cslib.BitString.prod_parityFactorCleared_mul, Cslib.BitString.coeffNorm1_clearedMonomialSumPoly_le, and Cslib.BitString.coeffNorm1_coeff_parityFactorCleared_le: cleared-denominator homogenization ($\Delta = d_{\text{den}}^k$, $\Gamma = \Delta^{2\ell-1}$, $\Omega = \Gamma^{\#I}$) and numerator ℓ₁-norm bounds from §5.4 and Appendix B.2.

References

• S. Toda, PP is as hard as the polynomial-time hierarchy
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• OpenAI, The Exponential Time Hypothesis is False (Sections 5.1, 5.3, 5.4, 5.5, and Appendix B.2)

1. Monomial sums, integer lifts, and commonZeroCount

def Cslib.BitString.monomialSum {ι : Type u_1} (R : Type u_5) [CommRing R] (𝓜 : Finset (Finset ι)) (x : ι → Bool) : R

The sum of the monomials in 𝓜 : Finset (Finset ι) evaluated at x : ι → Bool in R.

@[simp]

theorem Cslib.BitString.monomialSum_empty {ι : Type u_1} (R : Type u_5) [CommRing R] (x : ι → Bool) : monomialSum R ∅ x = 0

The empty family of monomials evaluates to 0.

@[simp]

theorem Cslib.BitString.monomialSum_singleton {ι : Type u_1} (R : Type u_5) [CommRing R] (M : Finset ι) (x : ι → Bool) : monomialSum R {M} x = monomial R M x

A singleton family {M} evaluates to monomial R M x.

theorem Cslib.BitString.monomialSum_eq_card_filter {ι : Type u_1} (R : Type u_5) [CommRing R] (𝓜 : Finset (Finset ι)) (x : ι → Bool) : monomialSum R 𝓜 x = ↑{M ∈ 𝓜 | ∀ v ∈ M, x v = true}.card

monomialSum R 𝓜 x equals the cast to R of the number of monomials M ∈ 𝓜 satisfied by x.

theorem Cslib.BitString.monomialSum_zmod_two_eq_zero_iff_even {ι : Type u_1} (𝓜 : Finset (Finset ι)) (x : ι → Bool) : monomialSum (ZMod 2) 𝓜 x = 0 ↔ Even (monomialSum ℤ 𝓜 x)

A monomial sum vanishes in ZMod 2 at x if and only if its integer lift monomialSum ℤ 𝓜 x is even.

def Cslib.BitString.IsCommonZero {ι : Type u_1} {κ : Type u_2} (I : Finset κ) (P : κ → Finset (Finset ι)) (x : ι → Bool) : Prop

An assignment x : ι → Bool is a common zero of the family {P i}_{i ∈ I} over 𝔽₂ if every equation P i (i ∈ I) evaluates to 0 in ZMod 2 at x.

@[instance_reducible]

instance Cslib.BitString.instDecidableIsCommonZero {ι : Type u_1} {κ : Type u_2} (I : Finset κ) (P : κ → Finset (Finset ι)) (x : ι → Bool) : Decidable (IsCommonZero I P x)

theorem Cslib.BitString.isCommonZero_iff_forall_even {ι : Type u_1} {κ : Type u_2} (I : Finset κ) (P : κ → Finset (Finset ι)) (x : ι → Bool) : IsCommonZero I P x ↔ ∀ i ∈ I, Even (monomialSum ℤ (P i) x)

x is a common zero over 𝔽₂ if and only if all integer evaluations monomialSum ℤ (P i) x (i ∈ I) are even.

def Cslib.BitString.commonZeroCount {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) : ℕ

The number of common zeros x : ι → Bool of the polynomial system {P i}_{i ∈ I} over 𝔽₂.

theorem Cslib.BitString.prod_even_monomialSum_eq_ite {ι : Type u_1} {κ : Type u_2} (I : Finset κ) (P : κ → Finset (Finset ι)) (x : ι → Bool) : (∏ i ∈ I, if Even (monomialSum ℤ (P i) x) then 1 else 0) = if IsCommonZero I P x then 1 else 0

At any assignment x, the product of the evenness indicators of monomialSum ℤ (P i) x over i ∈ I is 1 if IsCommonZero I P x and 0 otherwise.

theorem Cslib.BitString.sum_prod_even_monomialSum_eq_commonZeroCount {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) : (∑ x : ι → Bool, ∏ i ∈ I, if Even (monomialSum ℤ (P i) x) then 1 else 0) = ↑(commonZeroCount I P)

Equation (5.1): the common-zero count of {P i}_{i ∈ I} over 𝔽₂ equals the sum over the Boolean cube of the product of evenness indicators of the integer lifts monomialSum ℤ (P i) x.

@[simp]

theorem Cslib.BitString.commonZeroCount_empty {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (P : κ → Finset (Finset ι)) : commonZeroCount ∅ P = 2 ^ Fintype.card ι

An empty system of equations has 2 ^ Fintype.card ι common zeros.

theorem Cslib.BitString.commonZeroCount_eq_zero_of_singleton_empty {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] {I : Finset κ} {P : κ → Finset (Finset ι)} {i : κ} (hi : i ∈ I) (hP : P i = {∅}) : commonZeroCount I P = 0

If some equation i ∈ I is the constant polynomial 1 (P i = {∅}), there are no common zeros.

theorem Cslib.BitString.commonZeroCount_le_two_pow {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) : commonZeroCount I P ≤ 2 ^ Fintype.card ι

commonZeroCount I P is at most 2 ^ Fintype.card ι.

2. Formal multilinear lifts and replacement total-degree bounds

noncomputable def Cslib.BitString.monomialPoly {ι : Type u_1} (R : Type u_5) [CommSemiring R] (M : Finset ι) : MvPolynomial ι R

The formal multilinear monomial ∏ v ∈ M, X v in MvPolynomial ι R.

noncomputable def Cslib.BitString.monomialSumPoly {ι : Type u_1} (R : Type u_5) [CommSemiring R] (𝓜 : Finset (Finset ι)) : MvPolynomial ι R

The formal multilinear polynomial ∑ M ∈ 𝓜, ∏ v ∈ M, X v in MvPolynomial ι R.

@[simp]

theorem Cslib.BitString.aeval_bitVal_monomialPoly {ι : Type u_1} (R : Type u_5) [CommRing R] (M : Finset ι) (x : ι → Bool) : (MvPolynomial.aeval fun (v : ι) => bitVal R (x v)) (monomialPoly R M) = monomial R M x

Evaluating monomialPoly R M at v ↦ bitVal R (x v) gives monomial R M x.

@[simp]

theorem Cslib.BitString.aeval_bitVal_monomialSumPoly {ι : Type u_1} (R : Type u_5) [CommRing R] (𝓜 : Finset (Finset ι)) (x : ι → Bool) : (MvPolynomial.aeval fun (v : ι) => bitVal R (x v)) (monomialSumPoly R 𝓜) = monomialSum R 𝓜 x

Evaluating monomialSumPoly R 𝓜 at v ↦ bitVal R (x v) gives monomialSum R 𝓜 x.

theorem Cslib.BitString.eval₂_monomialPoly {ι : Type u_1} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] (f : R →+* S) (q : ι → S) (M : Finset ι) : MvPolynomial.eval₂ f q (monomialPoly R M) = ∏ v ∈ M, q v

Evaluating monomialPoly R M via eval₂ f q gives ∏ v ∈ M, q v.

theorem Cslib.BitString.totalDegree_eval₂_monomialPoly_le {ι : Type u_1} {σ : Type u_3} {R : Type u_4} [CommSemiring R] (f : R →+* MvPolynomial σ R) (q : ι → MvPolynomial σ R) {M : Finset ι} {d₀ : ℕ} (hq : ∀ v ∈ M, (q v).totalDegree ≤ d₀) : (MvPolynomial.eval₂ f q (monomialPoly R M)).totalDegree ≤ M.card * d₀

Substituting polynomials q v of total degree at most d₀ into monomialPoly R M produces a polynomial of total degree at most #M * d₀.

theorem Cslib.BitString.totalDegree_eval₂_monomialSumPoly_le {ι : Type u_1} {σ : Type u_3} {R : Type u_4} [CommSemiring R] (f : R →+* MvPolynomial σ R) (q : ι → MvPolynomial σ R) {𝓜 : Finset (Finset ι)} {k d₀ : ℕ} (hk : ∀ M ∈ 𝓜, M.card ≤ k) (hq : ∀ M ∈ 𝓜, ∀ v ∈ M, (q v).totalDegree ≤ d₀) : (MvPolynomial.eval₂ f q (monomialSumPoly R 𝓜)).totalDegree ≤ k * d₀

Substituting polynomials q v of total degree at most d₀ into monomialSumPoly R 𝓜 of degree at most k produces a polynomial of total degree at most k * d₀.

3. Truncated parity-factor degree bound (eq. 5.5) and count recovery (eq. 5.4)

theorem Cslib.BitString.totalDegree_sumCoeffsBelow_prod_parityFactor_eval₂_le {ι : Type u_1} {κ : Type u_2} {σ : Type u_3} {R : Type u_4} [CommRing R] (I : Finset κ) {P : κ → Finset (Finset ι)} (ℓ : ℕ) {k d₀ : ℕ} (f : R →+* MvPolynomial σ R) (q : κ → ι → MvPolynomial σ R) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hq : ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (q i v).totalDegree ≤ d₀) : (Polynomial.sumCoeffsBelow ℓ (∏ i ∈ I, Polynomial.parityFactor ℓ (MvPolynomial.eval₂ f (q i) (monomialSumPoly R (P i))))).totalDegree ≤ k * d₀ * (I.card + 2 * (ℓ - 1))

Equation (5.5) (truncated product degree bound under variable replacement): under the same hypotheses, the truncated sum S_ℓ(∏ i ∈ I, B_i(V)) has total degree at most (k * d₀) * (#I + 2 * (ℓ - 1)).

theorem Cslib.BitString.sumCoeffsBelow_sum {α : Type u_5} {A : Type u_6} [Semiring A] (s : Finset α) (ℓ : ℕ) (F : α → Polynomial A) : Polynomial.sumCoeffsBelow ℓ (∑ a ∈ s, F a) = ∑ a ∈ s, Polynomial.sumCoeffsBelow ℓ (F a)

Polynomial.sumCoeffsBelow ℓ commutes with finite sums.

theorem Cslib.BitString.sum_sumCoeffsBelow_prod_parityFactor_modEq_commonZeroCount {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) : ∑ x : ι → Bool, Polynomial.sumCoeffsBelow ℓ (∏ i ∈ I, Polynomial.parityFactor ℓ (monomialSum ℤ (P i) x)) ≡ ↑(commonZeroCount I P) [ZMOD 2 ^ ℓ]

Equation (5.4) (congruence modulo 2 ^ ℓ): for ℓ ≥ 1, summing the truncated product of parity factors of monomialSum ℤ (P i) x over x : ι → Bool recovers commonZeroCount I P modulo 2 ^ ℓ.

theorem Cslib.BitString.emod_sum_sumCoeffsBelow_prod_parityFactor_eq_commonZeroCount {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {ℓ : ℕ} (hℓ : Fintype.card ι < ℓ) : (∑ x : ι → Bool, Polynomial.sumCoeffsBelow ℓ (∏ i ∈ I, Polynomial.parityFactor ℓ (monomialSum ℤ (P i) x))) % 2 ^ ℓ = ↑(commonZeroCount I P)

Equation (5.4) (exact recovery via % 2 ^ ℓ): when Fintype.card ι < ℓ (in particular for ℓ = Fintype.card ι + 1), reducing the cube sum of truncated parity-factor products modulo 2 ^ ℓ recovers commonZeroCount I P on the nose.

4. Heavy-variable incidence bounds (§5.5)

def Cslib.BitString.varIncidence {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (F : Finset κ) (scope : κ → Finset ι) (v : ι) : ℕ

The number of constraints i ∈ F whose scope scope i contains variable v.

def Cslib.BitString.totalIncidence {ι : Type u_1} {κ : Type u_2} (F : Finset κ) (scope : κ → Finset ι) : ℕ

The total variable-constraint incidence ∑ i ∈ F, #(scope i).

theorem Cslib.BitString.sum_varIncidence_eq_totalIncidence {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (U : Finset ι) (F : Finset κ) (scope : κ → Finset ι) (hU : ∀ i ∈ F, scope i ⊆ U) : ∑ v ∈ U, varIncidence F scope v = totalIncidence F scope

Double-counting variable-constraint incidences over a universe U containing all scopes.

theorem Cslib.BitString.totalIncidence_le_mul_card {ι : Type u_1} {κ : Type u_2} (F : Finset κ) (scope : κ → Finset ι) {k : ℕ} (hk : ∀ i ∈ F, (scope i).card ≤ k) : totalIncidence F scope ≤ k * F.card

If every constraint in F has scope size at most k, then totalIncidence F scope is at most k * #F.

def Cslib.BitString.heavyVars {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (U : Finset ι) (F : Finset κ) (scope : κ → Finset ι) (b₀ : ℕ) : Finset ι

The set of heavy variables in U whose incidence in F strictly exceeds b₀.

theorem Cslib.BitString.card_heavyVars_mul_succ_le_totalIncidence {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (U : Finset ι) (F : Finset κ) (scope : κ → Finset ι) (b₀ : ℕ) (hU : ∀ i ∈ F, scope i ⊆ U) : (heavyVars U F scope b₀).card * (b₀ + 1) ≤ totalIncidence F scope

Markov / counting bound: #(heavyVars U F scope b₀) * (b₀ + 1) ≤ totalIncidence F scope.

theorem Cslib.BitString.card_heavyVars_mul_le_totalIncidence {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (U : Finset ι) (F : Finset κ) (scope : κ → Finset ι) (b₀ : ℕ) (hU : ∀ i ∈ F, scope i ⊆ U) : (heavyVars U F scope b₀).card * b₀ ≤ totalIncidence F scope

#(heavyVars U F scope b₀) * b₀ ≤ totalIncidence F scope.

theorem Cslib.BitString.card_heavyVars_le_div {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (U : Finset ι) (F : Finset κ) (scope : κ → Finset ι) {b₀ : ℕ} (hb₀ : 0 < b₀) (hU : ∀ i ∈ F, scope i ⊆ U) : (heavyVars U F scope b₀).card ≤ totalIncidence F scope / b₀

§5.5 (heavy-variable cardinality bound): for b₀ > 0, the number of heavy variables is at most totalIncidence F scope / b₀.

theorem Cslib.BitString.varIncidence_le_of_mem_sdiff_heavyVars {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] {U : Finset ι} {F : Finset κ} {scope : κ → Finset ι} {b₀ : ℕ} {v : ι} (hv : v ∈ U \ heavyVars U F scope b₀) : varIncidence F scope v ≤ b₀

Every variable in U \ heavyVars U F scope b₀ has incidence at most b₀.

theorem Cslib.BitString.varIncidence_sdiff_heavyVars_le {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (U : Finset ι) (F : Finset κ) (scope : κ → Finset ι) (b₀ : ℕ) (hU : ∀ i ∈ F, scope i ⊆ U) (v : ι) : varIncidence F (fun (i : κ) => scope i \ heavyVars U F scope b₀) v ≤ b₀

Removing heavyVars U F scope b₀ from every scope reduces the incidence of every variable v : ι to at most b₀.

5. Exact branching on a variable subset S (§5.5)

def Cslib.BitString.patchAssignment {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (b y : ι → Bool) (v : ι) : Bool

The assignment that takes values from b on S and from y outside S.

@[simp]

theorem Cslib.BitString.patchAssignment_of_mem {ι : Type u_1} [DecidableEq ι] {S : Finset ι} {b y : ι → Bool} {v : ι} (hv : v ∈ S) : patchAssignment S b y v = b v

On S, patchAssignment S b y agrees with b.

@[simp]

theorem Cslib.BitString.patchAssignment_of_notMem {ι : Type u_1} [DecidableEq ι] {S : Finset ι} {b y : ι → Bool} {v : ι} (hv : v ∉ S) : patchAssignment S b y v = y v

Outside S, patchAssignment S b y agrees with y.

theorem Cslib.BitString.monomial_patchAssignment {ι : Type u_1} (R : Type u_5) [CommRing R] [DecidableEq ι] (S : Finset ι) (b y : ι → Bool) (M : Finset ι) : monomial R M (patchAssignment S b y) = (if ∀ v ∈ M ∩ S, b v = true then 1 else 0) * monomial R (M \ S) y

A monomial M evaluated on patchAssignment S b y factors into the indicator that b is all true on M ∩ S times monomial R (M \ S) y.

def Cslib.BitString.restrictMonomials {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (b : ι → Bool) (𝓜 : Finset (Finset ι)) : Finset (Finset ι)

The reduced family of monomials in the remaining variables after specializing S to b and combining duplicate restricted monomials M \ S modulo 2.

theorem Cslib.BitString.disjoint_of_mem_restrictMonomials {ι : Type u_1} [DecidableEq ι] {S : Finset ι} {b : ι → Bool} {𝓜 : Finset (Finset ι)} {M' : Finset ι} (hM' : M' ∈ restrictMonomials S b 𝓜) : Disjoint M' S

Every monomial in restrictMonomials S b 𝓜 is disjoint from S.

theorem Cslib.BitString.card_le_of_mem_restrictMonomials {ι : Type u_1} [DecidableEq ι] {S : Finset ι} {b : ι → Bool} {𝓜 : Finset (Finset ι)} {k : ℕ} (hk : ∀ M ∈ 𝓜, M.card ≤ k) {M' : Finset ι} (hM' : M' ∈ restrictMonomials S b 𝓜) : M'.card ≤ k

Specializing S never increases the degree of any monomial: if ∀ M ∈ 𝓜, #M ≤ k, then ∀ M' ∈ restrictMonomials S b 𝓜, #M' ≤ k.

theorem Cslib.BitString.card_restrictMonomials_le {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (b : ι → Bool) (𝓜 : Finset (Finset ι)) : (restrictMonomials S b 𝓜).card ≤ 𝓜.card

Specializing S and reducing modulo 2 never increases the number of monomials: #(restrictMonomials S b 𝓜) ≤ #𝓜.

theorem Cslib.BitString.monomialSum_patchAssignment_eq_sum_image {ι : Type u_1} (R : Type u_5) [CommRing R] [DecidableEq ι] (S : Finset ι) (b y : ι → Bool) (𝓜 : Finset (Finset ι)) : monomialSum R 𝓜 (patchAssignment S b y) = ∑ M' ∈ Finset.image (fun (x : Finset ι) => x \ S) 𝓜, ↑{M ∈ 𝓜 | M \ S = M' ∧ ∀ v ∈ M ∩ S, b v = true}.card * monomial R M' y

Over any commutative ring R, monomialSum R 𝓜 (patchAssignment S b y) groups by restricted monomials M' ∈ 𝓜.image (· \ S).

theorem Cslib.BitString.monomialSum_zmod_two_restrictMonomials {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (b y : ι → Bool) (𝓜 : Finset (Finset ι)) : monomialSum (ZMod 2) (restrictMonomials S b 𝓜) y = monomialSum (ZMod 2) 𝓜 (patchAssignment S b y)

§5.5 (exact 𝔽₂ specialization): over ZMod 2, evaluating restrictMonomials S b 𝓜 at y equals evaluating the original family 𝓜 at patchAssignment S b y.

theorem Cslib.BitString.isCommonZero_patchAssignment_iff {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (S : Finset ι) (b y : ι → Bool) (I : Finset κ) (P : κ → Finset (Finset ι)) : IsCommonZero I P (patchAssignment S b y) ↔ IsCommonZero I (fun (i : κ) => restrictMonomials S b (P i)) y

patchAssignment S b y is a common zero of P if and only if y is a common zero of the specialized system fun i => restrictMonomials S b (P i).

def Cslib.BitString.branchAssignments {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) : Finset (ι → Bool)

Canonical branch assignments supported on S (false outside S).

def Cslib.BitString.subproblemAssignments {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) : Finset (ι → Bool)

Canonical subproblem assignments supported outside S (false on S).

theorem Cslib.BitString.card_branchAssignments {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) : (branchAssignments S).card = 2 ^ S.card

There are 2 ^ #S canonical branch assignments in branchAssignments S.

def Cslib.BitString.equationScope {ι : Type u_1} [DecidableEq ι] (𝓜 : Finset (Finset ι)) : Finset ι

The variable scope ⋃ M ∈ 𝓜, M of a family 𝓜 of monomials.

theorem Cslib.BitString.card_equationScope_le {ι : Type u_1} [DecidableEq ι] {𝓜 : Finset (Finset ι)} {k : ℕ} (hk : ∀ M ∈ 𝓜, M.card ≤ k) : (equationScope 𝓜).card ≤ k * 𝓜.card

If every monomial in 𝓜 has size at most k, then #(equationScope 𝓜) ≤ k * #𝓜.

theorem Cslib.BitString.equationScope_restrictMonomials_subset_sdiff {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (b : ι → Bool) (𝓜 : Finset (Finset ι)) : equationScope (restrictMonomials S b 𝓜) ⊆ equationScope 𝓜 \ S

After specializing S, the variable scope of restrictMonomials S b 𝓜 is contained in equationScope 𝓜 \ S.

theorem Cslib.BitString.varIncidence_equationScope_restrictMonomials_heavyVars_le {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (U : Finset ι) (F : Finset κ) (P : κ → Finset (Finset ι)) (b₀ : ℕ) (hU : ∀ i ∈ F, equationScope (P i) ⊆ U) (b : ι → Bool) (v : ι) : varIncidence F (fun (i : κ) => equationScope (restrictMonomials (heavyVars U F (fun (i : κ) => equationScope (P i)) b₀) b (P i))) v ≤ b₀

§5.5 (post-branching incidence bound): after branching on the heavy variables S = heavyVars U F (fun i => equationScope (P i)) b₀, every variable v : ι appears in at most b₀ reduced scopes equationScope (restrictMonomials S b (P i)) (i ∈ F).

theorem Cslib.BitString.card_branchAssignments_heavyVars_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (U : Finset ι) (F : Finset κ) (scope : κ → Finset ι) {b₀ : ℕ} (hb₀ : 0 < b₀) (hU : ∀ i ∈ F, scope i ⊆ U) : (branchAssignments (heavyVars U F scope b₀)).card ≤ 2 ^ (totalIncidence F scope / b₀)

§5.5 (heavy-variable branch count bound): for b₀ > 0, the number of canonical branches on heavyVars U F scope b₀ is at most 2 ^ (totalIncidence F scope / b₀).

theorem Cslib.BitString.commonZeroCount_eq_sum_branches {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (S : Finset ι) (I : Finset κ) (P : κ → Finset (Finset ι)) : commonZeroCount I P = ∑ b ∈ branchAssignments S, {y ∈ subproblemAssignments S | IsCommonZero I (fun (i : κ) => restrictMonomials S b (P i)) y}.card

§5.5 (additive branch decomposition of commonZeroCount): branching over all canonical assignments b ∈ branchAssignments S to S partitions commonZeroCount I P into the sum of common-zero counts on subproblemAssignments S of the reduced systems fun i => restrictMonomials S b (P i).

6. Cleared-denominator homogenization and ℓ₁-norm bounds (§5.4 & Appendix B.2)

noncomputable def Cslib.BitString.parityBaseDigitCleared {A : Type u_5} [CommRing A] (ℓ j : ℕ) (Δ A_i : A) : A

Cleared-denominator evaluation a_j * Δ + b_j * A_i of parityBaseDigit ℓ j = a_j + b_j X at L_i = A_i / Δ.

theorem Cslib.BitString.parityBaseDigitCleared_mul {A : Type u_5} [CommRing A] (ℓ j : ℕ) (Δ y : A) : parityBaseDigitCleared ℓ j Δ (Δ * y) = Δ * Polynomial.evalInt y (Polynomial.parityBaseDigit ℓ j)

Homogenization of parityBaseDigit ℓ j: parityBaseDigitCleared ℓ j Δ (Δ * y) = Δ * evalInt y (parityBaseDigit ℓ j).

def Cslib.BitString.hPolyCleared {A : Type u_5} [CommRing A] (Δ A_i : A) : A

Cleared-denominator evaluation A_i * (A_i - Δ) of hPoly = X ^ 2 - X at L_i = A_i / Δ.

theorem Cslib.BitString.hPolyCleared_mul {A : Type u_5} [CommRing A] (Δ y : A) : hPolyCleared Δ (Δ * y) = Δ ^ 2 * Polynomial.evalInt y Polynomial.hPoly

Homogenization of hPoly: hPolyCleared Δ (Δ * y) = Δ ^ 2 * evalInt y hPoly.

noncomputable def Cslib.BitString.parityFactorCleared {A : Type u_5} [CommRing A] (ℓ : ℕ) (Δ A_i : A) : Polynomial A

The cleared-denominator parity factor Γ B_i(V) with uniform factor denominator Γ = Δ ^ (2 * ℓ - 1): ∑ j ∈ range ℓ, C (Δ ^ (2 * (ℓ - 1 - j)) * parityBaseDigitCleared ℓ j Δ A_i * hPolyCleared Δ A_i ^ j) * X ^ j.

theorem Cslib.BitString.coeff_parityFactorCleared {A : Type u_5} [CommRing A] (ℓ : ℕ) (Δ A_i : A) (s : ℕ) : (parityFactorCleared ℓ Δ A_i).coeff s = if s < ℓ then Δ ^ (2 * (ℓ - 1 - s)) * parityBaseDigitCleared ℓ s Δ A_i * hPolyCleared Δ A_i ^ s else 0

The s-th coefficient of parityFactorCleared ℓ Δ A_i.

theorem Cslib.BitString.parityFactorCleared_mul {A : Type u_5} [CommRing A] {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (Δ y : A) : parityFactorCleared ℓ Δ (Δ * y) = Polynomial.C (Δ ^ (2 * ℓ - 1)) * Polynomial.parityFactor ℓ y

§5.4 & Appendix B.2 (single-factor denominator clearing, $\Gamma = \Delta^{2\ell-1}$): for ℓ ≥ 1, parityFactorCleared ℓ Δ (Δ * y) = C (Δ ^ (2 * ℓ - 1)) * parityFactor ℓ y.

theorem Cslib.BitString.prod_parityFactorCleared_mul {κ : Type u_2} {A : Type u_5} [CommRing A] (I : Finset κ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (Δ : A) (y : κ → A) : ∏ i ∈ I, parityFactorCleared ℓ Δ (Δ * y i) = Polynomial.C ((Δ ^ (2 * ℓ - 1)) ^ I.card) * ∏ i ∈ I, Polynomial.parityFactor ℓ (y i)

§5.4 & Appendix B.2 (product denominator clearing, $\Omega = \Gamma^{\#I}$): for ℓ ≥ 1, the product of cleared factors over i ∈ I equals C ((Δ ^ (2 * ℓ - 1)) ^ #I) times the product of parityFactor ℓ (y i).

theorem Cslib.BitString.sumCoeffsBelow_C_mul {A : Type u_5} [CommRing A] (c : A) (p : Polynomial A) (m : ℕ) : Polynomial.sumCoeffsBelow m (Polynomial.C c * p) = c * Polynomial.sumCoeffsBelow m p

Scaling a polynomial by C c scales sumCoeffsBelow m by c.

theorem Cslib.BitString.sumCoeffsBelow_prod_parityFactorCleared_mul {κ : Type u_2} {A : Type u_5} [CommRing A] (I : Finset κ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (Δ : A) (y : κ → A) (m : ℕ) : Polynomial.sumCoeffsBelow m (∏ i ∈ I, parityFactorCleared ℓ Δ (Δ * y i)) = (Δ ^ (2 * ℓ - 1)) ^ I.card * Polynomial.sumCoeffsBelow m (∏ i ∈ I, Polynomial.parityFactor ℓ (y i))

§5.4 (truncated cleared-denominator product): for ℓ ≥ 1, the sum of the first m coefficients of ∏ i ∈ I, parityFactorCleared ℓ Δ (Δ * y i) equals (Δ ^ (2 * ℓ - 1)) ^ #I times the sum of the first m coefficients of ∏ i ∈ I, parityFactor ℓ (y i).

noncomputable def Cslib.BitString.clearedMonomialPoly {ι : Type u_1} (d_den : ℤ) (k : ℕ) (θ : ι → Polynomial ℤ) (M : Finset ι) : Polynomial ℤ

The cleared-denominator monomial C (d_den ^ (k - #M)) * ∏ v ∈ M, θ v in ℤ[X] for a monomial M of degree at most k when each input has denominator d_den.

noncomputable def Cslib.BitString.clearedMonomialSumPoly {ι : Type u_1} (d_den : ℤ) (k : ℕ) (θ : ι → Polynomial ℤ) (𝓜 : Finset (Finset ι)) : Polynomial ℤ

The cleared-denominator monomial sum A_i = ∑ M ∈ 𝓜, clearedMonomialPoly d_den k θ M in ℤ[X].

theorem Cslib.BitString.coeffNorm1_clearedMonomialPoly_le {ι : Type u_1} {d_den : ℤ} {k B₀ : ℕ} {θ : ι → Polynomial ℤ} {M : Finset ι} (hd : d_den.natAbs ≤ B₀) (hM : M.card ≤ k) (hθ : ∀ v ∈ M, (θ v).coeffNorm1 ≤ B₀) : (clearedMonomialPoly d_den k θ M).coeffNorm1 ≤ B₀ ^ k

Appendix B.2 (monomial numerator norm bound): if d_den.natAbs ≤ B₀, #M ≤ k, and every θ v (v ∈ M) has coeffNorm1 (θ v) ≤ B₀, then coeffNorm1 (clearedMonomialPoly d_den k θ M) ≤ B₀ ^ k.

theorem Cslib.BitString.coeffNorm1_clearedMonomialSumPoly_le {ι : Type u_1} {d_den : ℤ} {k B₀ : ℕ} {θ : ι → Polynomial ℤ} {𝓜 : Finset (Finset ι)} (hd : d_den.natAbs ≤ B₀) (hk : ∀ M ∈ 𝓜, M.card ≤ k) (hθ : ∀ M ∈ 𝓜, ∀ v ∈ M, (θ v).coeffNorm1 ≤ B₀) : (clearedMonomialSumPoly d_den k θ 𝓜).coeffNorm1 ≤ 𝓜.card * B₀ ^ k

Appendix B.2 (equation numerator norm bound ∥Δ L_i∥₁ ≤ #𝓜 * B₀ ^ k): under the same hypotheses for all M ∈ 𝓜, coeffNorm1 (clearedMonomialSumPoly d_den k θ 𝓜) ≤ #𝓜 * B₀ ^ k.

theorem Cslib.BitString.coeffNorm1_parityBaseDigitCleared_le (ℓ j : ℕ) (Δ : ℤ) {A_i : Polynomial ℤ} {B : ℕ} (hA : A_i.coeffNorm1 ≤ B) : (parityBaseDigitCleared ℓ j (Polynomial.C Δ) A_i).coeffNorm1 ≤ (Polynomial.parityBaseDigit ℓ j).coeffNorm1 * (B + Δ.natAbs)

Appendix B.2 (∥Δ e_j(L_i)∥₁ bound): if coeffNorm1 A_i ≤ B, then coeffNorm1 (parityBaseDigitCleared ℓ j (C Δ) A_i) ≤ coeffNorm1 (parityBaseDigit ℓ j) * (B + Δ.natAbs).

theorem Cslib.BitString.coeffNorm1_hPolyCleared_le (Δ : ℤ) {A_i : Polynomial ℤ} {B : ℕ} (hA : A_i.coeffNorm1 ≤ B) : (hPolyCleared (Polynomial.C Δ) A_i).coeffNorm1 ≤ B * (B + Δ.natAbs)

Appendix B.2 (∥A_i (A_i - Δ)∥₁ bound): if coeffNorm1 A_i ≤ B, then coeffNorm1 (hPolyCleared (C Δ) A_i) ≤ B * (B + Δ.natAbs).

theorem Cslib.BitString.coeffNorm1_coeff_parityFactorCleared_le (ℓ : ℕ) (Δ : ℤ) {A_i : Polynomial ℤ} {B : ℕ} (hA : A_i.coeffNorm1 ≤ B) (s : ℕ) : ((parityFactorCleared ℓ (Polynomial.C Δ) A_i).coeff s).coeffNorm1 ≤ (Polynomial.parityBaseDigit ℓ s).coeffNorm1 * (B + Δ.natAbs) ^ (2 * ℓ - 1)

Appendix B.2 (∥[V ^ s] (Γ B_i)∥₁ bound): if coeffNorm1 A_i ≤ B, then every V ^ s- coefficient of parityFactorCleared ℓ (C Δ) A_i has coeffNorm1 at most coeffNorm1 (parityBaseDigit ℓ s) * (B + Δ.natAbs) ^ (2 * ℓ - 1).

theorem Cslib.BitString.coeffNorm1_coeff_parityFactorCleared_le_explicit (ℓ : ℕ) (Δ : ℤ) {A_i : Polynomial ℤ} {B : ℕ} (hA : A_i.coeffNorm1 ≤ B) (s : ℕ) : ((parityFactorCleared ℓ (Polynomial.C Δ) A_i).coeff s).coeffNorm1 ≤ 2 * ((2 * ℓ) ^ s * 2 ^ (3 * ℓ)) * (B + Δ.natAbs) ^ (2 * ℓ - 1)

Appendix B.2 (explicit ∥[V ^ s] (Γ B_i)∥₁ bound): combining coeffNorm1_coeff_parityFactorCleared_le with coeffNorm1_parityBaseDigit_le yields the explicit exponential bound 2 * ((2 * ℓ) ^ s * 2 ^ (3 * ℓ)) * (B + Δ.natAbs) ^ (2 * ℓ - 1) for every V ^ s-coefficient of parityFactorCleared ℓ (C Δ) A_i.