Gotsman--Linial: EdgeRecovery

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

Recovering constant-sign edges from grading energy

The counting argument is separated from construction of the grading matrix. Its hypotheses are explicit entrywise, total-energy, and distance-energy facts. No edge-count or anticommutator conclusion is assumed.

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.distanceShell {α : Type u_1} [Fintype α] (d : α → ℕ) (k : ℕ) : Finset α

A finite distance layer, also useful for weights indexed by ordered pairs.

Equations

• Complexity.BooleanAnalysis.PolynomialThreshold.Internal.distanceShell d k = {a : α | d a = k}

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.mem_distanceShell {α : Type u_1} [Fintype α] (d : α → ℕ) (k : ℕ) (a : α) : a ∈ distanceShell d k ↔ d a = k

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.twice_mass_sub_neighbor_le_distance {α : Type u_1} [Fintype α] (d : α → ℕ) (w : α → ℝ) (hw : ∀ (a : α), 0 ≤ w a) : 2 * ∑ a : α, w a - ∑ a ∈ distanceShell d 1, w a ≤ 2 * ∑ a ∈ distanceShell d 0, w a + ∑ a : α, ↑(d a) * w a

Pointwise distance counting: distance-zero entries are the only possible source of a deficit between total mass and distance-weighted mass.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.neighbor_deficit_le_twice_zero_mass {α : Type u_1} [Fintype α] (d : α → ℕ) (w : α → ℝ) (hw : ∀ (a : α), 0 ≤ w a) (htotal : ∑ a : α, w a = ↑(distanceShell d 1).card / 4) (henergy : ∑ a : α, ↑(d a) * w a ≤ ∑ a : α, w a) : ∑ a ∈ distanceShell d 1, (1 / 4 - w a) ≤ 2 * ∑ a ∈ distanceShell d 0, w a

The sum of the nonnegative neighbor deficits is controlled by twice the distance-zero energy. Equivalently, A₀ + F ≤ 2 A₀.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.selected_neighbor_card_le_eight_mass {α : Type u_1} [Fintype α] (d : α → ℕ) (w : α → ℝ) (s : Finset α) (hs : s ⊆ distanceShell d 1) (hw : ∀ (a : α), 0 ≤ w a) (hcap : ∀ a ∈ distanceShell d 1, w a ≤ 1 / 4) (htotal : ∑ a : α, w a = ↑(distanceShell d 1).card / 4) (henergy : ∑ a : α, ↑(d a) * w a ≤ ∑ a : α, w a) : ↑s.card ≤ 8 * (∑ a ∈ distanceShell d 0, w a + ∑ a ∈ s, w a)

Restricting the nonnegative deficits to any chosen neighbor subset gives the counting bound needed before applying the anticommutator identity.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.anticommutator_entry_sq_of_same_sign {ι : Type u_2} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℂ) (h : ι → ℝ) (hh : ∀ (i : ι), h i = 1 ∨ h i = -1) (i j : ι) (hij : h i = h j) : ‖((M * Matrix.diagonal fun (i : ι) => ↑(h i)) + (Matrix.diagonal fun (i : ι) => ↑(h i)) * M) i j‖ ^ 2 = 4 * ‖M i j‖ ^ 2

On an equal-sign pair the anticommutator has four times the squared entry mass. The diagonal is included as an equal-sign pair.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.anticommutator_energy_ge_selected {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ρ : ι → ι → ℕ) (hzero : ∀ (i j : ι), ρ i j = 0 → i = j) (M : Matrix ι ι ℂ) (h : ι → ℝ) (hh : ∀ (i : ι), h i = 1 ∨ h i = -1) (s : Finset (ι × ι)) (hs : s ⊆ distanceShell (fun (p : ι × ι) => ρ p.1 p.2) 1) (hsign : ∀ p ∈ s, h p.1 = h p.2) : 4 * (∑ p ∈ distanceShell (fun (p : ι × ι) => ρ p.1 p.2) 0, ‖M p.1 p.2‖ ^ 2 + ∑ p ∈ s, ‖M p.1 p.2‖ ^ 2) ≤ hsNormSq ((M * Matrix.diagonal fun (i : ι) => ↑(h i)) + (Matrix.diagonal fun (i : ι) => ↑(h i)) * M)

The diagonal and a disjoint set of equal-sign neighbor entries contribute four times their mass to the Hilbert--Schmidt squared norm.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.edge_recovery_for_subset {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ρ : ι → ι → ℕ) (hzero : ∀ (i j : ι), ρ i j = 0 → i = j) (M : Matrix ι ι ℂ) (h : ι → ℝ) (hh : ∀ (i : ι), h i = 1 ∨ h i = -1) (s : Finset (ι × ι)) (hs : s ⊆ distanceShell (fun (p : ι × ι) => ρ p.1 p.2) 1) (hsign : ∀ p ∈ s, h p.1 = h p.2) (hcap : ∀ (i j : ι), ρ i j = 1 → ‖M i j‖ ^ 2 ≤ 1 / 4) (htotal : hsNormSq M = ↑(distanceShell (fun (p : ι × ι) => ρ p.1 p.2) 1).card / 4) (henergy : ∑ i : ι, ∑ j : ι, ↑(ρ i j) * ‖M i j‖ ^ 2 ≤ hsNormSq M) : ↑s.card ≤ 2 * hsNormSq ((M * Matrix.diagonal fun (i : ι) => ↑(h i)) + (Matrix.diagonal fun (i : ι) => ↑(h i)) * M)

Abstract edge recovery from the exact finite matrix energy hypotheses. The chosen set may be any subset of constant-sign distance-one pairs.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.edge_recovery {n : ℕ} (M : Matrix (Cube n) (Cube n) ℂ) (h : Cube n → ℝ) (hh : ∀ (x : Cube n), h x = 1 ∨ h x = -1) (htotal : hsNormSq M = ↑n * 2 ^ n / 4) (hdistance : ∑ x : Fin n → Bool, ∑ y : Fin n → Bool, ↑(hammingDist x y) * ‖M x y‖ ^ 2 ≤ hsNormSq M) (hcap : ∀ (x y : Cube n), x ≠ y → ‖M x y‖ ^ 2 ≤ 1 / 4) : ↑(orderedConstantEdges h).card ≤ 2 * hsNormSq ((M * Matrix.diagonal fun (x : Cube n) => ↑(h x)) + (Matrix.diagonal fun (x : Cube n) => ↑(h x)) * M)

The edge-recovery inequality on the Boolean cube, from the three matrix facts established by the grading and commutator constructions.