The Sensitivity Theorem

This file proves the main quantitative form of the sensitivity conjecture: for every Boolean function f of multilinear degree d ≥ 1, the sensitivity of f is bounded below by √d. The proof combines the parity imbalance lemma with the Huang hypercube lemma imported from Mathlib's Archive.Sensitivity.

Proof outline

1. Find a d-dimensional subcube on which the restriction of f has full degree d.
2. Reindex this subcube to Fin (m+1) → Bool and obtain a parity-sign imbalance: a class of more than 2^m vertices with the same parity sign.
3. Apply the Huang hypercube lemma to extract a vertex with at least √(m+1) same-class neighbours.
4. Each such neighbour is a bit-flip image flipBit q i along a distinct coordinate i, and at each such i the function f is sensitive.
5. Lift this lower bound on the local sensitivity of the restriction back to f itself.

theorem LeanPoolSensitivity.sensitivity_ge_sqrt_degree {n : ℕ} (f : BoolFun n) (hd : 1 ≤ f.degree) : √↑f.degree ≤ ↑f.sensitivity

Sensitivity Theorem (Huang 2019). For any Boolean function f of multilinear degree d ≥ 1, the sensitivity s(f) satisfies √d ≤ s(f).