huang_matrix_squared

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

combinatoricslinear-algebrasensitivity-conjecture

Lemma 2.2 from Huang (2019): The Huang matrix A_n (a signed adjacency matrix of the n-dimensional hypercube with entries in {-1,0,1}) satisfies A_n^2 = nI. This is the key construction used to prove the Sensitivity Conjecture.

Preamble

import Mathlib.Analysis.Complex.Basic

/-- The signed adjacency matrix entry of the Huang matrix A_n.
    A_n[x,y] is nonzero iff x,y differ in exactly one coordinate k,
    in which case A_n[x,y] = (-1)^(number of true bits at positions < k in x). -/
noncomputable def huangEntry {n : ℕ} (x y : Fin n → Bool) : ℤ :=
  let diffSet := Finset.filter (fun i : Fin n => x i ≠ y i) Finset.univ
  if h : diffSet.card = 1 then
    let k := diffSet.min' (Finset.card_pos.mp (by omega))
    (-1 : ℤ) ^ (Finset.filter (fun j : Fin n => j < k ∧ x j = true) Finset.univ).card
  else 0

Formal statement

theorem huang_matrix_squared (n : ℕ) (x y : Fin n → Bool) : ∑ z : Fin n → Bool, huangEntry x z * huangEntry z y = if x = y then (↑n : ℤ) else 0 := by sorry

Source

https://arxiv.org/abs/1907.00847

View graph