Rational-to-cleared-denominator specialization and exact division recovery

This module bridges the rational replacement polynomials of Section 5.3–5.4 and the cleared-denominator integer interpolation pipeline of Section 5.4 and Appendix B.2–B.3 of OpenAI, The Exponential Time Hypothesis is False (pp. 37–39, 48–50):

1. Cleared-denominator evaluation at $T = 0$, ring homogenization, and natDegree bounds (§5.3–5.4 & Appendix B.2): When every monomial $M \in \mathcal{P}_i$ has size $\#M \le k$ and each variable $v \in M$ in equation $i \in I$ has an integer numerator polynomial $\theta_{x, i, v}(T) \in \mathbb{Z}[T]$ over a common denominator $d_{\mathrm{den}} \in \mathbb{Z}$ satisfying $\theta_{x, i, v}(0) = d_{\mathrm{den}} \cdot \mathrm{bitVal}_{\mathbb{Z}}(x_v)$ and $\deg_T \theta_{x, i, v} \le R_{\mathrm{deg}}$, the cleared-denominator equation polynomial Cslib.BitString.clearedMonomialSumPoly has natDegree ≤ k * R_deg, evaluates at $T = 0$ to $d_{\mathrm{den}}^k \cdot \mathrm{monomialSum}_{\mathbb{Z}}(\mathcal{P}_i, x)$, and maps into any commutative ring $R$ as C ((d_den : R) ^ k) times Cslib.BitString.univariateMonomialSumPoly whenever (θ x i v).map (Int.castRingHom R) = C (d_den : R) * q x i v for all $M \in \mathcal{P}_i$ and $v \in M$.
2. Cube-summed cleared-denominator polynomials $\tilde{H}_s(T) = \Omega [V^s] H(T)$ and exact integer division recovery (§5.4 & Appendix B.3, eq. B.1): Summing the cleared parity-factor products over $x \in \{0, 1\}^\iota$ yields Cslib.BitString.univariateClearedParityProduct, its $V^s$-coordinates Cslib.BitString.univariateClearedParityCoord ($\tilde{H}_s(T) \in \mathbb{Z}[T]$), and its truncated sum Cslib.BitString.univariateClearedParityTruncatedSum. Over any field $K$ with $(d_{\mathrm{den}} : K) \neq 0$, $1 \le \ell$, and $\forall i \in I, \forall M \in \mathcal{P}_i, \#M \le k$, $\tilde{H}_s(T)$ maps into $K[T]$ as the common product denominator $\Omega = (d_{\mathrm{den}}^k)^{(2\ell - 1)\#I}$ (Cslib.BitString.clearedProductDenom) times the rational coordinate polynomial [V^s] H(T) associated to the rational replacement family Cslib.BitString.divDenomReplacement ($r_{x, i, v}(T) = d_{\mathrm{den}}^{-1} \theta_{x, i, v}(T)$). At $T = 0$, when $1 \le \ell$, $\#M \le k$, and $\theta_{x, i, v}(0) = d_{\mathrm{den}} \cdot \mathrm{bitVal}_{\mathbb{Z}}(x_v)$, $\tilde{H}_s(0)$ is an exact integer multiple of $\Omega$; when $d_{\mathrm{den}} \neq 0$ and Fintype.card ι < ℓ (and $D_H \neq 0$ for Cramer determinant recovery), dividing each $\tilde{H}_s(0)$ (or Cramer's rule determinant numerator $N_{H, s} = D_H \tilde{H}_s(0)$ in eq. B.1) by $\Omega$ (or $\Omega D_H$), summing over $0 \le s < \ell$, and reducing modulo $2^\ell$ recovers commonZeroCount I P on the nose, both on a single problem and summed across all heavy-variable branches at shared precision $\ell = n + 1$.

Main definitions

• Cslib.BitString.clearedProductDenom: the product denominator $\Omega = ((d_{\mathrm{den}}^k)^{2\ell - 1})^{m_{\mathrm{test}}}$.
• Cslib.BitString.univariateClearedParityProduct, Cslib.BitString.univariateClearedParityCoord, Cslib.BitString.univariateClearedParityTruncatedSum: the cube-summed cleared-denominator bivariate polynomial $\tilde{H}(T, V) \in \mathbb{Z}[T][V]$, its $V^s$-coordinate polynomials $\tilde{H}_s(T) \in \mathbb{Z}[T]$, and its truncated sum $S_\ell(\tilde{H}(T)) \in \mathbb{Z}[T]$.
• Cslib.BitString.divDenomReplacement: the rational replacement family $r_{x, i, v}(T) = d_{\mathrm{den}}^{-1} \theta_{x, i, v}(T) \in K[T]$.

Main results

