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

The hypercube in dimension n.

Equations
Instances For
Equations
instance Sensitivity.instFintypeQ (n : ) :
Equations
def Sensitivity.π {n : } :

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

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

n will always denote a natural number.

Q 0 has a unique element.

Equations
theorem Sensitivity.Q.card (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 : ) :
p = q p 0 = q 0
def Sensitivity.Q.adjacent {n : } (p : ) :
Set ()

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
• = {q : | ∃! (i : Fin n), p i q i}
Instances For
theorem Sensitivity.Q.not_adjacent_zero (p : ) (q : ) :

In Q 0, no two vertices are adjacent.

theorem Sensitivity.Q.adj_iff_proj_eq {n : } {p : } {q : } (h₀ : p 0 q 0) :

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 : } (h₀ : p 0 = q 0) :

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 : } :

The vector space #

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

Equations
• = ()
Instances For
theorem Sensitivity.V.ext {n : } {p : } {q : } (h₁ : p.1 = q.1) (h₂ : p.2 = q.2) :
p = q

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

Equations
• = Nat.rec (id inferInstance) (fun (n : ) (n_ih : ) => id inferInstance) n
Equations
• = Nat.rec (id inferInstance) (fun (n : ) (n_ih : ) => id inferInstance) n
Equations
• = Nat.rec (id inferInstance) (fun (n : ) (n_ih : ) => id inferInstance) n
noncomputable def Sensitivity.e {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 (, 0) else (0, )
Instances For
@[simp]
theorem Sensitivity.e_zero_apply (x : ) :
noncomputable def Sensitivity.ε {n : } :

The dual basis to e, defined inductively.

Equations
• One or more equations did not get rendered due to their size.
• = LinearMap.id
Instances For
theorem Sensitivity.duality {n : } (p : ) (q : ) :
() () = if p = q then 1 else 0
theorem Sensitivity.epsilon_total {n : } {v : } (h : ∀ (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 : } :
= 2 ^ n
Equations
• (_ : ) = (_ : )

The linear map #

noncomputable def Sensitivity.f (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
Instances For

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_succ_apply {n : } (v : ) :
() v = (() v.1 + v.2, v.1 - () 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 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 : ) :
|() (() ())| = if then 1 else 0
noncomputable def Sensitivity.g (m : ) :

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

Equations
Instances For

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 = (() v + Real.sqrt (m + 1) v, v)
theorem Sensitivity.f_image_g {m : } (w : ) (hv : ∃ (v : ), () v = w) :
() 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 ()) (hH : ().card 2 ^ m + 1) :
∃ y ∈ Submodule.span (Sensitivity.e '' H) , 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 ()) (hH : ().card 2 ^ m + 1) :
∃ q ∈ H, Real.sqrt (m + 1) ().card

Huang sensitivity theorem also known as the Huang degree theorem