Gotsman--Linial: CubeOperators

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/CubeOperators.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 commutators and Hamming-distance energy

The coordinate sign matrices are the actual diagonal operators of the Boolean cube. The identities here turn their Hilbert--Schmidt and entry estimates into the energy estimates used by the edge-recovery argument.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinate_commutator_apply {n : ℕ} (M : Matrix (Cube n) (Cube n) ℂ) (i : Fin n) (x y : Cube n) : (M * coordinateSignMatrix i - coordinateSignMatrix i * M) x y = ↑(cubeCoord y i - cubeCoord x i) * M x y

In the point basis, a coordinate commutator records the difference of the two endpoint signs.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.coordinate_commutator_sq_norm {n : ℕ} (M : Matrix (Cube n) (Cube n) ℂ) (i : Fin n) (x y : Cube n) : ‖(M * coordinateSignMatrix i - coordinateSignMatrix i * M) x y‖ ^ 2 = (if x i ≠ y i then 4 else 0) * ‖M x y‖ ^ 2

Squaring a coordinate difference gives four exactly on the coordinates where the Boolean endpoints differ.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_coordinate_commutator_sq_norm {n : ℕ} (M : Matrix (Cube n) (Cube n) ℂ) (x y : Cube n) : ∑ i : Fin n, ‖(M * coordinateSignMatrix i - coordinateSignMatrix i * M) x y‖ ^ 2 = 4 * ↑(hammingDist x y) * ‖M x y‖ ^ 2

Summing the squared entries over coordinates counts Hamming distance.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_hsNormSq_coordinate_commutator {n : ℕ} (M : Matrix (Cube n) (Cube n) ℂ) : ∑ i : Fin n, hsNormSq (M * coordinateSignMatrix i - coordinateSignMatrix i * M) = 4 * ∑ x : Cube n, ∑ y : Cube n, ↑(hammingDist x y) * ‖M x y‖ ^ 2

The total coordinate-commutator energy is four times the distance-weighted entry energy.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.distance_energy_le_of_coordinate_commutator_bound {n : ℕ} (M : Matrix (Cube n) (Cube n) ℂ) (hbound : ∀ (i : Fin n), hsNormSq (M * coordinateSignMatrix i - coordinateSignMatrix i * M) ≤ 2 ^ n) : ∑ x : Cube n, ∑ y : Cube n, ↑(hammingDist x y) * ‖M x y‖ ^ 2 ≤ ↑n * 2 ^ n / 4

A uniform coordinate-commutator Hilbert--Schmidt bound gives the distance energy inequality for the actual cube matrix.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.off_diagonal_sq_norm_le_quarter_of_commutator_bound {n : ℕ} (M : Matrix (Cube n) (Cube n) ℂ) (hbound : ∀ (i : Fin n) (x y : Cube n), ‖(M * coordinateSignMatrix i - coordinateSignMatrix i * M) x y‖ ^ 2 ≤ 1) (x y : Cube n) (hxy : x ≠ y) : ‖M x y‖ ^ 2 ≤ 1 / 4

A coordinate at which distinct endpoints differ turns an entrywise commutator estimate into the edge-entry cap 1/4.