The depth-three lower bound in CSLib's general circuit model

Normalize a CSLib circuit to a formula and then to the source three-layer circuit in one of its polarities. Balanced hardness covers both. The polynomial size overhead is absorbed by increasing the arbitrary constant in the square-root exponent.

theorem Complexity.DepthThreeLowerBound.eventually_nat_le_two_sqrt : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ↑n ≤ 2 ^ √↑n

theorem Complexity.DepthThreeLowerBound.shallow_cost_absorbed (A : ℝ) (hA : 0 < A) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (s : ℕ), ↑s ≤ 2 ^ (A * √↑n) → 2 * (2 * (↑n + ↑s) + 1) ^ 4 + 1 ≤ 2 ^ (5 * (A + 1) * √↑n)

theorem Complexity.DepthThreeLowerBound.cslib_depth_three_source_proof {n : ℕ} [NeZero n] (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1) (hd : c.depth ≤ 3) : ∃ (b : Bool) (C : Circuit3 (Fin n)), C.gateCount ≤ 2 * (2 * (n + c.size) + 1) ^ 4 + 1 ∧ C.Computes fun (x : Cube (Fin n)) => c.eval Basis.unboundedAndOr.interpretation x 0 ^^ b

theorem Complexity.DepthThreeLowerBound.balancedFamily_cslib_lower_bound_proof (A : ℝ) (hA : 0 < A) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature (n + 1) 1), c.depth ≤ 3 → c.Computes Basis.unboundedAndOr.interpretation (Cslib.Circuits.single (balancedFamily n)) → 2 ^ (A * √↑(n + 1)) < ↑c.size