Gotsman--Linial: CoordinateDegree

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

Coordinate multiplication raises the Fourier degree by at most one

The unweighted polynomial degree bound is transported to the actual diagonal matrices and continuous linear operators on the counting-inner-product Euclidean space, including the shifted flag used by the weighted grading construction.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateSignMatrix_mem_fourierSpace {n k : ℕ} (i : Fin n) {a : Cube n → ℂ} (ha : a ∈ fourierSpace n k) : (coordinateSignMatrix i).mulVec a ∈ fourierSpace n (k + 1)

The actual coordinate-sign matrix raises the unweighted degree by at most one.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateMultiplier_mem_fourierEuclideanSpace {n k : ℕ} (i : Fin n) {a : EuclideanSpace ℂ (Cube n)} (ha : a ∈ fourierEuclideanSpace n k) : (coordinateMultiplier i) a ∈ fourierEuclideanSpace n (k + 1)

The continuous coordinate multiplier has the same degree shift in Euclidean space.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateMultiplier_map_fourierEuclideanSpace_le {n k : ℕ} (i : Fin n) : Submodule.map (↑(coordinateMultiplier i)) (fourierEuclideanSpace n k) ≤ fourierEuclideanSpace n (k + 1)

Submodule-map form of the Euclidean coordinate-degree shift.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateMultiplier_fourierFlag_shift {n : ℕ} (i : Fin n) (k : ℕ) (a : EuclideanSpace ℂ (Cube n)) : a ∈ fourierFlag n k → (coordinateMultiplier i) a ∈ fourierFlag n (k + 1)

The shifted flag also has a one-step coordinate shift, including its bottom term.