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

Lax54.CriticalCombInput

Quantitative critical-comb consequence

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    This statement combines Lemmas 3.1 and 4.3 with the choice of parameters in the proof of Theorem 4.4. There are integers q3q\geq 3 and A2q2A\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 t2t\geq 2 teeth and V(G)At2Bi|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.

    Lean source view on GitHub

    1import Lax54.GraphDefinitions
    2
    3/-!
    4---
    5title: Quantitative critical-comb consequence
    6type: theorem
    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 q3q\geq 3 and
    10A2q2A\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
    12t2t\geq 2 teeth and
    13V(G)At2Bi|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

    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…