Lax Lean Archive

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

Lax570090.VertexRemovalStability · concepts/Lax570090/VertexRemovalStability.lean · lax-570090

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.

    Natural Language Statement

    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.

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    Each proof establishes this claim relative to its assumptions.

    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 Lax570090.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 Lax570090.VertexRemovalStability
    37
    Show Proof
    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…