Three-layer normalization of depth-three formulas

Flatten like-polarity gates and pad leaves. Every depth-three formula, or its complement, is an OR of CNFs with total clause-and-conjunction count at most twice its tree size.

theorem Complexity.AC0Formula.leaf_cnf {n : ℕ} (f : AC0Formula n) (h : f.depth = 0) : ∃ (F : CNF n), F.complexity ≤ f.size ∧ ∀ (x : BitString n), F.eval x = eval x f

theorem Complexity.AC0Formula.or_leaves_cnf {n : ℕ} (fs : AC0Forest n) (hd : forestDepth fs = 0) : ∃ (F : CNF n), F.complexity ≤ 1 ∧ ∀ (x : BitString n), F.eval x = evalAny x fs

theorem Complexity.AC0Formula.and_cnf {n : ℕ} (fs : AC0Forest n) (h : ∀ f ∈ fs.toList, ∃ (F : CNF n), F.complexity ≤ f.size ∧ ∀ (x : BitString n), F.eval x = eval x f) : ∃ (F : CNF n), F.complexity ≤ forestSize fs ∧ ∀ (x : BitString n), F.eval x = evalAll x fs

theorem Complexity.AC0Formula.depth_one_cnf {n : ℕ} (f : AC0Formula n) (hd : f.depth ≤ 1) : ∃ (F : CNF n), F.complexity ≤ f.size ∧ ∀ (x : BitString n), F.eval x = eval x f

theorem Complexity.AC0Formula.and_depth_two_cnf {n : ℕ} (fs : AC0Forest n) (hd : forestDepth fs ≤ 1) : ∃ (F : CNF n), F.complexity ≤ forestSize fs ∧ ∀ (x : BitString n), F.eval x = evalAll x fs

def Complexity.AC0Formula.cnfCost {n : ℕ} (Fs : List (CNF n)) : ℕ

Total number of clause and conjunction gates in a list of CNFs.

Equations

• Complexity.AC0Formula.cnfCost Fs = (List.map (fun (F : Complexity.CNF n) => F.complexity + 1) Fs).sum

theorem Complexity.AC0Formula.depth_two_sigma {n : ℕ} (f : AC0Formula n) (hd : f.depth ≤ 2) : ∃ (Fs : List (CNF n)), cnfCost Fs ≤ 2 * f.size ∧ ∀ (x : BitString n), (Fs.any fun (F : CNF n) => F.eval x) = eval x f

theorem Complexity.AC0Formula.forest_depth_two_sigma {n : ℕ} (fs : AC0Forest n) (hd : forestDepth fs ≤ 2) : ∃ (Fs : List (CNF n)), cnfCost Fs ≤ 2 * forestSize fs ∧ ∀ (x : BitString n), (Fs.any fun (F : CNF n) => F.eval x) = evalAny x fs

theorem Complexity.AC0Formula.or_depth_three_sigma {n : ℕ} (fs : AC0Forest n) (hd : forestDepth fs ≤ 2) : ∃ (Fs : List (CNF n)), cnfCost Fs ≤ 2 * (or fs).size ∧ ∀ (x : BitString n), (Fs.any fun (F : CNF n) => F.eval x) = eval x (or fs)

theorem Complexity.AC0Formula.depth_three_sigma_polarity {n : ℕ} (f : AC0Formula n) (hd : f.depth ≤ 3) : ∃ (b : Bool) (Fs : List (CNF n)), cnfCost Fs ≤ 2 * f.size ∧ ∀ (x : BitString n), (Fs.any fun (F : CNF n) => F.eval x) = (eval x f ^^ b)

theorem Complexity.AC0Formula.cnfCost_eq {n : ℕ} (Fs : List (CNF n)) : cnfCost Fs = ∑ j : Fin Fs.length, Fs[j].complexity + Fs.length

theorem Complexity.AC0Formula.depth_three_source_proof {n : ℕ} (f : AC0Formula n) (hd : f.depth ≤ 3) : ∃ (b : Bool) (C : DepthThreeLowerBound.Circuit3 (Fin n)), C.gateCount ≤ 2 * f.size + 1 ∧ C.Computes fun (x : DepthThreeLowerBound.Cube (Fin n)) => eval x f ^^ b