Gotsman--Linial: BlockVanishing

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

Vanishing of low antidiagonal blocks

The geometric step is reduced to an explicit finite sum: multiplication on both sides by the square root of a positive weight turns the weighted pairing into a Fourier pairing against the signed weight.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.abs_mul_thresholdSign (t : ℝ) : |t| * thresholdSign t = t

The threshold convention at zero is compatible with the signed absolute value identity used to build the weighted grading.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.projectionBlock_eq_zero_of_pairing {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (H : E →L[𝕜] E) (hpair : ∀ u ∈ U, ∀ v ∈ V, inner 𝕜 v (H u) = 0) : V.starProjection * H * U.starProjection = 0

If the image of one subspace under an operator is orthogonal to a second subspace, the corresponding projection block vanishes.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.projectionBlock_eq_zero_of_map_pairing {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A B U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (D : E →ₗ[𝕜] E) (H : E →L[𝕜] E) (hU : U ≤ Submodule.map D A) (hV : V ≤ Submodule.map D B) (hpair : ∀ a ∈ A, ∀ b ∈ B, inner 𝕜 (D b) (H (D a)) = 0) : V.starProjection * H * U.starProjection = 0

Lift an orthogonality calculation on preimages through a common linear map to a zero block between subspaces of its images.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sqrtWeight_inner_eq_sum {Ω : Type u_1} [Fintype Ω] (w h : Ω → ℝ) (hw : ∀ (x : Ω), 0 ≤ w x) (D : EuclideanSpace ℂ Ω →ₗ[ℂ] EuclideanSpace ℂ Ω) (hD : ∀ (a : EuclideanSpace ℂ Ω) (x : Ω), (D a).ofLp x = ↑√(w x) * a.ofLp x) (H : EuclideanSpace ℂ Ω →L[ℂ] EuclideanSpace ℂ Ω) (hH : ∀ (a : EuclideanSpace ℂ Ω) (x : Ω), (H a).ofLp x = ↑(h x) * a.ofLp x) (a b : EuclideanSpace ℂ Ω) : inner ℂ (D b) (H (D a)) = ∑ x : Ω, star (b.ofLp x) * a.ofLp x * (↑(w x) * ↑(h x))

The finite pairing identity underlying the low antidiagonal cutoff. The norm and inner product are the counting Euclidean ones.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sqrtWeight_inner_eq_sum_signedWeight {Ω : Type u_1} [Fintype Ω] (w h : Ω → ℝ) (q : Ω → ℂ) (hw : ∀ (x : Ω), 0 ≤ w x) (hwq : ∀ (x : Ω), ↑(w x) * ↑(h x) = q x) (D : EuclideanSpace ℂ Ω →ₗ[ℂ] EuclideanSpace ℂ Ω) (hD : ∀ (a : EuclideanSpace ℂ Ω) (x : Ω), (D a).ofLp x = ↑√(w x) * a.ofLp x) (H : EuclideanSpace ℂ Ω →L[ℂ] EuclideanSpace ℂ Ω) (hH : ∀ (a : EuclideanSpace ℂ Ω) (x : Ω), (H a).ofLp x = ↑(h x) * a.ofLp x) (a b : EuclideanSpace ℂ Ω) : inner ℂ (D b) (H (D a)) = ∑ x : Ω, star (b.ofLp x) * a.ofLp x * q x

Replace the weight times the diagonal sign by the actual signed weight.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sqrtWeight_pairing_eq_zero_of_fourier_separation {n r s k : ℕ} (w h : Cube n → ℝ) (q : Cube n → ℂ) (hw : ∀ (x : Cube n), 0 ≤ w x) (hwq : ∀ (x : Cube n), ↑(w x) * ↑(h x) = q x) (D : EuclideanSpace ℂ (Cube n) →ₗ[ℂ] EuclideanSpace ℂ (Cube n)) (hD : ∀ (a : EuclideanSpace ℂ (Cube n)) (x : Cube n), (D a).ofLp x = ↑√(w x) * a.ofLp x) (H : EuclideanSpace ℂ (Cube n) →L[ℂ] EuclideanSpace ℂ (Cube n)) (hH : ∀ (a : EuclideanSpace ℂ (Cube n)) (x : Cube n), (H a).ofLp x = ↑(h x) * a.ofLp x) (a b : EuclideanSpace ℂ (Cube n)) (ha : a.ofLp ∈ fourierSpace n r) (hb : b.ofLp ∈ fourierSpace n s) (hq : q ∈ fourierSpaceFrom n k) (hrs : r + s < k) : inner ℂ (D b) (H (D a)) = 0

High Fourier support of the signed weight kills every pairing whose two unweighted degrees have smaller total degree.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomial_signedWeight {n : ℕ} (p : MvPolynomial (Fin n) ℝ) (x : Cube n) : ↑|polynomialValue p x| * ↑(fullParity x * thresholdSign (polynomialValue p x)) = walshChar Finset.univ x * ↑(polynomialValue p x)

The choices w = |p| and h = parity * sign(p) multiply to the high-degree signed polynomial, including at a zero of the polynomial.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomial_sqrtWeight_pairing_eq_zero {n d r s : ℕ} (p : MvPolynomial (Fin n) ℝ) (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) (hnz : ∀ (x : Cube n), polynomialValue p x ≠ 0) (a b : EuclideanSpace ℂ (Cube n)) (ha : a.ofLp ∈ fourierSpace n r) (hb : b.ofLp ∈ fourierSpace n s) (hrs : r + s < n - d) : have D := sqrtWeightEquiv (fun (x : Cube n) => |polynomialValue p x|) ⋯; inner ℂ (D b) ((signMultiplier fun (x : Cube n) => fullParity x * thresholdSign (polynomialValue p x)) (D a)) = 0

The weighted pairing vanishes for the polynomial, weight, and parity-modified threshold sign. No Fourier-support assumption remains.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomial_projectionBlock_eq_zero {n d r s : ℕ} (p : MvPolynomial (Fin n) ℝ) (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) (hnz : ∀ (x : Cube n), polynomialValue p x ≠ 0) (U V : Submodule ℂ (EuclideanSpace ℂ (Cube n))) (hU : U ≤ weightedFourierSpace (fun (x : Cube n) => |polynomialValue p x|) ⋯ r) (hV : V ≤ weightedFourierSpace (fun (x : Cube n) => |polynomialValue p x|) ⋯ s) (hrs : r + s < n - d) : (V.starProjection * signMultiplier fun (x : Cube n) => fullParity x * thresholdSign (polynomialValue p x)) * U.starProjection = 0

The operator between two subspaces of weighted low-degree spaces is zero below the polynomial's degree cutoff.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedFlag_block_eq_zero_of_polynomial_degree {n d r s : ℕ} (p : MvPolynomial (Fin n) ℝ) (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) (hnz : ∀ (x : Cube n), polynomialValue p x ≠ 0) (hrs : r + s < n - d) : have K := weightedFourierFlag (fun (x : Cube n) => |polynomialValue p x|) ⋯; (flagProjection K s * signMultiplier fun (x : Cube n) => fullParity x * thresholdSign (polynomialValue p x)) * flagProjection K r = 0

Low antidiagonal vanishing for the actual weighted grading constructed from the polynomial. All geometric hypotheses are discharged.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedFlag_matrixBlock_eq_zero_of_polynomial_degree {n d r s : ℕ} (p : MvPolynomial (Fin n) ℝ) (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) (hnz : ∀ (x : Cube n), polynomialValue p x ≠ 0) (hrs : r + s < n - d) {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι ℂ (EuclideanSpace ℂ (Cube n))) : have K := weightedFourierFlag (fun (x : Cube n) => |polynomialValue p x|) ⋯; operatorMatrix b (flagProjection K s) * operatorMatrix b (signMultiplier fun (x : Cube n) => fullParity x * thresholdSign (polynomialValue p x)) * operatorMatrix b (flagProjection K r) = 0

The same vanishing statement in any orthonormal matrix coordinates, ready for the Hilbert-Schmidt block coupling.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.weightedProjectionMatrix_block_eq_zero_of_polynomial_degree {n d : ℕ} (p : MvPolynomial (Fin n) ℝ) (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) (hnz : ∀ (x : Cube n), polynomialValue p x ≠ 0) (r s : Fin (n + 1)) (hrs : ↑r + ↑s < n - d) : let w := fun (x : Cube n) => |polynomialValue p x|; have hw := ⋯; (weightedProjectionMatrix w hw s * signMatrix fun (x : Cube n) => fullParity x * polynomialThreshold p x) * weightedProjectionMatrix w hw r = 0

The concrete cutoff used by the finite block coupling: actual weighted projection matrices, actual diagonal parity-modified polynomial threshold, and no unproved construction assumptions.