hypercube_induced_subgraph_degree
Provedcombinatoricsgraph-theorysensitivity-conjecture
Theorem 1.1 from Huang (2019): Every (2^{n-1}+1)-vertex induced subgraph of the n-dimensional hypercube graph Q_n has maximum degree at least sqrt(n). This is the main combinatorial result that implies the Sensitivity Conjecture.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem hypercube_induced_subgraph_degree (n : ℕ) (hn : 1 ≤ n) (S : Finset (Fin n → Bool)) (hS : S.card ≥ 2 ^ (n - 1) + 1) : ∃ v ∈ S, n ≤ (Finset.filter (fun w => (Finset.filter (fun i : Fin n => v i ≠ w i) Finset.univ).card = 1) S).card ^ 2 := by sorry
Source