Correlation bounds imply threshold-weight bounds

If every feature has correlation at most ε with a target, any linear combination representing the target with margin γ must have coefficient weight at least γ / ε. This elementary duality argument provides the threshold-weight step for consequences of OpenAI's depth-three circuit result: https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Beyond-the-Square-Root-Exponent-for-Depth-Three-Boolean-Circuits-September-23-2026

The result is stated for arbitrary finite domains and real-valued features, so it applies to CNF indicators and other feature classes. A bias is another feature, namely the constant function one, and needs its own correlation bound. The conclusion bounds the sum of absolute coefficient values. It does not bound the number of arbitrary-weight gates or the binary encoding length of their coefficients.

theorem Complexity.BooleanAnalysis.margin_le_correlation_mul_weight {X : Type u_1} {J : Type u_2} [Fintype X] [Nonempty X] [Fintype J] (g : X → ℝ) (H : J → X → ℝ) (a : J → ℝ) (ε γ : ℝ) (hcorr : ∀ (j : J), |Finset.univ.expect fun (x : X) => g x * H j x| ≤ ε) (hmargin : ∀ (x : X), γ ≤ g x * ∑ j : J, a j * H j x) : γ ≤ ε * ∑ j : J, |a j|

Small correlations force large coefficient weight for any representation with a uniform signed margin. The margin and correlation bounds are explicit.

theorem Complexity.BooleanAnalysis.threshold_weight_lower_bound {X : Type u_1} {J : Type u_2} [Fintype X] [Nonempty X] [Fintype J] (g : X → ℝ) (H : J → X → ℝ) (a : J → ℝ) {ε : ℝ} (hε : 0 < ε) (hcorr : ∀ (j : J), |Finset.univ.expect fun (x : X) => g x * H j x| ≤ ε) (hmargin : ∀ (x : X), 1 ≤ g x * ∑ j : J, a j * H j x) : 1 / ε ≤ ∑ j : J, |a j|

A margin-one threshold representation has weight at least the reciprocal of the common correlation bound.