Polynomial compilation of CNF parity tests over 𝔽₂

For a propositional clause c : Clause V, its violation bit !c.eval σ on an assignment σ : V → Bool expands over 𝔽₂ = ZMod 2 into a multilinear sum of monomials (Cslib.Logic.PL.Clause.falsifyMonomials): a tautological clause expands to ∅ (0), the empty clause expands to {∅} (1), and a nontautological clause with positive variables P and negative variables N expands to {S ∪ N | S ⊆ P}, using the identity ∏_{v ∈ P} (1 + x_v) ∏_{v ∈ N} x_v = ∑_{S ⊆ P} ∏_{v ∈ S ∪ N} x_v over ZMod 2. Repeated literals within c collapse automatically, so every monomial has support in (c.map Prod.fst).toFinset and degree at most c.length, and there are at most 2 ^ c.length monomials.

Given a formula φ : CNF V with m = φ.length clauses and a binary parity-check row r : Fin φ.length → Bool, equation (6.1) of [OAI26c] specifies the 𝔽₂ polynomial equation P_r(σ) = ∑_{e : r e = true} v_e(σ) = 0. Retaining the monomials that occur in an odd number of active clauses (Cslib.Logic.PL.CNF.parityRowMonomials) cancels duplicate monomials modulo 2: adding rows in the Boolean ring corresponds to taking the symmetric difference of their monomial sets (Cslib.Logic.PL.CNF.parityRowMonomials_add), evaluating the compiled monomial sum agrees with the parity check ∑ e, r e * φ.violations σ e (Cslib.Logic.PL.CNF.sum_parityRowMonomials), and when every clause has length at most k, each retained monomial has degree at most k and there are at most weight r * 2 ^ k monomials (≤ P * 2 ^ k for r = testRow γ of length P).

On a finite variable type V, the common zeros of {φ.parityRowMonomials r | r ∈ rows} are therefore the assignments accepted by PassesTests φ.violations rows, decomposing as numPassing φ.violations rows = φ.modelCountOn Finset.univ + D(rows) where D(rows) counts accepted nonsatisfying assignments, and equaling φ.modelCountOn Finset.univ after the 3 * Fintype.card V greedy rounds of CNF.numPassing_greedy [OpenAI2026ETH, Lemma 6.2, §6.3].

Main definitions

• Cslib.Logic.PL.Clause.falsifyMonomials: canonical 𝔽₂ multilinear monomial set of !c.eval.
• Cslib.Logic.PL.CNF.parityRowMonomials: mod-2 cancelled 𝔽₂ monomial set of a parity row on clause violations.

Main results

• Cslib.Logic.PL.Clause.sum_falsifyMonomials: semantic agreement of Clause.falsifyMonomials with bitVal (ZMod 2) (!c.eval σ).
• Cslib.Logic.PL.Clause.subset_vars_of_mem_falsifyMonomials, Cslib.Logic.PL.Clause.card_le_length_of_mem_falsifyMonomials, Cslib.Logic.PL.Clause.card_falsifyMonomials_le: support, degree, and 2 ^ c.length sparsity bounds for one clause.
• Cslib.Logic.PL.CNF.sum_parityRowMonomials, Cslib.Logic.PL.CNF.sum_parityRowMonomials_eq_zero_iff: semantic agreement of a compiled parity row with ∑ e, r e * φ.violations σ e.
• Cslib.Logic.PL.CNF.parityRowMonomials_add: mod-2 symmetric-difference cancellation across added parity rows.
• Cslib.Logic.PL.CNF.card_parityRowMonomials_le, Cslib.Logic.PL.CNF.card_parityRowMonomials_testRow_le: sparsity bounds weight r * 2 ^ k and P * 2 ^ k.
• Cslib.Logic.PL.CNF.commonZero_parityRowMonomials_iff_passesTests, Cslib.Logic.PL.CNF.numPassing_violations_eq_modelCountOn_add, Cslib.Logic.PL.CNF.card_commonZeros_greedy, Cslib.Logic.PL.CNF.greedy_system_bounds: common-zero equivalence, N(A) = #F + D(A) decomposition, exact CNF.modelCountOn Finset.univ recovery after 3 n greedy rounds, and candidate-system size, degree, and sparsity bounds.

