Bridge to Mathlib's Huang Theorem #
Repackages Mathlib's Sensitivity.huang_degree_theorem (the Huang hypercube
lemma) in a form that uses Finset (Fin (m+1) → Bool) and the flipBit
predicate from LeanPool.Sensitivity.Defs, ready to feed into the
sensitivity-conjecture argument.
The Mathlib formalisation in Archive.Sensitivity originated in the
lean-sensitivity
project, a community formalisation of Huang's proof carried out shortly after
the original paper appeared in 2019.
theorem
LeanPoolSensitivity.huang_finset
{m : ℕ}
(H : Finset (Fin (m + 1) → Bool))
(hH : 2 ^ m + 1 ≤ H.card)
:
A finset-flavoured restatement of Mathlib's
Sensitivity.huang_degree_theorem: any subset H of the hypercube of size
at least 2^m + 1 contains a vertex q with at least √(m+1) neighbours
in H, where neighbours are bit-flip images flipBit q i.