Sparse 𝔽₂ Polynomial Systems and Branch-Reduced Parity Counting for CNF Formulas

This module connects the sparse CNF parity-test compilation of Sections 6.1–6.3 (Complexity.Logics.Propositional.CNF.ExactTests and Complexity.Logics.Propositional.CNF.PolynomialTests) with the sparse 𝔽₂ polynomial system, heavy-variable branching, and cleared-denominator parity-amplifier counter of Section 5 and Appendix B.2–B.3 (Complexity.Foundations.BooleanAnalysis.SparseEquations, Complexity.Foundations.BooleanAnalysis.SparseBranching, and Complexity.Foundations.BooleanAnalysis.SparseClearedSpecialization) of OpenAI, The Exponential Time Hypothesis is False (printed pp. 37–43, 48–50):

1. Indexed sparse 𝔽₂ polynomial system of parity-check rows (CNF.parityRowSystem): For any φ : CNF V and list rows : List (Fin φ.length → Bool) of parity-check rows on the clause-violation vector, φ.parityRowSystem rows : Fin rows.length → Finset (Finset V) indexes the compiled 𝔽₂ equations φ.parityRowMonomials (rows.get i). Its Cslib.BitString common zero predicate IsCommonZero univ (φ.parityRowSystem rows) is equivalent to PassesTests φ.violations rows, and its common-zero count commonZeroCount univ (φ.parityRowSystem rows) equals numPassing φ.violations rows.
2. Degree, sparsity, variable-scope, and heavy-variable branch bounds (§5.5 & Lemma 6.2): When every clause of φ has width at most k and every row in rows has Hamming weight at most W, each equation φ.parityRowSystem rows i has degree at most k, at most W * 2 ^ k monomials, and variable scope equationScope (φ.parityRowSystem rows i) of size at most k * (W * 2 ^ k) contained in φ.vars.toFinset. Consequently, branching on the heavy variables heavyVars univ univ (fun i => equationScope (φ.parityRowSystem rows i)) b₀ produces at most 2 ^ ((rows.length * (k * (W * 2 ^ k))) / b₀) branches, each with post-branching free-variable incidence at most b₀.
3. End-to-end greedy parity-test model counting via commonZeroCount and cleared-denominator branch evaluation (§6.1–6.3 & §5.4–5.5): Combining CNF.numPassing_greedy_initial (Lemmas 6.1–6.2) with CNF.commonZeroCount_parityRowSystem and commonZeroCount_eq_sum_branch_emod_ediv_cleared shows that for any width-≤ k formula φ on n = Fintype.card V ≥ 1 variables with φ.length ≤ B * n (B ≥ 1), there exist at most 3 * n initial rows A₀ of weight at most D₀ = 320000 * B ^ 2 * (Nat.log 2 φ.length + 1) ^ 3 such that any 3 * n-step greedy sequence minimizing commonZeroCount univ (φ.parityRowSystem (A i ++ [testRow γ'])) over candidate rows of list length P = 20000 * B ^ 2 * (Nat.log 2 φ.length + 1) ^ 2 satisfies commonZeroCount univ (φ.parityRowSystem (A (3 * n))) = φ.modelCountOn Finset.univ, and its branch-summed cleared-denominator parity-product evaluation at T = 0 recovers φ.modelCountOn Finset.univ on the nose.

Main definitions

• Cslib.Logic.PL.CNF.parityRowSystem: the Fin rows.length-indexed sparse 𝔽₂ polynomial system fun i => φ.parityRowMonomials (rows.get i).

Main results

• Cslib.Logic.PL.CNF.isCommonZero_parityRowSystem_iff, Cslib.Logic.PL.CNF.commonZeroCount_parityRowSystem: equivalence between IsCommonZero / commonZeroCount of φ.parityRowSystem rows and PassesTests / numPassing.
• Cslib.Logic.PL.CNF.card_equationScope_parityRowSystem_le, Cslib.Logic.PL.CNF.totalIncidence_parityRowSystem_le, Cslib.Logic.PL.CNF.card_branchAssignments_heavyVars_parityRowSystem_le, Cslib.Logic.PL.CNF.varIncidence_restrictMonomials_heavyVars_parityRowSystem_le: variable-scope, total-incidence, and heavy-variable branching bounds for compiled parity-row systems.
• Cslib.Logic.PL.CNF.commonZeroCount_parityRowSystem_greedy, Cslib.Logic.PL.CNF.exists_initialTests_commonZeroCount_greedy, Cslib.Logic.PL.CNF.modelCountOn_eq_sum_branch_emod_ediv_cleared_greedy: exact recovery of φ.modelCountOn Finset.univ after 3 * Fintype.card V greedy rounds via commonZeroCount and cleared-denominator branch evaluation.

References

• OpenAI, The Exponential Time Hypothesis is False (Sections 5.4–5.5 and 6.1–6.3)

1. Indexed sparse 𝔽₂ polynomial system of parity-check rows

def Cslib.Logic.PL.CNF.parityRowSystem {V : Type u_1} [DecidableEq V] (φ : CNF V) (rows : List (Fin (List.length φ) → Bool)) (i : Fin rows.length) : Finset (Finset V)

The Fin rows.length-indexed sparse 𝔽₂ polynomial system compiled from a list rows : List (Fin φ.length → Bool) of parity-check rows on the clause-violation bits of φ ([OAI26c], eq. 6.1, p. 39).

theorem Cslib.Logic.PL.CNF.isCommonZero_parityRowSystem_iff {V : Type u_1} [DecidableEq V] (φ : CNF V) (rows : List (Fin (List.length φ) → Bool)) (σ : V → Bool) : BitString.IsCommonZero Finset.univ (φ.parityRowSystem rows) σ ↔ BitString.PassesTests φ.violations rows σ

§6 (eq. 6.1 common-zero equivalence): σ : V → Bool is a common zero of φ.parityRowSystem rows if and only if PassesTests φ.violations rows σ.

theorem Cslib.Logic.PL.CNF.card_mem_parityRowSystem_le {V : Type u_1} [DecidableEq V] {φ : CNF V} {k : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) (rows : List (Fin (List.length φ) → Bool)) (i : Fin rows.length) {M : Finset V} (hM : M ∈ φ.parityRowSystem rows i) : M.card ≤ k

If every clause of φ has width at most k, then every monomial in φ.parityRowSystem rows i has size at most k.

theorem Cslib.Logic.PL.CNF.card_parityRowSystem_le {V : Type u_1} [DecidableEq V] {φ : CNF V} {k W : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) {rows : List (Fin (List.length φ) → Bool)} (hW : ∀ r ∈ rows, BitString.weight r ≤ W) (i : Fin rows.length) : (φ.parityRowSystem rows i).card ≤ W * 2 ^ k

If every clause of φ has width at most k and every row in rows has Hamming weight at most W, then every equation φ.parityRowSystem rows i contains at most W * 2 ^ k monomials.

theorem Cslib.Logic.PL.CNF.card_equationScope_parityRowSystem_le {V : Type u_1} [DecidableEq V] {φ : CNF V} {k W : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) {rows : List (Fin (List.length φ) → Bool)} (hW : ∀ r ∈ rows, BitString.weight r ≤ W) (i : Fin rows.length) : (BitString.equationScope (φ.parityRowSystem rows i)).card ≤ k * (W * 2 ^ k)

If every clause of φ has width at most k and every row in rows has Hamming weight at most W, then the variable scope equationScope (φ.parityRowSystem rows i) has size at most k * (W * 2 ^ k).

theorem Cslib.Logic.PL.CNF.totalIncidence_parityRowSystem_le {V : Type u_1} [DecidableEq V] {φ : CNF V} {k W : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) {rows : List (Fin (List.length φ) → Bool)} (hW : ∀ r ∈ rows, BitString.weight r ≤ W) : (BitString.totalIncidence Finset.univ fun (i : Fin rows.length) => BitString.equationScope (φ.parityRowSystem rows i)) ≤ k * (W * 2 ^ k) * rows.length

Under the same hypotheses, the total variable-equation incidence across all rows.length compiled equations is at most (k * (W * 2 ^ k)) * rows.length.

2. Common-zero counts, heavy-variable branching, and greedy parity recovery

theorem Cslib.Logic.PL.CNF.commonZeroCount_parityRowSystem {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) (rows : List (Fin (List.length φ) → Bool)) : BitString.commonZeroCount Finset.univ (φ.parityRowSystem rows) = BitString.numPassing φ.violations rows

§6 (common-zero count identity): commonZeroCount univ (φ.parityRowSystem rows) equals numPassing φ.violations rows.

theorem Cslib.Logic.PL.CNF.commonZeroCount_parityRowSystem_eq_modelCountOn_add {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) (rows : List (Fin (List.length φ) → Bool)) : BitString.commonZeroCount Finset.univ (φ.parityRowSystem rows) = φ.modelCountOn Finset.univ + {σ : V → Bool | eval σ φ = false ∧ BitString.PassesTests φ.violations rows σ}.card

N(P_A) = #F + D(A) in commonZeroCount form ([OAI26c], §6, p. 40).

theorem Cslib.Logic.PL.CNF.card_branchAssignments_heavyVars_parityRowSystem_le {V : Type u_1} [Fintype V] [DecidableEq V] {φ : CNF V} {k W b₀ : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) {rows : List (Fin (List.length φ) → Bool)} (hW : ∀ r ∈ rows, BitString.weight r ≤ W) (hb₀ : 0 < b₀) : (BitString.branchAssignments (BitString.heavyVars Finset.univ Finset.univ (fun (i : Fin rows.length) => BitString.equationScope (φ.parityRowSystem rows i)) b₀)).card ≤ 2 ^ (k * (W * 2 ^ k) * rows.length / b₀)

§5.5 & §6.3 (heavy-variable branch count bound on compiled parity systems): if every clause of φ has width at most k, every row in rows has Hamming weight at most W, and 0 < b₀, then branching on heavyVars univ univ (fun i => equationScope (φ.parityRowSystem rows i)) b₀ produces at most 2 ^ (((k * (W * 2 ^ k)) * rows.length) / b₀) canonical branches.

theorem Cslib.Logic.PL.CNF.varIncidence_restrictMonomials_heavyVars_parityRowSystem_le {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) (rows : List (Fin (List.length φ) → Bool)) (b₀ : ℕ) (b : V → Bool) (v : V) : BitString.varIncidence Finset.univ (fun (i : Fin rows.length) => BitString.equationScope (BitString.restrictMonomials (BitString.heavyVars Finset.univ Finset.univ (fun (j : Fin rows.length) => BitString.equationScope (φ.parityRowSystem rows j)) b₀) b (φ.parityRowSystem rows i))) v ≤ b₀

§5.5 & §6.3 (post-branching free-variable incidence bound on compiled parity systems): after branching on heavyVars univ univ (fun i => equationScope (φ.parityRowSystem rows i)) b₀, every variable v : V appears in at most b₀ restricted equations.

theorem Cslib.Logic.PL.CNF.commonZeroCount_parityRowSystem_greedy {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) {P : ℕ} (hn : 1 ≤ Fintype.card V) (hP : 1 ≤ P) (A : ℕ → List (Fin (List.length φ) → Bool)) (hinit : ∀ (σ : V → Bool), BitString.PassesTests φ.violations (A 0) σ → eval σ φ = false → List.length φ ≤ P * BitString.weight (φ.violations σ)) (γ : ℕ → Fin P → Fin (List.length φ) × Bool) (hA : ∀ (i : ℕ), A (i + 1) = A i ++ [BitString.testRow (γ i)]) (hγ : ∀ (i : ℕ) (γ' : Fin P → Fin (List.length φ) × Bool), BitString.commonZeroCount Finset.univ (φ.parityRowSystem (A i ++ [BitString.testRow (γ i)])) ≤ BitString.commonZeroCount Finset.univ (φ.parityRowSystem (A i ++ [BitString.testRow γ']))) : BitString.commonZeroCount Finset.univ (φ.parityRowSystem (A (3 * Fintype.card V))) = φ.modelCountOn Finset.univ

Lemma 6.2 & §6.3 (commonZeroCount greedy recovery of φ.modelCountOn Finset.univ): under the initial-residual hypothesis hinit, if each greedy step i chooses γ i minimizing commonZeroCount univ (φ.parityRowSystem (A i ++ [testRow γ'])), then after 3 * Fintype.card V rounds the common-zero count of φ.parityRowSystem (A (3 * Fintype.card V)) equals φ.modelCountOn Finset.univ (#F).

theorem Cslib.Logic.PL.CNF.exists_initialTests_commonZeroCount_greedy {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) {k B : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) (hn : 1 ≤ Fintype.card V) (hB : 1 ≤ B) (hm : List.length φ ≤ B * Fintype.card V) : have D₀ := BitString.initialRowWeightBound B (List.length φ); have P := BitString.greedyRowListLength B (List.length φ); ∃ (A₀ : List (Fin (List.length φ) → Bool)), A₀.length ≤ 3 * Fintype.card V ∧ (∀ r ∈ A₀, BitString.weight r ≤ D₀) ∧ ∀ (A : ℕ → List (Fin (List.length φ) → Bool)) (γ : ℕ → Fin P → Fin (List.length φ) × Bool), A 0 = A₀ → (∀ (i : ℕ), A (i + 1) = A i ++ [BitString.testRow (γ i)]) → (∀ (i : ℕ) (γ' : Fin P → Fin (List.length φ) × Bool), BitString.commonZeroCount Finset.univ (φ.parityRowSystem (A i ++ [BitString.testRow (γ i)])) ≤ BitString.commonZeroCount Finset.univ (φ.parityRowSystem (A i ++ [BitString.testRow γ']))) → BitString.commonZeroCount Finset.univ (φ.parityRowSystem (A (3 * Fintype.card V))) = φ.modelCountOn Finset.univ ∧ ∀ i ≤ 3 * Fintype.card V, (A i).length ≤ 6 * Fintype.card V ∧ ∀ (j : Fin (A i).length), (∀ M ∈ φ.parityRowSystem (A i) j, M ⊆ φ.vars.toFinset ∧ M.card ≤ k) ∧ (φ.parityRowSystem (A i) j).card ≤ max D₀ P * 2 ^ k ∧ (BitString.equationScope (φ.parityRowSystem (A i) j)).card ≤ k * (max D₀ P * 2 ^ k)

Lemmas 6.1–6.2 & §6.3 (initial + greedy parity tests via commonZeroCount with system sparsity and scope bounds): for any width-≤ k CNF φ on n = Fintype.card V ≥ 1 variables with φ.length ≤ B * n (B ≥ 1), there exist initial parity rows A₀ (A₀.length ≤ 3 * n, each of weight at most D₀ = initialRowWeightBound B φ.length) such that for any greedy sequence A (i + 1) = A i ++ [testRow (γ i)] with A 0 = A₀ minimizing commonZeroCount univ (φ.parityRowSystem (A i ++ [testRow γ'])) over candidate rows of list length P = greedyRowListLength B φ.length:

1. After 3 * n rounds, commonZeroCount univ (φ.parityRowSystem (A (3 * n))) = φ.modelCountOn Finset.univ.
2. At every stage i ≤ 3 * n, (A i).length ≤ 6 * n, and every compiled equation φ.parityRowSystem (A i) j has degree at most k, at most max D₀ P * 2 ^ k monomials, and variable-scope size #(equationScope (φ.parityRowSystem (A i) j)) ≤ k * (max D₀ P * 2 ^ k).

theorem Cslib.Logic.PL.CNF.modelCountOn_eq_sum_branch_emod_ediv_cleared_greedy {V : Type u_1} [Fintype V] [DecidableEq V] {ι' : Type u_2} [Fintype ι'] [DecidableEq ι'] (φ : CNF V) {k P : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) (hn : 1 ≤ Fintype.card V) (hP : 1 ≤ P) (A : ℕ → List (Fin (List.length φ) → Bool)) (hinit : ∀ (σ : V → Bool), BitString.PassesTests φ.violations (A 0) σ → eval σ φ = false → List.length φ ≤ P * BitString.weight (φ.violations σ)) (γ : ℕ → Fin P → Fin (List.length φ) × Bool) (hA : ∀ (i : ℕ), A (i + 1) = A i ++ [BitString.testRow (γ i)]) (hγ : ∀ (i : ℕ) (γ' : Fin P → Fin (List.length φ) × Bool), BitString.commonZeroCount Finset.univ (φ.parityRowSystem (A i ++ [BitString.testRow (γ i)])) ≤ BitString.commonZeroCount Finset.univ (φ.parityRowSystem (A i ++ [BitString.testRow γ']))) (S : Finset V) (e : ↥(Finset.univ \ S) ≃ ι') {d_den : ℤ} (hd : d_den ≠ 0) (θ : (V → Bool) → (ι' → Bool) → Fin (A (3 * Fintype.card V)).length → ι' → Polynomial ℤ) (hθ : ∀ b ∈ BitString.branchAssignments S, ∀ (x : ι' → Bool), ∀ j ∈ Finset.univ, ∀ M ∈ BitString.relabelRestrictedMonomials S e b (φ.parityRowSystem (A (3 * Fintype.card V)) j), ∀ v ∈ M, Polynomial.eval 0 (θ b x j v) = d_den * BitString.bitVal ℤ (x v)) : ↑(φ.modelCountOn Finset.univ) = ∑ b ∈ BitString.branchAssignments S, Polynomial.eval 0 (BitString.univariateClearedParityTruncatedSum Finset.univ (fun (j : Fin (A (3 * Fintype.card V)).length) => BitString.relabelRestrictedMonomials S e b (φ.parityRowSystem (A (3 * Fintype.card V)) j)) d_den k (BitString.branchPrecision (Fintype.card V)) (θ b)) / BitString.clearedProductDenom d_den k (BitString.branchPrecision (Fintype.card V)) Finset.univ.card % 2 ^ BitString.branchPrecision (Fintype.card V)

§5.4–5.5 & §6.3 (branch-summed cleared-denominator recovery of φ.modelCountOn Finset.univ after 3 * n greedy rounds): under the hypotheses of CNF.commonZeroCount_parityRowSystem_greedy, for any heavy-variable set S : Finset V, free-variable relabeling e : ↥(univ \ S) ≃ ι', nonzero common denominator d_den ≠ 0, and cleared-denominator replacement family θ evaluating at T = 0 to d_den * bitVal ℤ (x v), summing the branch modular residues of univariateClearedParityTruncatedSum divided by clearedProductDenom at shared precision branchPrecision (Fintype.card V) across all b ∈ branchAssignments S recovers φ.modelCountOn Finset.univ.