• Cslib.BitString.eval_zero_clearedMonomialSumPoly, Cslib.BitString.map_clearedMonomialSumPoly, Cslib.BitString.natDegree_clearedMonomialSumPoly_le: $T = 0$ evaluation, ring homogenization, and natDegree bound for cleared-denominator equation polynomials.
• Cslib.BitString.natDegree_univariateClearedParityCoord_le, Cslib.BitString.natDegree_univariateClearedParityTruncatedSum_le: equation (5.5a) natDegree bounds for $\tilde{H}_s(T)$ and $S_\ell(\tilde{H}(T))$.
• Cslib.BitString.map_univariateClearedParityCoord_divDenomReplacement, Cslib.BitString.map_univariateClearedParityTruncatedSum_divDenomReplacement: over any field $K$ with $(d_{\mathrm{den}} : K) \neq 0$, $1 \le \ell$, and monomial degree at most $k$, $\tilde{H}_s(T) = \Omega [V^s] H(T)$ and $S_\ell(\tilde{H}(T)) = \Omega S_\ell(H(T))$.
• Cslib.BitString.bivariateCoeffNorm1_parityFactorCleared_le, Cslib.BitString.bivariateCoeffNorm1_prod_parityFactorCleared_le, Cslib.BitString.coeffNorm1_univariateClearedParityCoord_le: Appendix B.2 bivariate and coordinate ℓ₁-norm bounds for cleared parity factors and $\tilde{H}_s(T)$.
• Cslib.BitString.eval_zero_univariateClearedParityCoord, Cslib.BitString.ediv_eval_zero_univariateClearedParityCoord, Cslib.BitString.emod_sum_ediv_eval_zero_univariateClearedParityCoord_eq_commonZeroCount, Cslib.BitString.emod_ediv_eval_zero_univariateClearedParityTruncatedSum_eq_commonZeroCount: exact integer divisibility by $\Omega$ at $T = 0$ and exact modular recovery of commonZeroCount.
• Cslib.BitString.emod_sum_cramer_ediv_eq_commonZeroCount: Appendix B.3 (eq. B.1) exact integer division recovery from Cramer's rule determinant numerators $N_{H, s} = D_H \tilde{H}_s(0)$ when $d_{\mathrm{den}} \neq 0$, $D_H \neq 0$, and Fintype.card ι < ℓ.
• Cslib.BitString.commonZeroCount_eq_sum_branch_emod_ediv_cleared: §5.5 branch-summed exact recovery from cleared-denominator branch polynomials at shared precision $\ell = n + 1$.

References

• OpenAI, The Exponential Time Hypothesis is False (Sections 5.3–5.5 and Appendix B.2–B.3)

1. Ring-homomorphism transport and natDegree bounds for cleared parity factors

theorem Cslib.BitString.map_parityBaseDigitCleared {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] (φ : A →+* B) (ℓ j : ℕ) (Δ A_i : A) : φ (parityBaseDigitCleared ℓ j Δ A_i) = parityBaseDigitCleared ℓ j (φ Δ) (φ A_i)

Any ring homomorphism φ : A →+* B commutes with parityBaseDigitCleared.

theorem Cslib.BitString.map_hPolyCleared {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] (φ : A →+* B) (Δ A_i : A) : φ (hPolyCleared Δ A_i) = hPolyCleared (φ Δ) (φ A_i)

Any ring homomorphism φ : A →+* B commutes with hPolyCleared.

theorem Cslib.BitString.map_parityFactorCleared {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] (φ : A →+* B) (ℓ : ℕ) (Δ A_i : A) : Polynomial.map φ (parityFactorCleared ℓ Δ A_i) = parityFactorCleared ℓ (φ Δ) (φ A_i)

Mapping parityFactorCleared ℓ Δ A_i coefficientwise by φ : A →+* B yields parityFactorCleared ℓ (φ Δ) (φ A_i).

theorem Cslib.BitString.eval_coeff_prod_parityFactorCleared {κ : Type u_2} {R : Type u_3} [CommRing R] (I : Finset κ) (ℓ : ℕ) (Δ : Polynomial R) (A_i : κ → Polynomial R) (s : ℕ) (t : R) : Polynomial.eval t ((∏ i ∈ I, parityFactorCleared ℓ Δ (A_i i)).coeff s) = (∏ i ∈ I, parityFactorCleared ℓ (Polynomial.eval t Δ) (Polynomial.eval t (A_i i))).coeff s

Evaluating the s-th coefficient of ∏ i ∈ I, parityFactorCleared ℓ Δ (A_i i) at t : R agrees with the s-th coefficient of ∏ i ∈ I, parityFactorCleared ℓ (Δ.eval t) ((A_i i).eval t).

theorem Cslib.BitString.natDegree_parityBaseDigitCleared_le {R : Type u_3} [CommRing R] (ℓ j : ℕ) (Δ A_i : Polynomial R) {d : ℕ} (hΔ : Δ.natDegree = 0) (hA : A_i.natDegree ≤ d) : (parityBaseDigitCleared ℓ j Δ A_i).natDegree ≤ d

When Δ has natDegree = 0 and A_i has natDegree ≤ d, parityBaseDigitCleared ℓ j Δ A_i has natDegree ≤ d.

theorem Cslib.BitString.natDegree_hPolyCleared_le {R : Type u_3} [CommRing R] (Δ A_i : Polynomial R) {d : ℕ} (hΔ : Δ.natDegree = 0) (hA : A_i.natDegree ≤ d) : (hPolyCleared Δ A_i).natDegree ≤ 2 * d

