Unrestricted depth-three lower bound: language lower bound

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/LanguageLowerBound.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

theorem Complexity.DepthThreeLowerBound.language_depth_three_gate_lower_bound (A : ℝ) (hA : 0 < A) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (C : Circuit3 (Fin n)), (C.Computes fun (x : Cube (Fin n)) => language (List.ofFn x)) → 2 ^ (A * √↑n) < ↑C.gateCount