Balanced hardness under both depth-three polarities

Fix the fresh input bit to recover the original hard function from either output polarity. Input substitution preserves the number of gates. The existing balanced-padding count gives exactly half of the input cube.

theorem Complexity.DepthThreeLowerBound.balancedLanguage_ofFn_proof (n : ℕ) (x : Cube (Fin (n + 1))) : balancedLanguage (List.ofFn x) = balancedFamily n x

theorem Complexity.DepthThreeLowerBound.balancedFamily_card_proof (n : ℕ) : (Algebraic.Cutwidth.accepting (balancedFamily n)).card = 2 ^ n

theorem Complexity.DepthThreeLowerBound.balancedFamily_restrict (n : ℕ) (b : Bool) : ∃ (α : Fin (n + 1) → Fin n ⊕ Bool), ∀ (x : Cube (Fin n)), (balancedFamily n (GateInput.assignment α x) ^^ b) = language (List.ofFn x)

theorem Complexity.DepthThreeLowerBound.balancedFamily_lower_bound_proof (A : ℝ) (hA : 0 < A) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (b : Bool) (D : Circuit3 (Fin (n + 1))), (D.Computes fun (x : Cube (Fin (n + 1))) => balancedFamily n x ^^ b) → 2 ^ (A * √↑(n + 1)) < ↑D.gateCount

theorem Complexity.DepthThreeLowerBound.Circuit3.dualEval_eq_not_eval_proof {V : Type u_1} (C : Circuit3 V) (x : Cube V) : C.dualEval x = !C.eval x

theorem Complexity.DepthThreeLowerBound.balancedFamily_both_polarities_proof (A : ℝ) (hA : 0 < A) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (D : Circuit3 (Fin (n + 1))), D.Computes (balancedFamily n) ∨ D.ComputesDual (balancedFamily n) → 2 ^ (A * √↑(n + 1)) < ↑D.gateCount