When Δ has natDegree = 0 and A_i has natDegree ≤ d, hPolyCleared Δ A_i has natDegree ≤ 2 * d.

theorem Cslib.BitString.natDegree_coeff_parityFactorCleared_le {R : Type u_3} [CommRing R] (ℓ : ℕ) (Δ A_i : Polynomial R) {d : ℕ} (hΔ : Δ.natDegree = 0) (hA : A_i.natDegree ≤ d) (s : ℕ) : ((parityFactorCleared ℓ Δ A_i).coeff s).natDegree ≤ d * (1 + 2 * s)

When Δ has natDegree = 0 and A_i has natDegree ≤ d, the s-th coefficient of parityFactorCleared ℓ Δ A_i has natDegree ≤ d * (1 + 2 * s).

theorem Cslib.BitString.natDegree_coeff_prod_parityFactorCleared_le {κ : Type u_2} {R : Type u_3} [CommRing R] (I : Finset κ) (ℓ : ℕ) (Δ : Polynomial R) (A_i : κ → Polynomial R) {d : ℕ} (hΔ : Δ.natDegree = 0) (hA : ∀ i ∈ I, (A_i i).natDegree ≤ d) (s : ℕ) : ((∏ i ∈ I, parityFactorCleared ℓ Δ (A_i i)).coeff s).natDegree ≤ d * (I.card + 2 * s)

