Gotsman--Linial: Main

Adapted from OpenAI's formalization of Average Sensitivity of Polynomial Threshold Functions (25 September 2026), at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/GotsmanLinial/Main.lean

The original Boolean-cube representation is used internally in this proof development; Complexitylib.BooleanAnalysis.PolynomialThreshold transports the result to the library's Fourier and influence API. Changes here adapt module visibility, namespace names, formatting, and redundant simp attributes to complexitylib.

Assembly of the Gotsman--Linial average-sensitivity bound

The first lemmas are explicitly conditional assembly bridges. The final theorems discharge their matrix and counting hypotheses using the concrete weighted Boolean-cube grading and a sign-preserving constant perturbation.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.normalized_edge_bound {N C T a : ℝ} (hN : 0 < N) (hedge : C ≤ 2 * T) (henergy : T ≤ 4 * a * N) : C / N ≤ 8 * a

The two analytic constants combine to the constant 8 after normalizing by the number of cube vertices. This is only a scalar bridge.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sensitivity_bound_of_counting_energy {n d : ℕ} (f : Cube n → ℝ) (C T : ℝ) (hcount : averageSensitivity f = C / 2 ^ n) (hedge : C ≤ 2 * T) (henergy : T ≤ 4 * (↑d * √↑n) * 2 ^ n) : averageSensitivity f ≤ 8 * ↑d * √↑n

Convert a counted-edge identity, edge recovery, and an anticommutator energy estimate into the desired sensitivity inequality. The counting and energy premises are explicit.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sensitivity_bound_of_cube_grading {n d : ℕ} (f : Cube n → ℝ) (hf : ∀ (x : Cube n), f x = 1 ∨ f x = -1) (P : Fin (n + 1) → Matrix (Cube n) (Cube n) ℂ) (hP : OrthogonalProjectionFamily P) (htrace : ∀ (k : Fin (n + 1)), (P k).trace.re = ↑(n.choose ↑k)) (htri : ∀ (i : Fin n), BlockTridiagonal P (coordinateSignMatrix i)) (hvanish : ∀ (r s : Fin (n + 1)), ↑r + ↑s < n - d → (P s * signMatrix fun (x : Cube n) => fullParity x * f x) * P r = 0) : averageSensitivity f ≤ 8 * ↑d * √↑n

The finite-matrix bound assuming an orthogonal projection family with binomial multiplicities, coordinate tridiagonality, and low-block vanishing.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialThreshold_averageSensitivity_le_of_nonzero {n d : ℕ} (p : MvPolynomial (Fin n) ℝ) (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) (hnz : ∀ (x : Cube n), polynomialValue p x ≠ 0) : averageSensitivity (polynomialThreshold p) ≤ 8 * ↑d * √↑n

The bound for a polynomial without cube zeros. The projection family and both block-vanishing properties are constructed from its absolute value, rather than retained as hypotheses.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialThreshold_averageSensitivity_le {n d : ℕ} (p : MvPolynomial (Fin n) ℝ) (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) : averageSensitivity (polynomialThreshold p) ≤ 8 * ↑d * √↑n

Every real multilinear polynomial of degree at most d has average sensitivity at most 8*d*sqrt(n), including cube zeros under sign(0)=1. The argument in fact covers all natural n and d.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.gotsmanLinialStatement : GotsmanLinialStatement

The average-sensitivity bound for 1 ≤ d ≤ n, without auxiliary construction hypotheses.