Gotsman--Linial: GradingShift

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

A degree shift is tridiagonal in the associated orthogonal grading

These lemmas retain the degree-shift premise explicitly. The cube application discharges it using coordinate multiplication and the weighted Fourier flag.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.instCompleteSpace_complexitylib_3 {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : CompleteSpace E

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjection_mul_shift_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (Z : E →L[𝕜] E) (hshift : ∀ (k : ℕ), ∀ x ∈ K k, Z x ∈ K (k + 1)) {r s : ℕ} (hrs : r + 1 < s) : flagProjection K s * Z * flagProjection K r = 0

An operator that raises the flag index by at most one has no blocks strictly above the first off-diagonal.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flagProjection_tridiagonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (Z : E →L[𝕜] E) (hZ : IsSelfAdjoint Z) (hshift : ∀ (k : ℕ), ∀ x ∈ K k, Z x ∈ K (k + 1)) {r s : ℕ} (hrs : r + 1 < s ∨ s + 1 < r) : flagProjection K s * Z * flagProjection K r = 0

Self-adjointness gives the other half of the band by taking adjoints.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.map_flagProjection_tridiagonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : Type u_3} [Ring A] (F : (E →L[𝕜] E) →+* A) (K : ℕ → Submodule 𝕜 E) (hK : Monotone K) (Z : E →L[𝕜] E) (hZ : IsSelfAdjoint Z) (hshift : ∀ (k : ℕ), ∀ x ∈ K k, Z x ∈ K (k + 1)) {r s : ℕ} (hrs : r + 1 < s ∨ s + 1 < r) : F (flagProjection K s) * F Z * F (flagProjection K r) = 0

The band property is preserved by taking matrices or any other ring representation of the operator algebra.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.shift_mem_map_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (V : ℕ → Submodule 𝕜 E) (D Z : E →ₗ[𝕜] E) (hcommute : ∀ (x : E), Z (D x) = D (Z x)) (hshift : ∀ (k : ℕ), ∀ x ∈ V k, Z x ∈ V (k + 1)) (k : ℕ) {x : E} (hx : x ∈ Submodule.map D (V k)) : Z x ∈ Submodule.map D (V (k + 1))

Commutation transports a degree-shift statement through a weight map.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.instCompleteSpace_complexitylib_4 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] : CompleteSpace E

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.operatorMatrix_flagProjection_tridiagonal {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι ℂ E) (K : ℕ → Submodule ℂ E) (hK : Monotone K) (Z : E →L[ℂ] E) (hZ : IsSelfAdjoint Z) (hshift : ∀ (k : ℕ), ∀ x ∈ K k, Z x ∈ K (k + 1)) (n : ℕ) (r s : Fin (n + 1)) (hrs : ↑r + 1 < ↑s ∨ ↑s + 1 < ↑r) : operatorMatrix b (flagProjection K ↑s) * operatorMatrix b Z * operatorMatrix b (flagProjection K ↑r) = 0

The concrete matrix form consumed by the commutator estimate.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateMultiplier_sqrtWeight_commute {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (i : Fin n) (a : EuclideanSpace ℂ (Cube n)) : (coordinateMultiplier i) ((sqrtWeightEquiv w hw) a) = (sqrtWeightEquiv w hw) ((coordinateMultiplier i) a)

Coordinate signs commute with the actual positive square-root weight.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinateMultiplier_weightedFlag_shift {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (i : Fin n) (k : ℕ) (a : EuclideanSpace ℂ (Cube n)) : a ∈ transportFlag (sqrtWeightEquiv w hw) (fourierFlag n) k → (coordinateMultiplier i) a ∈ transportFlag (sqrtWeightEquiv w hw) (fourierFlag n) (k + 1)

The actual weighted Fourier flag retains the one-step coordinate shift.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedFlag_operatorMatrix_tridiagonal {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (b : OrthonormalBasis (Cube n) ℂ (EuclideanSpace ℂ (Cube n))) (i : Fin n) (r s : Fin (n + 1)) (hrs : ↑r + 1 < ↑s ∨ ↑s + 1 < ↑r) : flagProjectionMatrix b (transportFlag (sqrtWeightEquiv w hw) (fourierFlag n)) ↑s * operatorMatrix b (coordinateMultiplier i) * flagProjectionMatrix b (transportFlag (sqrtWeightEquiv w hw) (fourierFlag n)) ↑r = 0

Tridiagonality for the actually constructed weighted Fourier projections, expressed in an arbitrary orthonormal coordinate system.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedProjectionMatrix_tridiagonal {n : ℕ} (w : Cube n → ℝ) (hw : ∀ (x : Cube n), 0 < w x) (i : Fin n) (r s : Fin (n + 1)) (hrs : ↑r + 1 < ↑s ∨ ↑s + 1 < ↑r) : weightedProjectionMatrix w hw s * coordinateSignMatrix i * weightedProjectionMatrix w hw r = 0

The raw coordinate-sign matrices are tridiagonal for the actual weighted Fourier projection family. There is no remaining degree-shift hypothesis.