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 Michael 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.

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.

Equations

• Sensitivity.Q n = (Fin n → Bool)

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

Equations

• Sensitivity.instInhabitedQ n = inferInstanceAs (Inhabited (Fin n → Bool))

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

Equations

• Sensitivity.instFintypeQ n = inferInstanceAs (Fintype (Fin n → Bool))

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

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

Equations

• Sensitivity.π p = p ∘ Fin.succ

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

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

n will always denote a natural number.

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

Q 0 has a unique element.

Equations

• Sensitivity.Q.instUniqueOfNatNat = { default := fun (x : Fin 0) => true, uniq := Sensitivity.Q.instUniqueOfNatNat._proof_1 }

theorem Sensitivity.Q.card (n : ℕ) : Fintype.card (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 q : Q n.succ) : p = q ↔ p 0 = q 0 ∧ π p = π q

def Sensitivity.Q.adjacent {n : ℕ} (p : Q n) : Set (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.

Equations

• p.adjacent = {q : Sensitivity.Q n | ∃! i : Fin n, p i ≠ q i}

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

In Q 0, no two vertices are adjacent.

theorem Sensitivity.Q.adj_iff_proj_eq {n : ℕ} {p q : Q n.succ} (h₀ : p 0 ≠ q 0) : q ∈ p.adjacent ↔ π p = π 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 q : Q n.succ} (h₀ : p 0 = q 0) : q ∈ p.adjacent ↔ π q ∈ (π p).adjacent

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 q : Q n} : q ∈ p.adjacent ↔ p ∈ q.adjacent

The vector space

def Sensitivity.V : ℕ → Type

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

Equations

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

@[simp]

theorem Sensitivity.V_zero : V 0 = ℝ

@[simp]

theorem Sensitivity.V_succ {n : ℕ} : V (n + 1) = (V n × V n)

theorem Sensitivity.V.ext {n : ℕ} {p q : V n.succ} (h₁ : p.1 = q.1) (h₂ : p.2 = q.2) : p = q

theorem Sensitivity.V.ext_iff {n : ℕ} {p q : V n.succ} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2

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

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

Equations

• Sensitivity.V.instDecidableEq n = Nat.recAux (id inferInstance) (fun (n : ℕ) (a : DecidableEq (Sensitivity.V n)) => id inferInstance) n

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

Equations

• Sensitivity.V.instAddCommGroup n = Nat.recAux (id inferInstance) (fun (n : ℕ) (a : AddCommGroup (Sensitivity.V n)) => id inferInstance) n

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

Equations

• Sensitivity.V.instModuleReal n = Nat.recAux (id inferInstance) (fun (n : ℕ) (a : Module ℝ (Sensitivity.V n)) => id inferInstance) n

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

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

Equations

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

@[simp]

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

noncomputable def Sensitivity.ε {n : ℕ} : Q n → 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 q : Q n) : (ε p) (e q) = if p = q then 1 else 0

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

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

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

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 ℝ (V n) = 2 ^ n

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

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

The linear map

noncomputable def Sensitivity.f (n : ℕ) : V n →ₗ[ℝ] 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 n.succ = ((Sensitivity.f n).coprod LinearMap.id).prod (LinearMap.id.coprod (-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 : f 0 = 0

theorem Sensitivity.f_succ_apply {n : ℕ} (v : V n.succ) : (f n.succ) v = ((f n) v.1 + v.2, v.1 - (f n) v.2)

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 : V n) : (f n) ((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 q : Q n) : |(ε q) ((f n) (e p))| = if p ∈ q.adjacent then 1 else 0

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

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

Equations

• Sensitivity.g m = (Sensitivity.f m + √(↑m + 1) • LinearMap.id).prod LinearMap.id

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 : V m) : (g m) v = ((f m) v + √(↑m + 1) • v, v)

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

theorem Sensitivity.f_image_g {m : ℕ} (w : V m.succ) (hv : ∃ (v : V m), (g m) v = w) : (f m.succ) w = √(↑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 (Q m.succ)) (hH : H.toFinset.card ≥ 2 ^ m + 1) : ∃ y ∈ Submodule.span ℝ (e '' H) ⊓ LinearMap.range (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 (Q m.succ)) (hH : H.toFinset.card ≥ 2 ^ m + 1) : ∃ q ∈ H, √(↑m + 1) ≤ ↑(H ∩ q.adjacent).toFinset.card

Huang sensitivity theorem also known as the Huang degree theorem