Lemma 5.2 (cleared-denominator univariate natDegree bound): if Δ.natDegree = 0 and every A_i i (i ∈ I) has natDegree ≤ d, then the s-th coefficient of ∏ i ∈ I, parityFactorCleared ℓ Δ (A_i i) has natDegree ≤ d * (#I + 2 * s).

theorem Cslib.BitString.natDegree_coeff_prod_parityFactorCleared_le_of_lt {κ : Type u_2} {R : Type u_3} [CommRing R] (I : Finset κ) {ℓ s d : ℕ} (Δ : Polynomial R) (A_i : κ → Polynomial R) (hΔ : Δ.natDegree = 0) (hA : ∀ i ∈ I, (A_i i).natDegree ≤ d) (hs : s < ℓ) : ((∏ i ∈ I, parityFactorCleared ℓ Δ (A_i i)).coeff s).natDegree ≤ d * (I.card + 2 * (ℓ - 1))

For s < ℓ, the s-th coefficient of ∏ i ∈ I, parityFactorCleared ℓ Δ (A_i i) has natDegree ≤ d * (#I + 2 * (ℓ - 1)).

2. Cleared-denominator monomials and equations: $T = 0$ evaluation, ring homogenization,

and natDegree bounds (§5.3–5.4 & Appendix B.2)

theorem Cslib.BitString.eval_clearedMonomialPoly {ι : Type u_1} (d_den : ℤ) (k : ℕ) (θ : ι → Polynomial ℤ) (M : Finset ι) (t : ℤ) : Polynomial.eval t (clearedMonomialPoly d_den k θ M) = d_den ^ (k - M.card) * ∏ v ∈ M, Polynomial.eval t (θ v)

Evaluating clearedMonomialPoly d_den k θ M at t : ℤ yields d_den ^ (k - #M) * ∏ v ∈ M, (θ v).eval t.

theorem Cslib.BitString.eval_zero_clearedMonomialPoly {ι : Type u_1} (d_den : ℤ) {k : ℕ} (θ : ι → Polynomial ℤ) {M : Finset ι} (x : ι → Bool) (hM : M.card ≤ k) (hθ : ∀ v ∈ M, Polynomial.eval 0 (θ v) = d_den * bitVal ℤ (x v)) : Polynomial.eval 0 (clearedMonomialPoly d_den k θ M) = d_den ^ k * monomial ℤ M x

At T = 0, if #M ≤ k and every θ v (v ∈ M) evaluates to d_den * bitVal ℤ (x v), then clearedMonomialPoly d_den k θ M evaluates to d_den ^ k * monomial ℤ M x.

theorem Cslib.BitString.eval_zero_clearedMonomialSumPoly {ι : Type u_1} (d_den : ℤ) {k : ℕ} (θ : ι → Polynomial ℤ) {𝓜 : Finset (Finset ι)} (x : ι → Bool) (hk : ∀ M ∈ 𝓜, M.card ≤ k) (hθ : ∀ M ∈ 𝓜, ∀ v ∈ M, Polynomial.eval 0 (θ v) = d_den * bitVal ℤ (x v)) : Polynomial.eval 0 (clearedMonomialSumPoly d_den k θ 𝓜) = d_den ^ k * monomialSum ℤ 𝓜 x

§5.3–5.4 ($T = 0$ evaluation of cleared equation polynomial): at T = 0, if every M ∈ 𝓜 has #M ≤ k and every θ v (v ∈ M) evaluates to d_den * bitVal ℤ (x v), then clearedMonomialSumPoly d_den k θ 𝓜 evaluates to d_den ^ k * monomialSum ℤ 𝓜 x.

theorem Cslib.BitString.map_clearedMonomialPoly {ι : Type u_1} {R : Type u_3} [CommRing R] (d_den : ℤ) {k : ℕ} (θ : ι → Polynomial ℤ) (q : ι → Polynomial R) {M : Finset ι} (hM : M.card ≤ k) (hq : ∀ v ∈ M, Polynomial.map (Int.castRingHom R) (θ v) = Polynomial.C ↑d_den * q v) : Polynomial.map (Int.castRingHom R) (clearedMonomialPoly d_den k θ M) = Polynomial.C (↑d_den ^ k) * univariateMonomialPoly R q M

Mapping clearedMonomialPoly d_den k θ M into R[X] when #M ≤ k and (θ v).map (Int.castRingHom R) = C (d_den : R) * q v yields C ((d_den : R) ^ k) * univariateMonomialPoly R q M.

theorem Cslib.BitString.map_clearedMonomialSumPoly {ι : Type u_1} {R : Type u_3} [CommRing R] (d_den : ℤ) {k : ℕ} (θ : ι → Polynomial ℤ) (q : ι → Polynomial R) {𝓜 : Finset (Finset ι)} (hk : ∀ M ∈ 𝓜, M.card ≤ k) (hq : ∀ M ∈ 𝓜, ∀ v ∈ M, Polynomial.map (Int.castRingHom R) (θ v) = Polynomial.C ↑d_den * q v) : Polynomial.map (Int.castRingHom R) (clearedMonomialSumPoly d_den k θ 𝓜) = Polynomial.C (↑d_den ^ k) * univariateMonomialSumPoly R q 𝓜

§5.4 (ring homogenization of cleared equation polynomial): mapping clearedMonomialSumPoly d_den k θ 𝓜 into R[X] when ∀ M ∈ 𝓜, #M ≤ k and (θ v).map (Int.castRingHom R) = C (d_den : R) * q v yields C ((d_den : R) ^ k) * univariateMonomialSumPoly R q 𝓜.

theorem Cslib.BitString.natDegree_clearedMonomialPoly_le {ι : Type u_1} (d_den : ℤ) (k : ℕ) (θ : ι → Polynomial ℤ) {M : Finset ι} {R_deg : ℕ} (hθ : ∀ v ∈ M, (θ v).natDegree ≤ R_deg) : (clearedMonomialPoly d_den k θ M).natDegree ≤ M.card * R_deg

If every θ v (v ∈ M) has natDegree ≤ R_deg, then clearedMonomialPoly d_den k θ M has natDegree ≤ #M * R_deg.

theorem Cslib.BitString.natDegree_clearedMonomialSumPoly_le {ι : Type u_1} (d_den : ℤ) {k R_deg : ℕ} (θ : ι → Polynomial ℤ) {𝓜 : Finset (Finset ι)} (hk : ∀ M ∈ 𝓜, M.card ≤ k) (hθ : ∀ M ∈ 𝓜, ∀ v ∈ M, (θ v).natDegree ≤ R_deg) : (clearedMonomialSumPoly d_den k θ 𝓜).natDegree ≤ k * R_deg

If every M ∈ 𝓜 has #M ≤ k and every θ v (v ∈ M) has natDegree ≤ R_deg, then clearedMonomialSumPoly d_den k θ 𝓜 has natDegree ≤ k * R_deg.

3. Cube-summed cleared-denominator polynomials $\tilde{H}_s(T) = \Omega [V^s] H(T)$ and

exact integer division recovery (§5.4 & Appendix B.2–B.3)

def Cslib.BitString.clearedProductDenom (d_den : ℤ) (k ℓ m_test : ℕ) : ℤ

The common product denominator $\Omega = \Gamma^{m_{\mathrm{test}}} = ((d_{\mathrm{den}}^k)^{2\ell - 1})^{m_{\mathrm{test}}}$ of the product of $m_{\mathrm{test}}$ cleared parity factors (§5.4 and Appendix B.2).

theorem Cslib.BitString.clearedProductDenom_ne_zero {d_den : ℤ} (hd : d_den ≠ 0) (k ℓ m_test : ℕ) : clearedProductDenom d_den k ℓ m_test ≠ 0

When d_den ≠ 0, clearedProductDenom d_den k ℓ m_test ≠ 0.

noncomputable def Cslib.BitString.univariateClearedParityProduct {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) (k ℓ : ℕ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) : Polynomial (Polynomial ℤ)

The cube-summed cleared-denominator bivariate polynomial $\tilde{H}(T, V) = \sum_{x \in \{0, 1\}^\iota} \prod_{i \in I} (\Gamma B_i)(T, V)$ in Polynomial (Polynomial ℤ) (ℤ[T][V]).

noncomputable def Cslib.BitString.univariateClearedParityCoord {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) (k ℓ : ℕ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (s : ℕ) : Polynomial ℤ

The $V^s$-coordinate polynomial $\tilde{H}_s(T) = [V^s] \tilde{H}(T) \in \mathbb{Z}[T]$.

theorem Cslib.BitString.univariateClearedParityCoord_eq_sum {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) (k ℓ : ℕ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (s : ℕ) : univariateClearedParityCoord I P d_den k ℓ θ s = ∑ x : ι → Bool, (∏ i ∈ I, parityFactorCleared ℓ (Polynomial.C (d_den ^ k)) (clearedMonomialSumPoly d_den k (θ x i) (P i))).coeff s

Explicit cube-sum expansion of univariateClearedParityCoord.

noncomputable def Cslib.BitString.univariateClearedParityTruncatedSum {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) (k ℓ : ℕ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) : Polynomial ℤ

The truncated coefficient sum $S_\ell(\tilde{H}(T)) = \sum_{s < \ell} \tilde{H}_s(T) \in \mathbb{Z}[T]$.

theorem Cslib.BitString.univariateClearedParityTruncatedSum_eq_sum_coord {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) (k ℓ : ℕ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) : univariateClearedParityTruncatedSum I P d_den k ℓ θ = ∑ s ∈ Finset.range ℓ, univariateClearedParityCoord I P d_den k ℓ θ s

univariateClearedParityTruncatedSum is the sum of univariateClearedParityCoord over s ∈ range ℓ.

theorem Cslib.BitString.natDegree_univariateClearedParityCoord_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) (k ℓ : ℕ) {R_deg s : ℕ} (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hθ : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (θ x i v).natDegree ≤ R_deg) (hs : s < ℓ) : (univariateClearedParityCoord I P d_den k ℓ θ s).natDegree ≤ k * R_deg * (I.card + 2 * (ℓ - 1))

Equation (5.5a) (cleared-denominator coordinate natDegree bound): for s < ℓ, if every equation P i (i ∈ I) has degree at most k and every numerator θ x i v has natDegree ≤ R_deg, then univariateClearedParityCoord I P d_den k ℓ θ s has natDegree ≤ (k * R_deg) * (#I + 2 * (ℓ - 1)).

theorem Cslib.BitString.natDegree_univariateClearedParityTruncatedSum_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) (k ℓ : ℕ) {R_deg : ℕ} (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hθ : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (θ x i v).natDegree ≤ R_deg) : (univariateClearedParityTruncatedSum I P d_den k ℓ θ).natDegree ≤ k * R_deg * (I.card + 2 * (ℓ - 1))

Equation (5.5a) (cleared-denominator truncated-sum natDegree bound): under the same hypotheses, univariateClearedParityTruncatedSum I P d_den k ℓ θ has natDegree ≤ (k * R_deg) * (#I + 2 * (ℓ - 1)).

theorem Cslib.BitString.map_univariateClearedParityCoord {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) {k ℓ : ℕ} (hℓ : 1 ≤ ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (q : (ι → Bool) → κ → ι → Polynomial R) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hq : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.map (Int.castRingHom R) (θ x i v) = Polynomial.C ↑d_den * q x i v) (s : ℕ) : Polynomial.map (Int.castRingHom R) (univariateClearedParityCoord I P d_den k ℓ θ s) = Polynomial.C ↑(clearedProductDenom d_den k ℓ I.card) * univariateParityCoord I P ℓ q s

§5.4 & Appendix B.2–B.3 (homogenization of $\tilde{H}_s(T) = \Omega [V^s] H(T)$): for 1 ≤ ℓ, if ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k and every numerator θ x i v maps into R[X] as C (d_den : R) * q x i v, then mapping univariateClearedParityCoord I P d_den k ℓ θ s into R[X] gives C (clearedProductDenom d_den k ℓ #I : R) * univariateParityCoord I P ℓ q s.

theorem Cslib.BitString.map_univariateClearedParityTruncatedSum {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) {k ℓ : ℕ} (hℓ : 1 ≤ ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (q : (ι → Bool) → κ → ι → Polynomial R) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hq : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.map (Int.castRingHom R) (θ x i v) = Polynomial.C ↑d_den * q x i v) : Polynomial.map (Int.castRingHom R) (univariateClearedParityTruncatedSum I P d_den k ℓ θ) = Polynomial.C ↑(clearedProductDenom d_den k ℓ I.card) * univariateParityTruncatedSum I P ℓ q

§5.4 & Appendix B.2–B.3 (homogenization of $S_\ell(\tilde{H}(T)) = \Omega S_\ell(H(T))$ over R[X]): under the same hypotheses, mapping univariateClearedParityTruncatedSum I P d_den k ℓ θ into R[X] gives C (clearedProductDenom d_den k ℓ #I : R) * univariateParityTruncatedSum I P ℓ q.

noncomputable def Cslib.BitString.divDenomReplacement {ι : Type u_1} {κ : Type u_2} (K : Type u_4) [Field K] (d_den : ℤ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (x : ι → Bool) (i : κ) (v : ι) : Polynomial K

The rational replacement family $r_{x, i, v}(T) = d_{\mathrm{den}}^{-1} \theta_{x, i, v}(T) \in K[T]$ over a field $K$ associated to an integer numerator family $\theta$ with common denominator $d_{\mathrm{den}}$.

theorem Cslib.BitString.C_mul_divDenomReplacement {ι : Type u_1} {κ : Type u_2} {K : Type u_4} [Field K] {d_den : ℤ} (hd : ↑d_den ≠ 0) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (x : ι → Bool) (i : κ) (v : ι) : Polynomial.map (Int.castRingHom K) (θ x i v) = Polynomial.C ↑d_den * divDenomReplacement K d_den θ x i v

Multiplying divDenomReplacement K d_den θ x i v by C (d_den : K) when (d_den : K) ≠ 0 recovers (θ x i v).map (Int.castRingHom K).

theorem Cslib.BitString.map_univariateClearedParityCoord_divDenomReplacement {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] {K : Type u_4} [Field K] (I : Finset κ) (P : κ → Finset (Finset ι)) {d_den : ℤ} (hd : ↑d_den ≠ 0) {k ℓ : ℕ} (hℓ : 1 ≤ ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (s : ℕ) : Polynomial.map (Int.castRingHom K) (univariateClearedParityCoord I P d_den k ℓ θ s) = Polynomial.C ↑(clearedProductDenom d_den k ℓ I.card) * univariateParityCoord I P ℓ (divDenomReplacement K d_den θ) s

§5.4 & Appendix B.3 ($\tilde{H}_s(T) = \Omega [V^s] H(T)$ over a field $K$): when (d_den : K) ≠ 0, 1 ≤ ℓ, and ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k, mapping univariateClearedParityCoord I P d_den k ℓ θ s into K[T] equals C (clearedProductDenom d_den k ℓ #I : K) times univariateParityCoord for divDenomReplacement K d_den θ.

theorem Cslib.BitString.map_univariateClearedParityTruncatedSum_divDenomReplacement {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] {K : Type u_4} [Field K] (I : Finset κ) (P : κ → Finset (Finset ι)) {d_den : ℤ} (hd : ↑d_den ≠ 0) {k ℓ : ℕ} (hℓ : 1 ≤ ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) : Polynomial.map (Int.castRingHom K) (univariateClearedParityTruncatedSum I P d_den k ℓ θ) = Polynomial.C ↑(clearedProductDenom d_den k ℓ I.card) * univariateParityTruncatedSum I P ℓ (divDenomReplacement K d_den θ)

§5.4 & Appendix B.3 ($S_\ell(\tilde{H}(T)) = \Omega S_\ell(H(T))$ over a field $K$): under the same hypotheses, mapping univariateClearedParityTruncatedSum I P d_den k ℓ θ into K[T] equals C (clearedProductDenom d_den k ℓ #I : K) times univariateParityTruncatedSum for divDenomReplacement K d_den θ.

theorem Cslib.BitString.eval_zero_univariateClearedParityCoord {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) {k ℓ : ℕ} (hℓ : 1 ≤ ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hθ : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.eval 0 (θ x i v) = d_den * bitVal ℤ (x v)) (s : ℕ) : Polynomial.eval 0 (univariateClearedParityCoord I P d_den k ℓ θ s) = clearedProductDenom d_den k ℓ I.card * ∑ x : ι → Bool, (∏ i ∈ I, Polynomial.parityFactor ℓ (monomialSum ℤ (P i) x)).coeff s

§5.4 & Appendix B.3 (exact integer factorization of $\tilde{H}_s(0)$ at $T = 0$): for 1 ≤ ℓ, if ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k and every θ x i v evaluates at 0 to d_den * bitVal ℤ (x v), then (univariateClearedParityCoord I P d_den k ℓ θ s).eval 0 equals clearedProductDenom d_den k ℓ #I times the integer value of [V^s] H(0).

theorem Cslib.BitString.eval_zero_univariateClearedParityTruncatedSum {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) {k ℓ : ℕ} (hℓ : 1 ≤ ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hθ : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.eval 0 (θ x i v) = d_den * bitVal ℤ (x v)) : Polynomial.eval 0 (univariateClearedParityTruncatedSum I P d_den k ℓ θ) = clearedProductDenom d_den k ℓ I.card * ∑ x : ι → Bool, Polynomial.sumCoeffsBelow ℓ (∏ i ∈ I, Polynomial.parityFactor ℓ (monomialSum ℤ (P i) x))

§5.4 & Appendix B.3 (exact integer factorization of $S_\ell(\tilde{H})(0)$ at $T = 0$): under the same hypotheses, (univariateClearedParityTruncatedSum I P d_den k ℓ θ).eval 0 equals clearedProductDenom d_den k ℓ #I times the integer value of $S_\ell(H(0))$.

theorem Cslib.BitString.dvd_eval_zero_univariateClearedParityCoord {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) {k ℓ : ℕ} (hℓ : 1 ≤ ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hθ : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.eval 0 (θ x i v) = d_den * bitVal ℤ (x v)) (s : ℕ) : clearedProductDenom d_den k ℓ I.card ∣ Polynomial.eval 0 (univariateClearedParityCoord I P d_den k ℓ θ s)

Appendix B.3 (exact divisibility of $\tilde{H}_s(0)$ by $\Omega$): under the hypotheses of eval_zero_univariateClearedParityCoord, clearedProductDenom d_den k ℓ #I divides (univariateClearedParityCoord I P d_den k ℓ θ s).eval 0 in ℤ.

theorem Cslib.BitString.ediv_eval_zero_univariateClearedParityCoord {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {d_den : ℤ} (hd : d_den ≠ 0) {k ℓ : ℕ} (hℓ : 1 ≤ ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hθ : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.eval 0 (θ x i v) = d_den * bitVal ℤ (x v)) (s : ℕ) : Polynomial.eval 0 (univariateClearedParityCoord I P d_den k ℓ θ s) / clearedProductDenom d_den k ℓ I.card = ∑ x : ι → Bool, (∏ i ∈ I, Polynomial.parityFactor ℓ (monomialSum ℤ (P i) x)).coeff s

Appendix B.3 (exact integer quotient $\tilde{H}_s(0) / \Omega = H_s(0)$): when in addition d_den ≠ 0, exact integer division of (univariateClearedParityCoord I P d_den k ℓ θ s).eval 0 by clearedProductDenom d_den k ℓ #I recovers the integer coefficient sum ∑ x : ι → Bool, (∏ i ∈ I, parityFactor ℓ (monomialSum ℤ (P i) x)).coeff s.

theorem Cslib.BitString.emod_sum_ediv_eval_zero_univariateClearedParityCoord_eq_commonZeroCount {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {d_den : ℤ} (hd : d_den ≠ 0) {k ℓ : ℕ} (hℓ : Fintype.card ι < ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hθ : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.eval 0 (θ x i v) = d_den * bitVal ℤ (x v)) : (∑ s ∈ Finset.range ℓ, Polynomial.eval 0 (univariateClearedParityCoord I P d_den k ℓ θ s) / clearedProductDenom d_den k ℓ I.card) % 2 ^ ℓ = ↑(commonZeroCount I P)

§5.4 & Appendix B.3 (exact modular recovery of commonZeroCount from coordinate quotients $\tilde{H}_s(0) / \Omega$): when Fintype.card ι < ℓ and d_den ≠ 0, summing the exact integer quotients (univariateClearedParityCoord I P d_den k ℓ θ s).eval 0 / Ω over s ∈ range ℓ and reducing modulo 2 ^ ℓ recovers commonZeroCount I P.

theorem Cslib.BitString.emod_ediv_eval_zero_univariateClearedParityTruncatedSum_eq_commonZeroCount {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {d_den : ℤ} (hd : d_den ≠ 0) {k ℓ : ℕ} (hℓ : Fintype.card ι < ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hθ : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.eval 0 (θ x i v) = d_den * bitVal ℤ (x v)) : Polynomial.eval 0 (univariateClearedParityTruncatedSum I P d_den k ℓ θ) / clearedProductDenom d_den k ℓ I.card % 2 ^ ℓ = ↑(commonZeroCount I P)

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

theorem Cslib.BitString.emod_sum_cramer_ediv_eq_commonZeroCount {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) {d_den D_H : ℤ} (hd : d_den ≠ 0) (hDH : D_H ≠ 0) {k ℓ : ℕ} (hℓ : Fintype.card ι < ℓ) (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (N_H : ℕ → ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hθ : ∀ (x : ι → Bool), ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, Polynomial.eval 0 (θ x i v) = d_den * bitVal ℤ (x v)) (hcramer : ∀ s ∈ Finset.range ℓ, N_H s = D_H * Polynomial.eval 0 (univariateClearedParityCoord I P d_den k ℓ θ s)) : (∑ s ∈ Finset.range ℓ, N_H s / (clearedProductDenom d_den k ℓ I.card * D_H)) % 2 ^ ℓ = ↑(commonZeroCount I P)

Appendix B.3 (eq. B.1, Cramer's rule determinant exact division recovery): if N_H : ℕ → ℤ and D_H : ℤ (D_H ≠ 0) satisfy N_H s = D_H * (univariateClearedParityCoord I P d_den k ℓ θ s).eval 0 for all s ∈ range ℓ (as in $N_H = \det V^{(0)} = (\det V) \cdot \Omega H_s(0)$), then for d_den ≠ 0 and Fintype.card ι < ℓ, summing the exact integer quotients N_H s / (clearedProductDenom d_den k ℓ #I * D_H) over s ∈ range ℓ and reducing modulo 2 ^ ℓ recovers commonZeroCount I P.

theorem Cslib.BitString.commonZeroCount_eq_sum_branch_emod_ediv_cleared {ι : Type u_1} {κ : Type u_2} {ι' : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι'] (S : Finset ι) (e : ↥(Finset.univ \ S) ≃ ι') (I : Finset κ) (P : κ → Finset (Finset ι)) {d_den : ℤ} (hd : d_den ≠ 0) {k : ℕ} (θ : (ι → Bool) → (ι' → Bool) → κ → ι' → Polynomial ℤ) (hk : ∀ i ∈ I, ∀ M ∈ P i, M.card ≤ k) (hθ : ∀ b ∈ branchAssignments S, ∀ (x : ι' → Bool), ∀ i ∈ I, ∀ M ∈ relabelRestrictedMonomials S e b (P i), ∀ v ∈ M, Polynomial.eval 0 (θ b x i v) = d_den * bitVal ℤ (x v)) : ↑(commonZeroCount I P) = ∑ b ∈ branchAssignments S, Polynomial.eval 0 (univariateClearedParityTruncatedSum I (fun (i : κ) => relabelRestrictedMonomials S e b (P i)) d_den k (branchPrecision (Fintype.card ι)) (θ b)) / clearedProductDenom d_den k (branchPrecision (Fintype.card ι)) I.card % 2 ^ branchPrecision (Fintype.card ι)

§5.5 & Appendix B.3 (branch-summed exact integer division recovery at shared precision $\ell = n + 1$): summing the branch modular residues of ((univariateClearedParityTruncatedSum ...).eval 0 / clearedProductDenom ...) at precision branchPrecision (Fintype.card ι) across all b ∈ branchAssignments S recovers commonZeroCount I P.

4. Bivariate ℓ₁-norm bounds for cleared parity products and coordinates

(Appendix B.2)

theorem Cslib.BitString.bivariateCoeffNorm1_parityFactorCleared_le (ℓ : ℕ) (Δ : ℤ) {A_i : Polynomial ℤ} {B E_ℓ : ℕ} (hA : A_i.coeffNorm1 ≤ B) (hE : ∀ s < ℓ, (Polynomial.parityBaseDigit ℓ s).coeffNorm1 ≤ E_ℓ) : (parityFactorCleared ℓ (Polynomial.C Δ) A_i).bivariateCoeffNorm1 ≤ ℓ * E_ℓ * (B + Δ.natAbs) ^ (2 * ℓ - 1)

Appendix B.2 (∥Γ B_i∥₁ ≤ B₁ = ℓ E_ℓ (B + |Δ|)^{2ℓ - 1}): if A_i.coeffNorm1 ≤ B and ∀ s < ℓ, (parityBaseDigit ℓ s).coeffNorm1 ≤ E_ℓ, then (parityFactorCleared ℓ (C Δ) A_i).bivariateCoeffNorm1 ≤ ℓ * E_ℓ * (B + Δ.natAbs) ^ (2 * ℓ - 1).

theorem Cslib.BitString.bivariateCoeffNorm1_prod_parityFactorCleared_le {κ : Type u_2} (I : Finset κ) (ℓ : ℕ) (Δ : ℤ) {A_i : κ → Polynomial ℤ} {B E_ℓ : ℕ} (hA : ∀ i ∈ I, (A_i i).coeffNorm1 ≤ B) (hE : ∀ s < ℓ, (Polynomial.parityBaseDigit ℓ s).coeffNorm1 ≤ E_ℓ) : (∏ i ∈ I, parityFactorCleared ℓ (Polynomial.C Δ) (A_i i)).bivariateCoeffNorm1 ≤ (ℓ * E_ℓ * (B + Δ.natAbs) ^ (2 * ℓ - 1)) ^ I.card

Appendix B.2 (∥Ω ∏_{i ∈ I} B_i∥₁ ≤ B₁ ^ #I): under the same bounds for every i ∈ I, the product of cleared parity factors has bivariateCoeffNorm1 at most (ℓ * E_ℓ * (B + Δ.natAbs) ^ (2 * ℓ - 1)) ^ #I.

theorem Cslib.BitString.coeffNorm1_univariateClearedParityCoord_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (I : Finset κ) (P : κ → Finset (Finset ι)) (d_den : ℤ) (k ℓ : ℕ) {B E_ℓ : ℕ} (θ : (ι → Bool) → κ → ι → Polynomial ℤ) (hA : ∀ (x : ι → Bool), ∀ i ∈ I, (clearedMonomialSumPoly d_den k (θ x i) (P i)).coeffNorm1 ≤ B) (hE : ∀ j < ℓ, (Polynomial.parityBaseDigit ℓ j).coeffNorm1 ≤ E_ℓ) (s : ℕ) : (univariateClearedParityCoord I P d_den k ℓ θ s).coeffNorm1 ≤ 2 ^ Fintype.card ι * (ℓ * E_ℓ * (B + (d_den ^ k).natAbs) ^ (2 * ℓ - 1)) ^ I.card

Appendix B.2 (∥[V^s] \tilde{H}(T)∥₁ ≤ 2 ^ n * B₁ ^ #I): if every cleared equation polynomial clearedMonomialSumPoly d_den k (θ x i) (P i) has coeffNorm1 ≤ B and ∀ j < ℓ, (parityBaseDigit ℓ j).coeffNorm1 ≤ E_ℓ, then every coordinate polynomial univariateClearedParityCoord I P d_den k ℓ θ s has coeffNorm1 at most 2 ^ Fintype.card ι * (ℓ * E_ℓ * (B + (d_den ^ k).natAbs) ^ (2 * ℓ - 1)) ^ #I.