Internal: Normal Form Proof Machinery

This internal module contains the proof infrastructure for CNF/DNF:

• Circuit embedding: CNF.toCircuit and DNF.toCircuit embed normal form formulas as 2-level circuits over Basis.unboundedAON, together with correctness (eval_toCircuit) and size (size_toCircuit) proofs.

• Lower bound machinery: DNF.flip_complexity_lb shows that any DNF computing a flip-sensitive function on N variables needs at least 2^{N-1} terms. Key lemmas include term_mentions_all, full_term_unique, and card_true_of_flip_sensitive.

The public interface re-exports the main theorems from Circ.NF.

Helper lemmas for toCircuit correctness

CNF circuit embedding

def CircuitComplexity.CNF.toCircuit {N : ℕ} [NeZero N] (φ : CNF N) : Circuit Basis.unboundedAON N 1 φ.complexity

Embed a CNF formula as a 2-level AND-of-ORs circuit over Basis.unboundedAON.

The circuit has φ.complexity internal OR gates (one per clause) and a single output AND gate. Each OR gate reads only primary input wires, with the negated flag encoding literal polarity. The circuit size is φ.complexity + 1.

Equations

• One or more equations did not get rendered due to their size.

theorem CircuitComplexity.CNF.eval_toCircuit {N : ℕ} [NeZero N] (φ : CNF N) : (fun (x : BitString N) => φ.toCircuit.eval x 0) = φ.eval

The circuit produced by toCircuit correctly computes the CNF formula.

theorem CircuitComplexity.CNF.size_toCircuit {N : ℕ} [NeZero N] (φ : CNF N) : φ.toCircuit.size = φ.complexity + 1

The circuit size of toCircuit is φ.complexity + 1.

DNF circuit embedding

def CircuitComplexity.DNF.toCircuit {N : ℕ} [NeZero N] (φ : DNF N) : Circuit Basis.unboundedAON N 1 φ.complexity

Embed a DNF formula as a 2-level OR-of-ANDs circuit over Basis.unboundedAON.

The circuit has φ.complexity internal AND gates (one per term) and a single output OR gate. Each AND gate reads only primary input wires, with the negated flag encoding literal polarity. The circuit size is φ.complexity + 1.

Equations

• One or more equations did not get rendered due to their size.

theorem CircuitComplexity.DNF.eval_toCircuit {N : ℕ} [NeZero N] (φ : DNF N) : (fun (x : BitString N) => φ.toCircuit.eval x 0) = φ.eval

The circuit produced by toCircuit correctly computes the DNF formula.

theorem CircuitComplexity.DNF.size_toCircuit {N : ℕ} [NeZero N] (φ : DNF N) : φ.toCircuit.size = φ.complexity + 1

The circuit size of toCircuit is φ.complexity + 1.

CNF/DNF Lower Bound for Flip-Sensitive Functions

theorem CircuitComplexity.DNF.term_mentions_all {N : ℕ} (φ : DNF N) (f : BitString N → Bool) (hcomp : ∀ (x : BitString N), φ.eval x = f x) (hflip : ∀ (x : Fin N → Bool) (i : Fin N), f (Function.update x i !x i) = !f x) (term : List (Literal N)) (hterm : term ∈ φ.terms) (x : BitString N) (hsat : (term.all fun (l : Literal N) => l.eval x) = true) (i : Fin N) : ∃ l ∈ term, l.var = i

If φ : DNF N computes a flip-sensitive function, every satisfiable term mentions all N variables.

theorem CircuitComplexity.full_term_unique {N : ℕ} {term : List (Literal N)} (hfull : ∀ (i : Fin N), ∃ l ∈ term, l.var = i) {x y : BitString N} (hx : (term.all fun (l : Literal N) => l.eval x) = true) (hy : (term.all fun (l : Literal N) => l.eval y) = true) : x = y

If a term mentions all N variables, it is satisfied by at most one assignment.

theorem CircuitComplexity.card_true_of_flip_sensitive {N : ℕ} (hN : 1 ≤ N) (f : BitString N → Bool) (hflip : ∀ (x : Fin N → Bool) (i : Fin N), f (Function.update x i !x i) = !f x) : {x : BitString N | f x = true}.card = 2 ^ (N - 1)

If f is flip-sensitive with N ≥ 1, its true-set has exactly 2^{N-1} elements.

theorem CircuitComplexity.DNF.flip_complexity_lb {N : ℕ} (φ : DNF N) (hN : 1 ≤ N) (f : BitString N → Bool) (hcomp : ∀ (x : BitString N), φ.eval x = f x) (hflip : ∀ (x : Fin N → Bool) (i : Fin N), f (Function.update x i !x i) = !f x) : 2 ^ (N - 1) ≤ φ.complexity

If φ : DNF N computes a flip-sensitive function with N ≥ 1, then 2^{N-1} ≤ φ.complexity.