References

• OpenAI, The Exponential Time Hypothesis is False, §6 (eq. 6.1), §6.2 (Lemma 6.2), and §6.3, pp. 39–40, 42–43

Clause-falsification monomials over ZMod 2

def Cslib.Logic.PL.Clause.falsifyMonomials {V : Type u_1} [DecidableEq V] (c : Clause V) : Finset (Finset V)

The canonical multilinear 𝔽₂ monomials whose sum evaluates to !c.eval σ over ZMod 2. If some variable occurs both positively and negatively in c, the clause is tautological and the set is empty; otherwise it consists of S ∪ neg as S ranges over subsets of the positive variables pos of c, expanding ∏_{v ∈ pos} (1 + x_v) ∏_{v ∈ neg} x_v modulo 2.

@[simp]

theorem Cslib.Logic.PL.Clause.falsifyMonomials_nil {V : Type u_1} [DecidableEq V] : falsifyMonomials [] = {∅}

The empty clause is always falsified, so its falsification polynomial is the constant 1 ({∅}).

theorem Cslib.Logic.PL.Clause.falsifyMonomials_eq_empty_of_tautology {V : Type u_1} [DecidableEq V] {c : Clause V} {v : V} (hpos : (v, true) ∈ c) (hneg : (v, false) ∈ c) : c.falsifyMonomials = ∅

A tautological clause containing both (v, true) and (v, false) has empty falsification monomial set.

theorem Cslib.Logic.PL.Clause.subset_vars_of_mem_falsifyMonomials {V : Type u_1} [DecidableEq V] {c : Clause V} {M : Finset V} (hM : M ∈ c.falsifyMonomials) : M ⊆ (List.map Prod.fst c).toFinset

Every monomial in c.falsifyMonomials uses only variables occurring in c.

theorem Cslib.Logic.PL.Clause.card_le_card_vars_of_mem_falsifyMonomials {V : Type u_1} [DecidableEq V] {c : Clause V} {M : Finset V} (hM : M ∈ c.falsifyMonomials) : M.card ≤ (List.map Prod.fst c).toFinset.card

Every monomial in c.falsifyMonomials has degree at most the number of distinct variables in c.

theorem Cslib.Logic.PL.Clause.card_le_length_of_mem_falsifyMonomials {V : Type u_1} [DecidableEq V] {c : Clause V} {M : Finset V} (hM : M ∈ c.falsifyMonomials) : M.card ≤ List.length c

Every monomial in c.falsifyMonomials has degree at most c.length.

theorem Cslib.Logic.PL.Clause.card_falsifyMonomials_le_two_pow_card_vars {V : Type u_1} [DecidableEq V] (c : Clause V) : c.falsifyMonomials.card ≤ 2 ^ (List.map Prod.fst c).toFinset.card

A clause on d distinct variables expands to at most 2 ^ d falsification monomials.

theorem Cslib.Logic.PL.Clause.card_falsifyMonomials_le {V : Type u_1} [DecidableEq V] (c : Clause V) : c.falsifyMonomials.card ≤ 2 ^ List.length c

A clause c expands to at most 2 ^ c.length falsification monomials.

theorem Cslib.Logic.PL.Clause.sum_falsifyMonomials {V : Type u_1} [DecidableEq V] (c : Clause V) (σ : V → Bool) : ∑ M ∈ c.falsifyMonomials, BitString.monomial (ZMod 2) M σ = BitString.bitVal (ZMod 2) !eval σ c

Clause-falsification polynomial identity over 𝔽₂ [OpenAI2026ETH, §6]. For every clause c and truth assignment σ, the sum over c.falsifyMonomials in ZMod 2 equals the violation bit !c.eval σ read in ZMod 2.

