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:
n
will always denote a natural number.
Q 0
has a unique element.
Q n
has 2^n elements.
Until the end of this namespace, n
will be an implicit argument (still
a natural number).
In Q 0
, no two vertices are adjacent.
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.
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.
The vector space #
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)
Instances For
V n
is a real vector space whose equality relation is computable.
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))
Instances For
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
Instances For
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
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
.
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))
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.
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
.
The linear operator $g_m$ corresponding to Knuth's matrix $B_m$.
Instances For
In the following lemmas, m
will denote a natural number.
Again we unpack what are the values of g
.
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).
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
.
Huang sensitivity theorem also known as the Huang degree theorem