Quantitative critical-comb consequence

Lax54.CriticalCombInput · concepts/Lax54/CriticalCombInput.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.

    Natural Language Statement

    Lemma

    This statement combines Lemmas 3.1 and 4.3 with the choice of parameters in the proof of Theorem 4.4. There are integers q≥3q\geq 3 and A≤2q−2A\leq 2^{q-2} such that every qq-critical induced-C5C_5-free graph GG contains, either in GG or in its complement, a stable hubbed comb with t≥2t\geq 2 teeth and ∣V(G)∣≤At2∣Bi∣|V(G)|\leq At^2|B_i| for every block BiB_i. The complementary alternative is required because Lemma 4.3 gives low maximum degree in either GG or its complement; both induced-C5C_5-freeness and qq-criticality are invariant under complementation.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 11 of this submission's paper

    Lean source view on GitHub

    1import Lax54.GraphDefinitions
    2
    3/-!
    4---
    5title: Quantitative critical-comb consequence
    6type: lemma
    7---
    8This statement combines Lemmas 3.1 and 4.3 with the choice of parameters in
    9the proof of Theorem 4.4. There are integers q≥3q\geq 3 and
    10A≤2q−2A\leq 2^{q-2} such that every qq-critical induced-C5C_5-free graph GG
    11contains, either in GG or in its complement, a stable hubbed comb with
    12t≥2t\geq 2 teeth and
    13∣V(G)∣≤At2∣Bi∣|V(G)|\leq At^2|B_i| for every block BiB_i. The complementary alternative
    14is required because Lemma 4.3 gives low maximum degree in either GG or its
    15complement; both induced-C5C_5-freeness and qq-criticality are invariant
    16under complementation.
    17-/
    18
    19open scoped SimpleGraph
    20
    21namespace Lax54.CriticalCombInput
    22
    23open Lax54.GraphDefinitions
    24
    25universe u
    26
    27/-- The quantitative critical-comb statement used in the proof of Theorem 4.4. -/
    28axiom exists_critical_comb_parameters :
    29 ∃ q A : ℕ, 3 ≤ q ∧ A ≤ 2 ^ (q - 2) ∧
    30 ∀ {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
    31 IsC5Free G → IsQCritical q G →
    32 (∃ (t : ℕ) (C : StableHubComb G t),
    33 2 ≤ t ∧
    34 ∀ i : Fin t, Fintype.card V ≤ A * t ^ 2 * (C.block i).card) ∨
    35 (∃ (t : ℕ) (C : StableHubComb Gᶜ t),
    36 2 ≤ t ∧
    37 ∀ i : Fin t, Fintype.card V ≤ A * t ^ 2 * (C.block i).card)
    38
    39end Lax54.CriticalCombInput
    40
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…