Transport of the depth-three and threshold-weight bounds to canonical CNFs

The indexed construction records every clause occurrence and one middle gate per CNF. The weight bounds use the width-nonincreasing set conversion instead.

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

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

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

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

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

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

theorem Complexity.DepthThreeLowerBound.language_or_cnf_lower_bound_proof (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)

theorem Complexity.DepthThreeLowerBound.language_cnf_threshold_weight_proof (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|

theorem Complexity.DepthThreeLowerBound.language_cnf_integer_threshold_weight_proof (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)|