Gotsman--Linial: Model

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/Model.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.

Polynomial thresholds and average sensitivity

The Boolean cube encodes the sign cube {−1,1}^n: false represents −1 and true represents 1. The public statement quantifies directly over real multilinear polynomials and uses uniform counting probability, the convention sign(0) = 1, and the exact constant 8.

GotsmanLinialStatement is a proposition definition, not a proof of the bound.

@[reducible, inline]

abbrev Complexity.BooleanAnalysis.PolynomialThreshold.Internal.Cube (n : ℕ) : Type

The sign cube {−1,1}^n, with Boolean coordinates encoding the signs.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.Cube n = (Fin n → Bool)

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeCoord {n : ℕ} (x : Cube n) (i : Fin n) : ℝ

Interpret a Boolean cube coordinate as the corresponding real sign.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeCoord x i = if x i = true then 1 else -1

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flip {n : ℕ} (i : Fin n) (x : Cube n) : Cube n

Reverse one coordinate of a cube vertex.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flip i x = Function.update x i !x i

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.thresholdSign (t : ℝ) : ℝ

The threshold convention assigns 1 at zero.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.thresholdSign t = if 0 ≤ t then 1 else -1

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sensitiveVertices {n : ℕ} (f : Cube n → ℝ) (i : Fin n) : Finset (Cube n)

Vertices at which reversing coordinate i changes the function.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sensitiveEdgeCount {n : ℕ} (f : Cube n → ℝ) : ℕ

Number of ordered sensitive edges, indexed by their initial vertex and direction.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sensitiveEdgeCount f = ∑ i : Fin n, (Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sensitiveVertices f i).card

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.averageSensitivity {n : ℕ} (f : Cube n → ℝ) : ℝ

Sum of the uniform probabilities that a coordinate flip changes f.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.averageSensitivity f = ∑ i : Fin n, ↑(Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sensitiveVertices f i).card / 2 ^ n

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.IsMultilinear {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : Prop

Every exponent in every supported monomial is at most one.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.IsMultilinear p = ∀ m ∈ p.support, ∀ (i : Fin n), m i ≤ 1

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialValue {n : ℕ} (p : MvPolynomial (Fin n) ℝ) (x : Cube n) : ℝ

Evaluate a real polynomial at the signs represented by a cube vertex.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialValue p x = (MvPolynomial.eval (Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeCoord x)) p

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialThreshold {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : Cube n → ℝ

The polynomial threshold function with the nonnegative-at-zero convention.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.GotsmanLinialStatement : Prop

The average-sensitivity bound for positive dimension and degree at most the dimension.

Equations

• One or more equations did not get rendered due to their size.