Theorem 6

Reference: arxiv/2602.05192 First Proof by Mohammed Abouzaid, Andrew J. Blumberg, Martin Hairer, Joe Kileel, Tamara G. Kolda, Paul D. Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, Lauren Williams

def Arxiv.«2602.05192».IsEpsilonLight {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (ε : ℝ) (S : Finset V) : Prop

For a graph $G = (V, E)$, let $G_S = (V, E(S,S))$ denote the graph with the same vertex set, but only the edges between vertices in $S$. Let $L$ be the Laplacian matrix of $G$ and let $L_S$ be the Laplacian of $G_S$.

I say that a set of vertices $S$ is $\epsilon$-light if the matrix $\epsilon L - L_S$ is positive semidefinite.

Equations

• Arxiv.«2602.05192».IsEpsilonLight G ε S = (ε • SimpleGraph.lapMatrix ℝ G - SimpleGraph.lapMatrix ℝ (SimpleGraph.induce (↑S) G).spanningCoe).PosSemidef

theorem Arxiv.«2602.05192».epsilon_light_subset_exists : sorry ↔ ∃ c > 0, ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (ε : ℝ), 0 < ε → ε < 1 → ∃ (S : Finset (Fin n)), IsEpsilonLight G ε S ∧ ↑S.card ≥ c * ε * ↑n

Does there exist a constant $c > 0$ so that for every graph $G$ and every $\epsilon$ between $0$ and $1$, $V$ contains an $\epsilon$-light subset $S$ of size at least $c \epsilon |V|$?

Note: While no proof of this is published yet, the authors of arxiv/2602.05192 announced that a proof will be released on 2026-02-13.

TODO(firsching): update category and remove note when proof is published.