Bridge to Mathlib's Huang Theorem

Repackages the module port of 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 local module port in LeanPool.Sensitivity.Huang comes from Mathlib’s Archive.Sensitivity, which 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) : ∃ q ∈ H, √(↑m + 1) ≤ ↑{p ∈ H | ∃ (i : Fin (m + 1)), p = flipBit q i}.card

A finset-flavoured restatement of Mathlib's LeanPoolSensitivity.Huang.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.