mathlib documentation

mathlib-archive / sensitivity

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 (, using the Lean theorem prover (, by Leonardo de Moura at Microsoft Research, and his collaborators (, and using Lean's user maintained mathematics library (

The project was developed at and is now archived at

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 #


@[protected, instance]
@[protected, instance]
def sensitivity.Q (n : ) :

The hypercube in dimension n.

Instances for sensitivity.Q

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


n will always denote a natural number.

@[protected, instance]

Q 0 has a unique element.

theorem sensitivity.Q.card (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 : sensitivity.Q (n + 1)) :

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.


In Q 0, no two vertices are adjacent.

theorem sensitivity.Q.adj_iff_proj_eq {n : } {p q : sensitivity.Q (n + 1)} (h₀ : p 0 q 0) :

If p and q in Q (n+1) 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 : sensitivity.Q (n + 1)} (h₀ : p 0 = q 0) :

If p and q in Q (n+1) 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 : sensitivity.Q n} :

The vector space #

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

Instances for sensitivity.V

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

@[protected, instance]
noncomputable def sensitivity.V.decidable_eq (n : ) :
@[protected, instance]

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

theorem sensitivity.duality {n : } (p q : sensitivity.Q n) :
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.

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.finrank_V {n : } :

The linear map #

The linear operator $f_n$ corresponding to Huang's matrix $A_n$, defined inductively as a ℝ-linear map from V n to V 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.

theorem sensitivity.f_succ_apply {n : } (v : sensitivity.V (n + 1)) :

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.

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

noncomputable def sensitivity.g (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 + (m + 1) v, v)
theorem sensitivity.f_image_g {m : } (w : sensitivity.V (m + 1)) (hv : (v : sensitivity.V m), (sensitivity.g m) v = w) :
(sensitivity.f (m + 1)) 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 (sensitivity.Q (m + 1))) (hH : H.to_finset.card 2 ^ m + 1) :

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 (m + 1))) (hH : H.to_finset.card 2 ^ m + 1) :
(q : sensitivity.Q (m + 1)), q H (m + 1) ((H q.adjacent).to_finset.card)

Huang sensitivity theorem also known as the Huang degree theorem