An exactly balanced function hard for OR-AND-OR and AND-OR-AND

Balanced padding of OpenAI's hard language inherits its unrestricted depth-three lower bound under both polarities. The proof reuses complexitylib's existing balanced-padding construction and the source circuit substitution.

Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/LanguageLowerBound.lean

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

Positive-length slices of the list language are the balanced finite functions.

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

The De Morgan dual interpretation complements the circuit's original value.

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

Exactly half the inputs are accepted, including at the smallest padded dimension.

theorem Complexity.DepthThreeLowerBound.balancedFamily_lower_bound (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

Both the balanced function and its complement need more than every fixed square-root exponential number of OR-AND-OR gates.

theorem Complexity.DepthThreeLowerBound.balancedFamily_both_polarities (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

The same balanced family is hard for both unrestricted depth-three polarities.