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

Lax54.KeyCombLemma

Stable hubbed comb in a critical graph

concepts/Lax54/KeyCombLemma.lean · lax-54

proven

Loading review…

Sign in with ORCID

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

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    Lemma 3.1 of the paper, with reciprocal integer parameters. Let K=220K=2^{20}. For every sufficiently large EE, every D>0D>0, and every lower bound QQ, there is an exponent qmax{3,Q}q\geq\max\{3,Q\} with the following property. If GG is qq-critical, V(G)DX|V(G)|\leq D|X|, and EdegG[X](x)<XE\deg_{G[X]}(x)<|X| for every xXx\in X, then GG contains a stable hubbed comb such that EKtE\leq Kt and EXKt2BiE|X|\leq Kt^2|B_i| for every block BiB_i.

    The absolute constant KK replaces the constant 400400 in the paper to accommodate the integral form of Theorem 2.1. Its value does not affect the Erdős–Hajnal conclusion.

    Lean source view on GitHub

    1import Lax54.GraphDefinitions
    2
    3/-!
    4---
    5title: Stable hubbed comb in a critical graph
    6type: theorem
    7---
    8Lemma 3.1 of the paper, with reciprocal integer parameters. Let
    9K=220K=2^{20}. For every sufficiently large EE, every D>0D>0, and every lower
    10bound QQ, there is an exponent qmax{3,Q}q\geq\max\{3,Q\} with the following
    11property. If GG is qq-critical, V(G)DX|V(G)|\leq D|X|, and
    12EdegG[X](x)<XE\deg_{G[X]}(x)<|X| for every xXx\in X, then GG contains a stable hubbed
    13comb such that EKtE\leq Kt and
    14EXKt2BiE|X|\leq Kt^2|B_i| for every block BiB_i.
    15
    16The absolute constant KK replaces the constant 400400 in the paper to
    17accommodate the integral form of Theorem 2.1. Its value does not affect the
    18Erdős–Hajnal conclusion.
    19-/
    20
    21namespace Lax54.KeyCombLemma
    22
    23open Lax54.GraphDefinitions
    24
    25universe u
    26
    27/-- The absolute constant in the integral form of the key comb lemma. -/
    28def keyCombConstant : ℕ := 2 ^ 20
    29
    30/-- A sufficient lower bound on the sparsity parameter for obtaining at least two teeth. -/
    31def keySparsityThreshold : ℕ := 2 * keyCombConstant
    32
    33/-- Lemma 3.1, with reciprocal integer parameters and cleared denominators. -/
    34axiom key_comb_lemma :
    35 ∀ E D Q : ℕ, keySparsityThreshold ≤ E → 0 < D →
    36 ∃ q : ℕ, 3 ≤ q ∧ Q ≤ q ∧
    37 ∀ {V : Type u} [Fintype V] [DecidableEq V]
    38 (G : SimpleGraph V) [DecidableRel G.Adj] (X : Finset V),
    39 IsQCritical q G →
    40 Fintype.card V ≤ D * X.card →
    41 (∀ x : {v : V // v ∈ X},
    42 E * (G.induce (X : Set V)).degree x < X.card) →
    43 ∃ (t : ℕ) (C : StableHubComb G t),
    44 E ≤ keyCombConstant * t ∧
    45 ∀ i : Fin t,
    46 E * X.card ≤ keyCombConstant * t ^ 2 * (C.block i).card
    47
    48end Lax54.KeyCombLemma
    49
    Show Proof

    Used by

    none

    From Mathlib

    none

    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…