FormalConjectures/Arxiv/2602.05192/FirstProof6.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

2 declarations, 1 contain sorry, 0 declared as axioms

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

Imports (1)
  1. def Arxiv.«2602.05192».IsEpsilonLight 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$ line 46 source

    Source documentation

    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.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, Real, Finset

    Proof uses: Matrix.PosSemidef, HSub.hSub, Matrix, HSMul.hSMul, SimpleGraph.lapMatrix, Classical.propDecidable, SimpleGraph.Adj, SimpleGraph.spanningCoe, SimpleGraph.induce, Subtype, Membership.mem, Set, Function.Embedding, Function.Embedding.subtype, Exists, And, Eq

    22 instances, coercions and auxiliary constants left out.

    def IsEpsilonLight (G : SimpleGraph V) (ε : ℝ) (S : Finset V) : Prop :=
…
  2. theorem Arxiv.«2602.05192».epsilon_light_subset_exists sorry line 60 source

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Nat, SimpleGraph, Fin, LT.lt, Finset, Arxiv.«2602.05192».IsEpsilonLight, GE.ge, Finset.card, HMul.hMul

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.