Exponential CNF threshold weight for the explicit hard language

This consequence combines OpenAI's hard-slice correlations with input substitution and the elementary correlation-to-margin inequality. It bounds total absolute coefficient weight for margin-one representations. A constant bias can be included as a feature using the empty, identically true CNF.

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

The width cutoff is ceil (3 * (s + 1) * sqrt (n / 5)). For every fixed s ≥ 0, the bound holds at all sufficiently large input lengths, on the full language. Coefficient weight is distinct from arbitrary-weight gate count.

theorem Complexity.DepthThreeLowerBound.language_threshold_weight (s : ℝ) (hs : 0 ≤ s) : ∃ (N : ℕ), 20480 ≤ N ∧ ∀ (n : ℕ), N ≤ n → ∀ (J : Type) [inst : Fintype J] (H : J → CNF (Fin n)) (a : J → ℝ), (∀ (j : J), (H j).WidthAtMost (degreeCutoff s (dataDimension n))) → (∀ (x : Fin n → Bool), 1 ≤ sign (language (List.ofFn x)) * ∑ j : J, a j * indicator ((H j).eval x)) → 2 ^ (4 * (s + 1) * √↑(dataDimension n)) / 6 ≤ ∑ j : J, |a j|

Every margin-one representation of the explicit language by CNF indicators of the specified width has at least the stated exponential coefficient weight.

theorem Complexity.DepthThreeLowerBound.language_integer_threshold_weight (s : ℝ) (hs : 0 ≤ s) : ∃ (N : ℕ), 20480 ≤ N ∧ ∀ (n : ℕ), N ≤ n → ∀ (J : Type) [inst : Fintype J] (H : J → CNF (Fin n)) (z : J → ℤ), (∀ (j : J), (H j).WidthAtMost (degreeCutoff s (dataDimension n))) → (∀ (x : Fin n → Bool), language (List.ofFn x) = decide (0 ≤ ∑ j : J, z j * if (H j).eval x = true then 1 else 0)) → (2 ^ (4 * (s + 1) * √↑(dataDimension n)) / 6 - 1) / 2 ≤ ∑ j : J, |↑(z j)|

Integer threshold representations need exponential coefficient weight without an assumed margin. Ties at zero accept. An integer bias can be a coefficient of the empty CNF, and its absolute value then contributes to the weight.