Huang's sensitivity theorem

A formalization of Hao Huang's sensitivity theorem: in the hypercube of dimension n ≥ 1, if one colors more than half the vertices then at least one vertex has at least √n colored neighbors.

A fun summer collaboration by Reid Barton, Johan Commelin, Jesse Han, Chris Hughes, Robert Y. Lewis, and Patrick Massot, based on Don Knuth's account of the story (https://www.cs.stanford.edu/~knuth/papers/huang.pdf), using the Lean theorem prover (https://leanprover.github.io/), by Leonardo de Moura at Microsoft Research, and his collaborators (https://leanprover.github.io/people/), and using Lean's user maintained mathematics library (https://github.com/leanprover-community/mathlib).

The project was developed at https://github.com/leanprover-community/lean-sensitivity and is now archived at https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean

The next two lines assert we do not want to give a constructive proof, but rather use classical logic.

We also want to use the notation ∑ for sums.

The hypercube

Notations:

• ℕ denotes natural numbers (including zero).
• Fin n = {0, ⋯ , n - 1}.
• Bool = {true, false}.

def Sensitivity.Q (n : ℕ) : Type

The hypercube in dimension n.

instance Sensitivity.instInhabitedQ (n : ℕ) : Inhabited (Sensitivity.Q n)

instance Sensitivity.instFintypeQ (n : ℕ) : Fintype (Sensitivity.Q n)

def Sensitivity.π {n : ℕ} : Sensitivity.Q (Nat.succ n) → Sensitivity.Q n

The projection from Q n.succ to Q n forgetting the first value (ie. the image of zero).

theorem Sensitivity.Q.ext {n : ℕ} {f : Sensitivity.Q n} {g : Sensitivity.Q n} (h : ∀ (x : Fin n), f x = g x) : f = g

n will always denote a natural number.

instance Sensitivity.Q.instUniqueQOfNatNatInstOfNatNat : Unique (Sensitivity.Q 0)

Q 0 has a unique element.

theorem Sensitivity.Q.card (n : ℕ) : Fintype.card (Sensitivity.Q n) = 2 ^ n

Q n has 2^n elements.

Until the end of this namespace, n will be an implicit argument (still a natural number).

theorem Sensitivity.Q.succ_n_eq {n : ℕ} (p : Sensitivity.Q (Nat.succ n)) (q : Sensitivity.Q (Nat.succ n)) : p = q ↔ p 0 = q 0 ∧ Sensitivity.π p = Sensitivity.π q

def Sensitivity.Q.adjacent {n : ℕ} (p : Sensitivity.Q n) : Set (Sensitivity.Q n)

The adjacency relation defining the graph structure on Q n: p.adjacent q if there is an edge from p to q in Q n.

theorem Sensitivity.Q.not_adjacent_zero (p : Sensitivity.Q 0) (q : Sensitivity.Q 0) : ¬q ∈ Sensitivity.Q.adjacent p

In Q 0, no two vertices are adjacent.

theorem Sensitivity.Q.adj_iff_proj_eq {n : ℕ} {p : Sensitivity.Q (Nat.succ n)} {q : Sensitivity.Q (Nat.succ n)} (h₀ : p 0 ≠ q 0) : q ∈ Sensitivity.Q.adjacent p ↔ Sensitivity.π p = Sensitivity.π q

If p and q in Q n.succ have different values at zero then they are adjacent iff their projections to Q n are equal.

theorem Sensitivity.Q.adj_iff_proj_adj {n : ℕ} {p : Sensitivity.Q (Nat.succ n)} {q : Sensitivity.Q (Nat.succ n)} (h₀ : p 0 = q 0) : q ∈ Sensitivity.Q.adjacent p ↔ Sensitivity.π q ∈ Sensitivity.Q.adjacent (Sensitivity.π p)

If p and q in Q n.succ have the same value at zero then they are adjacent iff their projections to Q n are adjacent.

theorem Sensitivity.Q.adjacent.symm {n : ℕ} {p : Sensitivity.Q n} {q : Sensitivity.Q n} : q ∈ Sensitivity.Q.adjacent p ↔ p ∈ Sensitivity.Q.adjacent q

The vector space

def Sensitivity.V : ℕ → Type

The free vector space on vertices of a hypercube, defined inductively.

Equations

• Sensitivity.V 0 = ℝ
• Sensitivity.V (Nat.succ n) = (Sensitivity.V n × Sensitivity.V n)

theorem Sensitivity.V.ext {n : ℕ} {p : Sensitivity.V (Nat.succ n)} {q : Sensitivity.V (Nat.succ n)} (h₁ : p.fst = q.fst) (h₂ : p.snd = q.snd) : p = q

V n is a real vector space whose equality relation is computable.

instance Sensitivity.V.instDecidableEqV (n : ℕ) : DecidableEq (Sensitivity.V n)

instance Sensitivity.V.instAddCommGroupV (n : ℕ) : AddCommGroup (Sensitivity.V n)

instance Sensitivity.V.instModuleRealVSemiringToAddCommMonoidInstAddCommGroupV (n : ℕ) : Module ℝ (Sensitivity.V n)

noncomputable def Sensitivity.e {n : ℕ} : Sensitivity.Q n → Sensitivity.V n

The basis of V indexed by the hypercube, defined inductively.

Equations

• Sensitivity.e = fun x => 1
• Sensitivity.e = fun x => bif x 0 then (Sensitivity.e (Sensitivity.π x), 0) else (0, Sensitivity.e (Sensitivity.π x))

@[simp]

theorem Sensitivity.e_zero_apply (x : Sensitivity.Q 0) : Sensitivity.e x = 1

noncomputable def Sensitivity.ε {n : ℕ} : Sensitivity.Q n → Sensitivity.V n →ₗ[ℝ] ℝ

The dual basis to e, defined inductively.

Equations

• One or more equations did not get rendered due to their size.
• Sensitivity.ε x_2 = LinearMap.id

theorem Sensitivity.duality {n : ℕ} (p : Sensitivity.Q n) (q : Sensitivity.Q n) : ↑(Sensitivity.ε p) (Sensitivity.e q) = if p = q then 1 else 0

theorem Sensitivity.epsilon_total {n : ℕ} {v : Sensitivity.V n} (h : ∀ (p : Sensitivity.Q n), ↑(Sensitivity.ε p) v = 0) : v = 0

Any vector in V n annihilated by all ε p's is zero.

theorem Sensitivity.dualBases_e_ε (n : ℕ) : Module.DualBases Sensitivity.e Sensitivity.ε

e and ε are dual families of vectors. It implies that e is indeed a basis and ε computes coefficients of decompositions of vectors on that basis.

We will now derive the dimension of V, first as a cardinal in dim_V and, since this cardinal is finite, as a natural number in finrank_V

theorem Sensitivity.dim_V {n : ℕ} : Module.rank ℝ (Sensitivity.V n) = 2 ^ ↑n

instance Sensitivity.instFiniteDimensionalRealVInstDivisionRingRealInstAddCommGroupVInstModuleRealVSemiringToAddCommMonoidInstAddCommGroupV {n : ℕ} : FiniteDimensional ℝ (Sensitivity.V n)

theorem Sensitivity.finrank_V {n : ℕ} : FiniteDimensional.finrank ℝ (Sensitivity.V n) = 2 ^ n

The linear map

noncomputable def Sensitivity.f (n : ℕ) : Sensitivity.V n →ₗ[ℝ] Sensitivity.V n

The linear operator $f_n$ corresponding to Huang's matrix $A_n$, defined inductively as a ℝ-linear map from V n to V n.

Equations

• Sensitivity.f 0 = 0
• Sensitivity.f (Nat.succ n) = LinearMap.prod (LinearMap.coprod (Sensitivity.f n) LinearMap.id) (LinearMap.coprod LinearMap.id (-Sensitivity.f n))

The preceding definition uses linear map constructions to automatically get that f is linear, but its values are somewhat buried as a side-effect. The next two lemmas unbury them.

@[simp]

theorem Sensitivity.f_zero : Sensitivity.f 0 = 0

theorem Sensitivity.f_succ_apply {n : ℕ} (v : Sensitivity.V (Nat.succ n)) : ↑(Sensitivity.f (Nat.succ n)) v = (↑(Sensitivity.f n) v.fst + v.snd, v.fst - ↑(Sensitivity.f n) v.snd)

In the next statement, the explicit conversion (n : ℝ) of n to a real number is necessary since otherwise n • v refers to the multiplication defined using only the addition of V.

theorem Sensitivity.f_squared {n : ℕ} (v : Sensitivity.V n) : ↑(Sensitivity.f n) (↑(Sensitivity.f n) v) = ↑n • v

We now compute the matrix of f in the e basis (p is the line index, q the column index).

theorem Sensitivity.f_matrix {n : ℕ} (p : Sensitivity.Q n) (q : Sensitivity.Q n) : |↑(Sensitivity.ε q) (↑(Sensitivity.f n) (Sensitivity.e p))| = if p ∈ Sensitivity.Q.adjacent q then 1 else 0

noncomputable def Sensitivity.g (m : ℕ) : Sensitivity.V m →ₗ[ℝ] Sensitivity.V (Nat.succ m)

The linear operator $g_m$ corresponding to Knuth's matrix $B_m$.

In the following lemmas, m will denote a natural number.

Again we unpack what are the values of g.

theorem Sensitivity.g_apply {m : ℕ} (v : Sensitivity.V m) : ↑(Sensitivity.g m) v = (↑(Sensitivity.f m) v + Real.sqrt (↑m + 1) • v, v)

theorem Sensitivity.g_injective {m : ℕ} : Function.Injective ↑(Sensitivity.g m)

theorem Sensitivity.f_image_g {m : ℕ} (w : Sensitivity.V (Nat.succ m)) (hv : ∃ v, ↑(Sensitivity.g m) v = w) : ↑(Sensitivity.f (Nat.succ m)) w = Real.sqrt (↑m + 1) • w

The main proof

In this section, in order to enforce that n is positive, we write it as m + 1 for some natural number m.

dim X will denote the dimension of a subspace X as a cardinal.

fdim X will denote the (finite) dimension of a subspace X as a natural number.

Span S will denote the ℝ-subspace spanned by S.

Card X will denote the cardinal of a subset of a finite type, as a natural number.

In the following, ⊓ and ⊔ will denote intersection and sums of ℝ-subspaces, equipped with their subspace structures. The notations come from the general theory of lattices, with inf and sup (also known as meet and join).

theorem Sensitivity.exists_eigenvalue {m : ℕ} (H : Set (Sensitivity.Q (Nat.succ m))) (hH : Finset.card (Set.toFinset H) ≥ 2 ^ m + 1) : ∃ y, y ∈ Submodule.span ℝ (Sensitivity.e '' H) ⊓ LinearMap.range (Sensitivity.g m) ∧ y ≠ 0

If a subset H of Q (m+1) has cardinal at least 2^m + 1 then the subspace of V (m+1) spanned by the corresponding basis vectors non-trivially intersects the range of g m.

theorem Sensitivity.huang_degree_theorem {m : ℕ} (H : Set (Sensitivity.Q (Nat.succ m))) (hH : Finset.card (Set.toFinset H) ≥ 2 ^ m + 1) : ∃ q, q ∈ H ∧ Real.sqrt (↑m + 1) ≤ ↑(Finset.card (Set.toFinset (H ∩ Sensitivity.Q.adjacent q)))

Huang sensitivity theorem also known as the Huang degree theorem