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 #


The hypercube in dimension n.

Instances For

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

    Instances For
      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.

      Q n has 2^n elements.

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

      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.

      Instances For

        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.

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

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

          noncomputable def Sensitivity.e {n : } :

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

          Instances For
            noncomputable def Sensitivity.ε {n : } :

            The dual basis to e, defined inductively.

            • One or more equations did not get rendered due to their size.
            • Sensitivity.ε x_2 =
            Instances For
              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

              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.

              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.

                theorem Sensitivity.f_succ_apply {n : } (v : Sensitivity.V (Nat.succ n)) :
                (Sensitivity.f (Nat.succ n)) v = ((Sensitivity.f n) v.1 + v.2, v.1 - (Sensitivity.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.

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

                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.

                  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.f_image_g {m : } (w : Sensitivity.V (Nat.succ m)) (hv : ∃ (v : Sensitivity.V m), (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 : (Set.toFinset H).card 2 ^ m + 1) :
                  ∃ 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 : (Set.toFinset H).card 2 ^ m + 1) :
                  ∃ q ∈ H, Real.sqrt (m + 1) (Set.toFinset (H Sensitivity.Q.adjacent q)).card

                  Huang sensitivity theorem also known as the Huang degree theorem