Gotsman--Linial: Commutator

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

Entry bounds for a tridiagonal grading commutator

All norms here are norms of individual complex entries. No default norm on a matrix is used. A complete orthogonal family defines a phase unitary with eigenvalues I^k. For a tridiagonal operator the commutator is the difference of two unitary conjugates divided by 2 I.

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.spectralMultiplier {κ : Type u_1} {ι : Type u_2} [Fintype κ] (P : κ → Matrix ι ι ℂ) (a : κ → ℂ) : Matrix ι ι ℂ

A complex spectral multiplier for a finite family of projections.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.spectralMultiplier P a = ∑ k : κ, a k • P k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.spectralMultiplier_mul_projection {κ : Type u_1} {ι : Type u_2} [Fintype κ] [DecidableEq κ] [Fintype ι] [DecidableEq ι] (P : κ → Matrix ι ι ℂ) (hmul : ∀ (r s : κ), P r * P s = if r = s then P r else 0) (a : κ → ℂ) (r : κ) : spectralMultiplier P a * P r = a r • P r

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.projection_mul_spectralMultiplier {κ : Type u_1} {ι : Type u_2} [Fintype κ] [DecidableEq κ] [Fintype ι] [DecidableEq ι] (P : κ → Matrix ι ι ℂ) (hmul : ∀ (r s : κ), P r * P s = if r = s then P r else 0) (a : κ → ℂ) (r : κ) : P r * spectralMultiplier P a = a r • P r

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.spectralMultiplier_mul {κ : Type u_1} {ι : Type u_2} [Fintype κ] [DecidableEq κ] [Fintype ι] [DecidableEq ι] (P : κ → Matrix ι ι ℂ) (hmul : ∀ (r s : κ), P r * P s = if r = s then P r else 0) (a b : κ → ℂ) : spectralMultiplier P a * spectralMultiplier P b = spectralMultiplier P fun (k : κ) => a k * b k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.star_spectralMultiplier {κ : Type u_1} {ι : Type u_2} [Fintype κ] (P : κ → Matrix ι ι ℂ) (hstar : ∀ (k : κ), star (P k) = P k) (a : κ → ℂ) : star (spectralMultiplier P a) = spectralMultiplier P fun (k : κ) => star (a k)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.spectralMultiplier_unitary {κ : Type u_1} {ι : Type u_2} [Fintype κ] [DecidableEq κ] [Fintype ι] [DecidableEq ι] (P : κ → Matrix ι ι ℂ) (hmul : ∀ (r s : κ), P r * P s = if r = s then P r else 0) (hstar : ∀ (k : κ), star (P k) = P k) (hsum : ∑ k : κ, P k = 1) (a : κ → ℂ) (ha : ∀ (k : κ), a k * star (a k) = 1) : spectralMultiplier P a ∈ Matrix.unitaryGroup ι ℂ

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.spectralMultiplier_sandwich_block {κ : Type u_1} {ι : Type u_2} [Fintype κ] [DecidableEq κ] [Fintype ι] [DecidableEq ι] (P : κ → Matrix ι ι ℂ) (hmul : ∀ (r s : κ), P r * P s = if r = s then P r else 0) (a b : κ → ℂ) (Z : Matrix ι ι ℂ) (r s : κ) : P s * (spectralMultiplier P a * Z * spectralMultiplier P b) * P r = (a s * b r) • (P s * Z * P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.spectralMultiplier_commutator_block {κ : Type u_1} {ι : Type u_2} [Fintype κ] [DecidableEq κ] [Fintype ι] [DecidableEq ι] (P : κ → Matrix ι ι ℂ) (hmul : ∀ (r s : κ), P r * P s = if r = s then P r else 0) (a : κ → ℂ) (Z : Matrix ι ι ℂ) (r s : κ) : P s * (spectralMultiplier P a * Z - Z * spectralMultiplier P a) * P r = (a s - a r) • (P s * Z * P r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.spectral_blocks_reconstruct {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (P : κ → Matrix ι ι ℂ) (hsum : ∑ k : κ, P k = 1) (B : Matrix ι ι ℂ) : ∑ s : κ, ∑ r : κ, P s * B * P r = B

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.spectral_blocks_ext {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (P : κ → Matrix ι ι ℂ) (hsum : ∑ k : κ, P k = 1) (A B : Matrix ι ι ℂ) (h : ∀ (r s : κ), P s * A * P r = P s * B * P r) : A = B

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.I_pow_mul_star (k : ℕ) : Complex.I ^ k * star (Complex.I ^ k) = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.phase_coeff_adjacent (r s : ℕ) (h₁ : s ≤ r + 1) (h₂ : r ≤ s + 1) : Complex.I ^ s * star (Complex.I ^ r) - star (Complex.I ^ s) * Complex.I ^ r = 2 * Complex.I * (↑s - ↑r)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.entry_norm_le_one_of_two_unitaries {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C U V : Matrix ι ι ℂ) (hU : U ∈ Matrix.unitaryGroup ι ℂ) (hV : V ∈ Matrix.unitaryGroup ι ℂ) (h : (2 * Complex.I) • C = U - V) (x y : ι) : ‖C x y‖ ≤ 1

The difference of two unitary matrices, divided by 2 I, has entries of modulus at most one.

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.gradingPhase {n : ℕ} {ι : Type u_1} (P : Fin (n + 1) → Matrix ι ι ℂ) : Matrix ι ι ℂ

The spectral phase I^k of the degree grading.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.gradingPhase P = Complexity.BooleanAnalysis.PolynomialThreshold.Internal.spectralMultiplier P fun (k : Fin (n + 1)) => Complex.I ^ ↑k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.gradingPhase_unitary {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) : gradingPhase P ∈ Matrix.unitaryGroup ι ℂ

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.BlockTridiagonal {n : ℕ} {ι : Type u_1} [Fintype ι] (P : Fin (n + 1) → Matrix ι ι ℂ) (Z : Matrix ι ι ℂ) : Prop

Tridiagonality means that blocks at grading distance greater than one vanish.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.BlockTridiagonal P Z = ∀ (r s : Fin (n + 1)), ↑r + 1 < ↑s ∨ ↑s + 1 < ↑r → P s * Z * P r = 0

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.grading_commutator_phase_identity {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (Z : Matrix ι ι ℂ) (htri : BlockTridiagonal P Z) : (2 * Complex.I) • (degreeGrading P * Z - Z * degreeGrading P) = gradingPhase P * Z * star (gradingPhase P) - star (gradingPhase P) * Z * gradingPhase P

Two opposite phase conjugations differ by 2 I times the grading commutator.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.norm_degreeGrading_commutator_entry_le_one {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (Z : Matrix ι ι ℂ) (htri : BlockTridiagonal P Z) (hZ : Z ∈ Matrix.unitaryGroup ι ℂ) (x y : ι) : ‖(degreeGrading P * Z - Z * degreeGrading P) x y‖ ≤ 1

Every entry of the tridiagonal degree commutator has modulus at most one.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_degreeGrading_commutator_le {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (Z : Matrix ι ι ℂ) (htri : BlockTridiagonal P Z) : hsNormSq (degreeGrading P * Z - Z * degreeGrading P) ≤ hsNormSq Z

The Hilbert--Schmidt commutator bound is a consequence of block Parseval and the fact that each nonzero block has grading distance at most one.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_degreeGrading_commutator_le_card {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (Z : Matrix ι ι ℂ) (htri : BlockTridiagonal P Z) (hZ : Z ∈ Matrix.unitaryGroup ι ℂ) : hsNormSq (degreeGrading P * Z - Z * degreeGrading P) ≤ ↑(Fintype.card ι)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.centeredGrading_commutator_eq {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (Z : Matrix ι ι ℂ) : centeredGrading P * Z - Z * centeredGrading P = degreeGrading P * Z - Z * degreeGrading P

Centering the grading does not change its commutator.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.norm_centeredGrading_commutator_entry_le_one {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (Z : Matrix ι ι ℂ) (htri : BlockTridiagonal P Z) (hZ : Z ∈ Matrix.unitaryGroup ι ℂ) (x y : ι) : ‖(centeredGrading P * Z - Z * centeredGrading P) x y‖ ≤ 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sq_norm_centeredGrading_commutator_entry_le_one {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (Z : Matrix ι ι ℂ) (htri : BlockTridiagonal P Z) (hZ : Z ∈ Matrix.unitaryGroup ι ℂ) (x y : ι) : ‖(centeredGrading P * Z - Z * centeredGrading P) x y‖ ^ 2 ≤ 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.hsNormSq_centeredGrading_commutator_le_card {n : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P) (Z : Matrix ι ι ℂ) (htri : BlockTridiagonal P Z) (hZ : Z ∈ Matrix.unitaryGroup ι ℂ) : hsNormSq (centeredGrading P * Z - Z * centeredGrading P) ≤ ↑(Fintype.card ι)