Gotsman--Linial: SignParity

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

Removing threshold zeros and turning sensitive edges into constant-sign edges

All graph pairs are ordered. The cube coordinates are the real signs encoded by Bool in the public statement.

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fullParity {n : ℕ} (x : Cube n) : ℝ

Full parity, with values in the reals.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fullParity x = ∏ i : Fin n, Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeCoord x i

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.CubeAdjacent {n : ℕ} (x y : Cube n) : Prop

Two cube vertices differ by a single coordinate flip.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.CubeAdjacent x y = ∃ (i : Fin n), Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flip i x = y

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.orderedNeighborPairs (n : ℕ) : Finset (Cube n × Cube n)

All ordered pairs of neighboring vertices.

Equations

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

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.orderedConstantEdges {n : ℕ} (h : Cube n → ℝ) : Finset (Cube n × Cube n)

Ordered neighboring pairs at which a real function has equal values.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.orderedConstantEdges h = {e ∈ Complexity.BooleanAnalysis.PolynomialThreshold.Internal.orderedNeighborPairs n | h e.1 = h e.2}

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.exists_pos_shift_nonzero_preserves_sign {α : Type u_1} [Fintype α] (v : α → ℝ) : ∃ (ε : ℝ), 0 < ε ∧ (∀ (x : α), v x + ε ≠ 0) ∧ ∀ (x : α), thresholdSign (v x + ε) = thresholdSign (v x)

A positive constant removes all zeros of a real function on a finite set without changing its threshold signs, including the convention sign(0)=1.

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fullParity_sq {n : ℕ} (x : Cube n) : fullParity x ^ 2 = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fullParity_cases {n : ℕ} (x : Cube n) : fullParity x = 1 ∨ fullParity x = -1

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.fullParity_flip {n : ℕ} (i : Fin n) (x : Cube n) : fullParity (flip i x) = -fullParity x

Reversing one coordinate reverses full parity.

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hammingDist_flip {n : ℕ} (i : Fin n) (x : Cube n) : hammingDist x (flip i x) = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.adjacent_iff_hammingDist_eq_one {n : ℕ} (x y : Cube n) : CubeAdjacent x y ↔ hammingDist x y = 1

The flip definition of adjacency agrees with Hamming distance one.

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.directedEdgeEmbedding (n : ℕ) : Fin n × Cube n ↪ Cube n × Cube n

A vertex and a direction identify a unique ordered cube edge.

Equations

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

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.orderedNeighborPairs_eq_map {n : ℕ} : orderedNeighborPairs n = Finset.map (directedEdgeEmbedding n) Finset.univ

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.card_orderedNeighborPairs (n : ℕ) : (orderedNeighborPairs n).card = n * 2 ^ n

The n * 2^n count includes both orientations of every cube edge.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.card_orderedConstantEdges {n : ℕ} (h : Cube n → ℝ) : (orderedConstantEdges h).card = ∑ i : Fin n, {x : Cube n | h x = h (flip i x)}.card

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.parity_twist_eq_iff {n : ℕ} {f : Cube n → ℝ} (hf : ∀ (x : Cube n), f x = 1 ∨ f x = -1) (i : Fin n) (x : Cube n) : fullParity x * f x = fullParity (flip i x) * f (flip i x) ↔ f x ≠ f (flip i x)

Twisting a sign-valued function by parity changes sensitivity into equality across a coordinate flip.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.parity_twist_cases {n : ℕ} {f : Cube n → ℝ} (hf : ∀ (x : Cube n), f x = 1 ∨ f x = -1) (x : Cube n) : fullParity x * f x = 1 ∨ fullParity x * f x = -1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.card_orderedConstantEdges_parity {n : ℕ} {f : Cube n → ℝ} (hf : ∀ (x : Cube n), f x = 1 ∨ f x = -1) : (orderedConstantEdges fun (x : Cube n) => fullParity x * f x).card = sensitiveEdgeCount f

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.averageSensitivity_eq_parity_edges {n : ℕ} {f : Cube n → ℝ} (hf : ∀ (x : Cube n), f x = 1 ∨ f x = -1) : averageSensitivity f = ↑(orderedConstantEdges fun (x : Cube n) => fullParity x * f x).card / 2 ^ n

Exact uniform normalization: both sides count each sensitive undirected edge twice, once in each direction.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialThreshold_sensitivity_eq_parity_edges {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : averageSensitivity (polynomialThreshold p) = ↑(orderedConstantEdges fun (x : Cube n) => fullParity x * polynomialThreshold p x).card / 2 ^ n

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.ofReal_fullParity {n : ℕ} (x : Cube n) : ↑(fullParity x) = walshChar Finset.univ x

The real parity used for threshold signs is exactly the full complex Walsh character under the standard real embedding.

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialValue_add_C {n : ℕ} (p : MvPolynomial (Fin n) ℝ) (ε : ℝ) (x : Cube n) : polynomialValue (p + MvPolynomial.C ε) x = polynomialValue p x + ε

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.exists_nonzero_polynomial_same_threshold {n d : ℕ} {p : MvPolynomial (Fin n) ℝ} (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) : ∃ (q : MvPolynomial (Fin n) ℝ), IsMultilinear q ∧ q.totalDegree ≤ d ∧ (∀ (x : Cube n), polynomialValue q x ≠ 0) ∧ polynomialThreshold q = polynomialThreshold p

The zero-removal reduction preserves multilinearity, the degree bound, and the entire threshold function.