First Proof, Theorem 6

Reference: arxiv/2602.05192v2 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 : True ↔ ∃ 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|$?