Depth-three and threshold-weight bounds for canonical CNFs

These theorems use complexitylib's existing CNF rather than requiring source-specific formulas. The unrestricted gate bound counts clauses plus CNFs plus one; the coefficient bounds count absolute real or integer weights, including any constant feature.

theorem Complexity.CNF.eval_toDepthThree {n : ℕ} (F : CNF n) (x : BitString n) : F.toDepthThree.eval x = F.eval x

CNF conversion preserves evaluation, including empty clauses and conjunctions.

theorem Complexity.CNF.width_toDepthThree {n : ℕ} (F : CNF n) : F.toDepthThree.WidthAtMost F.width

The converted width is bounded by the canonical clause-length width.

theorem Complexity.DepthThreeLowerBound.Circuit3.eval_clauseInputs {n : ℕ} (C : List (Complexity.Literal n)) (x : BitString n) : (clauseInputs C).eval x = C.any fun (l : Complexity.Literal n) => l.eval x

Conversion of a clause preserves its disjunction.

theorem Complexity.DepthThreeLowerBound.Circuit3.middleEval_ofCNFs {n : ℕ} (Fs : List (Complexity.CNF n)) (j : Fin Fs.length) (x : BitString n) : (ofCNFs Fs).middleEval j x = Fs[j].eval x

Each middle gate computes its corresponding canonical CNF.

theorem Complexity.DepthThreeLowerBound.Circuit3.eval_ofCNFs {n : ℕ} (Fs : List (Complexity.CNF n)) (x : BitString n) : (ofCNFs Fs).eval x = Fs.any fun (F : Complexity.CNF n) => F.eval x

The converted three-layer circuit computes the OR of the input CNFs.

theorem Complexity.DepthThreeLowerBound.Circuit3.gateCount_ofCNFs {n : ℕ} (Fs : List (Complexity.CNF n)) : (ofCNFs Fs).gateCount = ∑ j : Fin Fs.length, Fs[j].complexity + Fs.length + 1

The exact cost is the number of clauses, plus the CNFs, plus the top gate.

theorem Complexity.DepthThreeLowerBound.language_or_cnf_lower_bound (A : ℝ) (hA : 0 < A) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (Fs : List (Complexity.CNF n)), (∀ (x : BitString n), (Fs.any fun (F : Complexity.CNF n) => F.eval x) = language (List.ofFn x)) → 2 ^ (A * √↑n) < ↑(∑ j : Fin Fs.length, Fs[j].complexity + Fs.length + 1)

The full hard language needs the stated total number of OR-of-CNF gates. This counts every clause, every CNF, and the top OR; it does not bound top fan-in alone.

theorem Complexity.DepthThreeLowerBound.language_cnf_threshold_weight (s : ℝ) (hs : 0 ≤ s) : ∃ (N : ℕ), 20480 ≤ N ∧ ∀ (n : ℕ), N ≤ n → ∀ (J : Type) [inst : Fintype J] (H : J → Complexity.CNF n) (a : J → ℝ), (∀ (j : J), (H j).width ≤ degreeCutoff s (dataDimension n)) → (∀ (x : Fin n → Bool), 1 ≤ sign (language (List.ofFn x)) * ∑ j : J, a j * indicator ((H j).eval x)) → 2 ^ (4 * (s + 1) * √↑(dataDimension n)) / 6 ≤ ∑ j : J, |a j|

The margin-one weight lower bound for complexitylib's canonical CNFs.

theorem Complexity.DepthThreeLowerBound.language_cnf_integer_threshold_weight (s : ℝ) (hs : 0 ≤ s) : ∃ (N : ℕ), 20480 ≤ N ∧ ∀ (n : ℕ), N ≤ n → ∀ (J : Type) [inst : Fintype J] (H : J → Complexity.CNF n) (z : J → ℤ), (∀ (j : J), (H j).width ≤ degreeCutoff s (dataDimension n)) → (∀ (x : Fin n → Bool), language (List.ofFn x) = decide (0 ≤ ∑ j : J, z j * if (H j).eval x = true then 1 else 0)) → (2 ^ (4 * (s + 1) * √↑(dataDimension n)) / 6 - 1) / 2 ≤ ∑ j : J, |↑(z j)|

The integer threshold-weight lower bound for canonical CNFs; ties accept.