Unrestricted depth-three lower bound: main

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

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

theorem Complexity.DepthThreeLowerBound.exists_polynomial_time_language_depth_three_lower_bound_proof : ∃ (L : List Bool → Bool) (M : FiniteMultiTapeMachine) (C : ℕ) (a : ℕ), 0 < C ∧ 0 < a ∧ (∀ (w : List Bool), MultiTapeHaltsIn M w (L w) (C * (w.length + 1) ^ a)) ∧ ∀ (A : ℝ), 0 < A → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (D : Circuit3 (Fin n)), (D.Computes fun (x : Cube (Fin n)) => L (List.ofFn x)) → 2 ^ (A * √↑n) < ↑D.gateCount