A balanced polynomial-time language with unrestricted depth-three hardness

These statements use complexitylib's canonical P and FP, through the checked machine simulation. Circuit gates are counted in the source's unrestricted shared three-layer model.

theorem Complexity.DepthThreeLowerBound.language_mem_P : {w : List Bool | language w = true} ∈ P

OpenAI's explicit depth-three hard language belongs to the canonical class P.

theorem Complexity.DepthThreeLowerBound.language_eval_mem_FP : (fun (w : List Bool) => [language w]) ∈ FP

Its one-bit verdict is a polynomial-time function in the canonical FP.

theorem Complexity.DepthThreeLowerBound.balancedLanguage_mem_P : {w : List Bool | balancedLanguage w = true} ∈ P

Balanced padding of the hard language also belongs to the canonical class P.

theorem Complexity.DepthThreeLowerBound.exists_balanced_language_in_P_depth_three_lower_bound : ∃ (L : List Bool → Bool), {w : List Bool | L w = true} ∈ P ∧ (∀ (n : ℕ), {x : Cube (Fin (n + 1)) | L (List.ofFn x) = true}.card = 2 ^ n) ∧ ∀ (A : ℝ), 0 < A → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (D : Circuit3 (Fin (n + 1))), ((D.Computes fun (x : Cube (Fin (n + 1))) => L (List.ofFn x)) ∨ D.ComputesDual fun (x : Cube (Fin (n + 1))) => L (List.ofFn x)) → 2 ^ (A * √↑(n + 1)) < ↑D.gateCount

An exactly balanced language in canonical P needs every fixed square-root exponential number of gates in both unrestricted depth-three polarities.