Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax56.VertexRemovalStability

Quantitative vertex-removal Erdős–Simonovits stability for K₆

concepts/Lax56/VertexRemovalStability.lean · lax-56

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimThis concept

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    For 0<ε<1/37500 < ε < 1/3750, a K6K₆-free graph on at least 20 vertices with more than ex(m,K6)−εm2ex(m,K₆) - εm² edges can be made 5-colourable by deleting fewer than 3500εm3500εm vertices. This is the explicit vertex-removal form used in the paper.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
    2import Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
    3import Mathlib.Combinatorics.SimpleGraph.Clique
    4import Mathlib.Data.Real.Basic
    5
    6/-!
    7---
    8title: Quantitative vertex-removal Erdős--Simonovits stability for K₆
    9type: theorem
    10---
    11For `0 < ε < 1/3750`, a `K₆`-free graph on at least 20 vertices with
    12more than `ex(m,K₆) - εm²` edges can be made 5-colourable by deleting
    13fewer than `3500εm` vertices. This is the explicit vertex-removal form used
    14in the paper.
    15-/
    16
    17namespace Lax56.VertexRemovalStability
    18
    19open SimpleGraph
    20
    21/-- The number of (unordered) edges of a finite simple graph. -/
    22noncomputable def edgeCount {V : Type*} [Finite V] (G : SimpleGraph V) : ℕ :=
    23 Nat.card G.edgeSet
    24
    25axiom exists_fiveColorable_delete
    26 {V : Type*} [Fintype V] (G : SimpleGraph V) (eps : ℝ)
    27 (hepsPos : 0 < eps) (hepsSmall : eps < 1 / 3750)
    28 (hcard : 20 ≤ Fintype.card V) (hK6 : G.CliqueFree 6)
    29 (hedges :
    30 (SimpleGraph.extremalNumber (Fintype.card V) (⊤ : SimpleGraph (Fin 6)) : ℝ) -
    31 eps * (Fintype.card V : ℝ) ^ 2 < edgeCount G) :
    32 ∃ Z : Set V,
    33 (Nat.card Z : ℝ) < 3500 * eps * Fintype.card V ∧
    34 (G.induce Zᶜ).Colorable 5
    35
    36end Lax56.VertexRemovalStability
    37
    Show Proof

    Builds on

    none

    Used by

    none

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…