theorem Cslib.Logic.PL.Clause.sum_falsifyMonomials_eq_zero_iff {V : Type u_1} [DecidableEq V] (c : Clause V) (σ : V → Bool) : ∑ M ∈ c.falsifyMonomials, BitString.monomial (ZMod 2) M σ = 0 ↔ eval σ c = true

The falsification polynomial of c vanishes at σ over ZMod 2 if and only if σ satisfies c.

theorem Cslib.Logic.PL.Clause.sum_falsifyMonomials_mem_lowDegree {V : Type u_1} [DecidableEq V] (c : Clause V) : (fun (σ : V → Bool) => ∑ M ∈ c.falsifyMonomials, BitString.monomial (ZMod 2) M σ) ∈ BitString.lowDegree (ZMod 2) V (List.length c)

The falsification polynomial of c has multilinear degree at most c.length over ZMod 2.

Parity-check row compilation and mod-2 cancellation

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

The canonical 𝔽₂ monomial set of the linear parity-check equation (6.1) for row r : Fin φ.length → Bool on φ : CNF V: a monomial M is retained precisely when it belongs to (φ.get e).falsifyMonomials for an odd number of active clauses e (r e = true), cancelling duplicate monomials modulo 2.

@[simp]

theorem Cslib.Logic.PL.CNF.mem_parityRowMonomials {V : Type u_1} [DecidableEq V] {φ : CNF V} {r : Fin (List.length φ) → Bool} {M : Finset V} : M ∈ φ.parityRowMonomials r ↔ {e : Fin (List.length φ) | r e = true ∧ M ∈ (List.get φ e).falsifyMonomials}.card % 2 = 1

A monomial belongs to φ.parityRowMonomials r if and only if it appears in an odd number of active clauses e with r e = true.

@[simp]

