Lax Lean Archive

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

Lax54.GraphDefinitions

Finite graph notions for the five-cycle Erdős–Hajnal theorem

concepts/Lax54/GraphDefinitions.lean · lax-54

definition

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 claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    This module defines the graph-theoretic notions used in the formalization. The graph C5C_5 is the cycle on five vertices, and induced-C5C_5-freeness is expressed using mathlib's induced-containment relation. For a finite graph GG, the homogeneous number is h(G)=max⁡{α(G),ω(G)}h(G)=\max\{\alpha(G),\omega(G)\} and κ(G)=α(G)ω(G)\kappa(G)=\alpha(G)\omega(G). The module also defines qq-critical graphs, the stable hubbed comb of Lemma 3.1, and the sparse-side and low-degree-side conclusions used in Rödl's theorem and Lemma 4.3.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Circulant
    2import Mathlib.Combinatorics.SimpleGraph.Clique
    3import Mathlib.Combinatorics.SimpleGraph.Copy
    4
    5/-!
    6---
    7title: Finite graph notions for the five-cycle Erdős–Hajnal theorem
    8type: definition
    9---
    10This module defines the graph-theoretic notions used in the formalization.
    11The graph C5C_5 is the cycle on five vertices, and induced-C5C_5-freeness is
    12expressed using mathlib's induced-containment relation. For a finite graph
    13GG, the homogeneous number is
    14h(G)=max⁡{α(G),ω(G)}h(G)=\max\{\alpha(G),\omega(G)\} and
    15κ(G)=α(G)ω(G)\kappa(G)=\alpha(G)\omega(G). The module also defines qq-critical graphs,
    16the stable hubbed comb of Lemma 3.1, and the sparse-side and low-degree-side
    17conclusions used in Rödl's theorem and Lemma 4.3.
    18-/
    19
    20open Finset
    21open scoped SimpleGraph
    22
    23namespace Lax54.GraphDefinitions
    24
    25universe u
    26
    27/-- The five-cycle. -/
    28abbrev C5 : SimpleGraph (Fin 5) := SimpleGraph.cycleGraph 5
    29
    30/-- A graph has no induced copy of the five-cycle. -/
    31def IsC5Free {V : Type u} (G : SimpleGraph V) : Prop :=
    32 ¬ C5 ⊴ G
    33
    34/-- The largest cardinality of a clique or stable set in a finite graph. -/
    35noncomputable def homogeneousNumber {V : Type u} (G : SimpleGraph V) : ℕ :=
    36 max G.cliqueNum G.indepNum
    37
    38/-- The product `ω(G) · α(G)` used in the critical-graph argument. -/
    39noncomputable def kappa {V : Type u} (G : SimpleGraph V) : ℕ :=
    40 G.cliqueNum * G.indepNum
    41
    42/--
    43A graph is `q`-critical if `kappa G ^ q < |V(G)|`, while every proper
    44vertex-induced subgraph `G[S]` satisfies `|S| ≤ kappa (G[S]) ^ q`.
    45-/
    46def IsQCritical {V : Type u} [Fintype V] (q : ℕ) (G : SimpleGraph V) : Prop :=
    47 kappa G ^ q < Fintype.card V ∧
    48 ∀ S : Finset V, S.card < Fintype.card V →
    49 S.card ≤ kappa (G.induce (S : Set V)) ^ q
    50
    51/--
    52A comb whose teeth form a stable set, together with the hub vertex from
    53Lemma 3.1. The hub is adjacent to every tooth and nonadjacent to every block.
    54The tooth `a_i` is adjacent to its block `B_i` and nonadjacent to every other
    55block.
    56-/
    57structure StableHubComb {V : Type u} [DecidableEq V]
    58 (G : SimpleGraph V) (t : ℕ) where
    59 tooth : Fin t → V
    60 block : Fin t → Finset V
    61 hub : V
    62 tooth_injective : Function.Injective tooth
    63 blocks_disjoint : ∀ {i j : Fin t}, i ≠ j → Disjoint (block i) (block j)
    64 tooth_not_mem : ∀ i j : Fin t, tooth i ∉ block j
    65 hub_not_mem : ∀ i : Fin t, hub ∉ block i
    66 tooth_adj_block : ∀ i : Fin t, ∀ x ∈ block i, G.Adj (tooth i) x
    67 tooth_nonadj_other : ∀ {i j : Fin t}, i ≠ j →
    68 ∀ x ∈ block j, ¬ G.Adj (tooth i) x
    69 teeth_stable : ∀ {i j : Fin t}, i ≠ j → ¬ G.Adj (tooth i) (tooth j)
    70 hub_adj_tooth : ∀ i : Fin t, G.Adj hub (tooth i)
    71 hub_nonadj_block : ∀ i : Fin t, ∀ x ∈ block i, ¬ G.Adj hub x
    72
    73/-- The vertices of `G` all have degree at most `d`. -/
    74def MaximumDegreeAtMost {V : Type u} [Fintype V] [DecidableEq V]
    75 (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) : Prop :=
    76 ∀ v : V, G.degree v ≤ d
    77
    78/--
    79The low-density alternative in Rödl's theorem. Either the graph or its
    80complement has edge density at most `1/E`; the definition clears the
    81denominator.
    82-/
    83def HasSparseSide {V : Type u} [Fintype V] [DecidableEq V]
    84 (G : SimpleGraph V) [DecidableRel G.Adj] (E : ℕ) : Prop :=
    85 E * 2 * G.edgeFinset.card ≤ Fintype.card V * (Fintype.card V - 1) ∨
    86 E * 2 * Gᶜ.edgeFinset.card ≤ Fintype.card V * (Fintype.card V - 1)
    87
    88/--
    89The maximum-degree version of the sparse-side conclusion. The witness `X`
    90satisfies `|V(G)| ≤ D|X|`; in either `G[X]` or its complement, every degree
    91`d(x)` satisfies `E d(x) < |X|`.
    92-/
    93def HasLowDegreeSide {V : Type u} [Fintype V] [DecidableEq V]
    94 (G : SimpleGraph V) [DecidableRel G.Adj] (E D : ℕ) : Prop :=
    95 ∃ X : Finset V,
    96 Fintype.card V ≤ D * X.card ∧
    97 ((∀ x : {v : V // v ∈ X},
    98 E * (G.induce (X : Set V)).degree x < X.card) ∨
    99 (∀ x : {v : V // v ∈ X},
    100 E * (Gᶜ.induce (X : Set V)).degree x < X.card))
    101
    102end Lax54.GraphDefinitions
    103

    Builds on

    none

    Used by

    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…