theorem Cslib.Logic.PL.CNF.parityRowMonomials_zero {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.parityRowMonomials 0 = ∅

The zero parity row compiles to the empty monomial set.

theorem Cslib.Logic.PL.CNF.parityRowMonomials_single {V : Type u_1} [DecidableEq V] (φ : CNF V) (e : Fin (List.length φ)) : φ.parityRowMonomials (Pi.single e true) = (List.get φ e).falsifyMonomials

A unit parity row selecting only clause e compiles to (φ.get e).falsifyMonomials.

theorem Cslib.Logic.PL.CNF.parityRowMonomials_add {V : Type u_1} [DecidableEq V] (φ : CNF V) (r₁ r₂ : Fin (List.length φ) → Bool) : φ.parityRowMonomials (r₁ + r₂) = symmDiff (φ.parityRowMonomials r₁) (φ.parityRowMonomials r₂)

Mod-2 monomial cancellation across rows. Adding two parity-check rows in the Boolean ring takes the symmetric difference of their compiled monomial sets.

theorem Cslib.Logic.PL.CNF.subset_vars_of_mem_parityRowMonomials {V : Type u_1} [DecidableEq V] {φ : CNF V} {r : Fin (List.length φ) → Bool} {M : Finset V} (hM : M ∈ φ.parityRowMonomials r) : M ⊆ φ.vars.toFinset

Every monomial in φ.parityRowMonomials r is supported on the variables of φ.

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

When every clause of φ has length at most k, every monomial in φ.parityRowMonomials r has degree at most k.

theorem Cslib.Logic.PL.CNF.sum_parityRowMonomials_mem_lowDegree {V : Type u_1} [DecidableEq V] {φ : CNF V} {k : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) (r : Fin (List.length φ) → Bool) : (fun (σ : V → Bool) => ∑ M ∈ φ.parityRowMonomials r, BitString.monomial (ZMod 2) M σ) ∈ BitString.lowDegree (ZMod 2) V k

When every clause of φ has length at most k, the compiled polynomial of row r has multilinear degree at most k over ZMod 2.

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

Sparsity of a compiled parity row [OpenAI2026ETH, §6.2]. When every clause of φ has length at most k, φ.parityRowMonomials r contains at most weight r * 2 ^ k monomials.

theorem Cslib.Logic.PL.CNF.card_parityRowMonomials_testRow_le {V : Type u_1} [DecidableEq V] {φ : CNF V} {k P : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) (γ : Fin P → Fin (List.length φ) × Bool) : (φ.parityRowMonomials (BitString.testRow γ)).card ≤ P * 2 ^ k

Sparsity of a compiled test-list row [OpenAI2026ETH, Lemma 6.2]. For any test list γ : Fin P → Fin φ.length × Bool on a k-CNF formula φ, φ.parityRowMonomials (testRow γ) contains at most P * 2 ^ k monomials.

theorem Cslib.Logic.PL.CNF.sum_parityRowMonomials {V : Type u_1} [DecidableEq V] (φ : CNF V) (r : Fin (List.length φ) → Bool) (σ : V → Bool) : ∑ M ∈ φ.parityRowMonomials r, BitString.monomial (ZMod 2) M σ = BitString.bitVal (ZMod 2) (∑ e : Fin (List.length φ), r e * φ.violations σ e)

Compiled parity-row evaluation identity [OpenAI2026ETH, eq. (6.1)]. Evaluating the sum of φ.parityRowMonomials r at σ over ZMod 2 equals the parity ∑ e, r e * φ.violations σ e read in ZMod 2.

theorem Cslib.Logic.PL.CNF.sum_parityRowMonomials_eq_zero_iff {V : Type u_1} [DecidableEq V] (φ : CNF V) (r : Fin (List.length φ) → Bool) (σ : V → Bool) : ∑ M ∈ φ.parityRowMonomials r, BitString.monomial (ZMod 2) M σ = 0 ↔ ∑ e : Fin (List.length φ), r e * φ.violations σ e = false

Parity-row zero criterion [OpenAI2026ETH, eq. (6.1)]. An assignment σ is a zero of the compiled ZMod 2 polynomial of row r if and only if the violation parity ∑ e, r e * φ.violations σ e is false.

theorem Cslib.Logic.PL.CNF.sum_parityRowMonomials_eq_zero_iff_dotProduct {V : Type u_1} [DecidableEq V] (φ : CNF V) (r : Fin (List.length φ) → Bool) (σ : V → Bool) : ∑ M ∈ φ.parityRowMonomials r, BitString.monomial (ZMod 2) M σ = 0 ↔ r ⬝ᵥ φ.violations σ = false

Dot-product form of CNF.sum_parityRowMonomials_eq_zero_iff.

theorem Cslib.Logic.PL.CNF.sum_parityRowMonomials_testRow_eq_zero_iff {V : Type u_1} [DecidableEq V] {P : ℕ} (φ : CNF V) (γ : Fin P → Fin (List.length φ) × Bool) (σ : V → Bool) : ∑ M ∈ φ.parityRowMonomials (BitString.testRow γ), BitString.monomial (ZMod 2) M σ = 0 ↔ BitString.testParity γ (φ.violations σ) = false

For a test list γ, the compiled ZMod 2 polynomial of testRow γ vanishes at σ if and only if testParity γ (φ.violations σ) = false.

theorem Cslib.Logic.PL.CNF.commonZero_parityRowMonomials_iff_passesTests {V : Type u_1} [DecidableEq V] (φ : CNF V) (rows : List (Fin (List.length φ) → Bool)) (σ : V → Bool) : (∀ r ∈ rows, ∑ M ∈ φ.parityRowMonomials r, BitString.monomial (ZMod 2) M σ = 0) ↔ BitString.PassesTests φ.violations rows σ

Common-zero characterization. An assignment σ vanishes on every compiled equation in rows if and only if PassesTests φ.violations rows σ.

theorem Cslib.Logic.PL.CNF.commonZero_map_parityRowMonomials_iff_passesTests {V : Type u_1} [DecidableEq V] (φ : CNF V) (rows : List (Fin (List.length φ) → Bool)) (σ : V → Bool) : (∀ eq ∈ List.map φ.parityRowMonomials rows, ∑ M ∈ eq, BitString.monomial (ZMod 2) M σ = 0) ↔ BitString.PassesTests φ.violations rows σ

Common-zero characterization phrased over the compiled equation list rows.map φ.parityRowMonomials.

Common-zero counts and exact bridge to CNF.modelCountOn

@[simp]

theorem Cslib.Logic.PL.CNF.modelCountOn_univ {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) : φ.modelCountOn Finset.univ = {σ : V → Bool | eval σ φ = true}.card

On a finite variable type V, φ.modelCountOn Finset.univ counts all satisfying assignments σ : V → Bool.

theorem Cslib.Logic.PL.CNF.card_commonZeros_parityRowMonomials {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) (rows : List (Fin (List.length φ) → Bool)) : {σ : V → Bool | ∀ r ∈ rows, ∑ M ∈ φ.parityRowMonomials r, BitString.monomial (ZMod 2) M σ = 0}.card = BitString.numPassing φ.violations rows

The number of common zeros of {φ.parityRowMonomials r | r ∈ rows} on V → Bool equals numPassing φ.violations rows.

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

N(A) = #F + D(A) decomposition [OpenAI2026ETH, §6, p. 40]. The number of assignments passing rows equals φ.modelCountOn Finset.univ plus the number of nonsatisfying assignments still accepted by rows.

theorem Cslib.Logic.PL.CNF.card_commonZeros_eq_modelCountOn_add {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) (rows : List (Fin (List.length φ) → Bool)) : {σ : V → Bool | ∀ r ∈ rows, ∑ M ∈ φ.parityRowMonomials r, BitString.monomial (ZMod 2) M σ = 0}.card = φ.modelCountOn Finset.univ + {σ : V → Bool | eval σ φ = false ∧ BitString.PassesTests φ.violations rows σ}.card

N(P_A) = #F + D(A) for compiled 𝔽₂ equations [OpenAI2026ETH, §6, p. 40].

theorem Cslib.Logic.PL.CNF.card_commonZeros_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.numPassing φ.violations (A i ++ [BitString.testRow (γ i)]) ≤ BitString.numPassing φ.violations (A i ++ [BitString.testRow γ'])) : {σ : V → Bool | ∀ r ∈ A (3 * Fintype.card V), ∑ M ∈ φ.parityRowMonomials r, BitString.monomial (ZMod 2) M σ = 0}.card = φ.modelCountOn Finset.univ

Exact common-zero count after 3 n greedy parity-test rounds [OpenAI2026ETH, Lemma 6.2 & §6.3]. Under the hypotheses of CNF.numPassing_greedy, the common zeros of the compiled 𝔽₂ polynomial system A (3 * Fintype.card V) number exactly φ.modelCountOn Finset.univ (#F).

theorem Cslib.Logic.PL.CNF.greedy_system_bounds {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) {k D₀ P : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) (A : ℕ → List (Fin (List.length φ) → Bool)) (hA₀_len : (A 0).length ≤ 3 * Fintype.card V) (hA₀_wt : ∀ r ∈ A 0, BitString.weight r ≤ D₀) (γ : ℕ → Fin P → Fin (List.length φ) × Bool) (hA : ∀ (i : ℕ), A (i + 1) = A i ++ [BitString.testRow (γ i)]) {i : ℕ} (hi : i ≤ 3 * Fintype.card V) : (List.map φ.parityRowMonomials (A i)).length ≤ 6 * Fintype.card V ∧ ∀ eq ∈ List.map φ.parityRowMonomials (A i), (∀ M ∈ eq, M ⊆ φ.vars.toFinset ∧ M.card ≤ k) ∧ eq.card ≤ max D₀ P * 2 ^ k

Quantitative bounds on compiled greedy systems [OpenAI2026ETH, Lemma 6.2, p. 42]. If every clause of φ has length at most k, the initial matrix A 0 has at most 3 n rows each of weight at most D₀, and each round appends testRow (γ i) of list length P, then at any stage i ≤ 3 n the compiled system (A i).map φ.parityRowMonomials has at most 3 n + i (≤ 6 n) equations, each of degree at most k, supported on φ.vars.toFinset, and containing at most max D₀ P * 2 ^ k monomials.