Restricted set or uniform blockade in a house-free graph

Lax57.HouseDichotomy · concepts/Lax57/HouseDichotomy.lean · lax-57

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

    There is an integer a≥1a\geq 1 such that, for every E≥3E\geq 3, every finite house-free graph GG has one of two outcomes. Either an induced subgraph on XX is 1/E1/E-restricted and ∣G∣≤Ea∣X∣|G|\leq E^a|X|, or GG has a complete or anticomplete blockade of length kk, where 2≤k≤E2\leq k\leq E, whose blocks all have size at least ∣G∣/ka|G|/k^a.

    This is the denominator-cleared form of Lemma 7.3 of Nguyen, Scott, and Seymour. The structural argument is stated for the house, the complement of the five-vertex path.

    Concept map
    3 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 5 of this submission's paper
    • page 17 of this submission's paper

    Lean source view on GitHub

    1import Lax57.GraphDefinitions
    2
    3/-!
    4---
    5title: Restricted set or uniform blockade in a house-free graph
    6type: lemma
    7---
    8There is an integer a≥1a\geq 1 such that, for every E≥3E\geq 3, every finite
    9house-free graph GG has one of two outcomes. Either an induced subgraph on
    10XX is 1/E1/E-restricted and ∣G∣≤Ea∣X∣|G|\leq E^a|X|, or GG has a complete or
    11anticomplete blockade of length kk, where 2≤k≤E2\leq k\leq E, whose blocks all
    12have size at least ∣G∣/ka|G|/k^a.
    13
    14This is the denominator-cleared form of Lemma 7.3 of Nguyen, Scott, and
    15Seymour. The structural argument is stated for the house, the complement of
    16the five-vertex path.
    17-/
    18
    19namespace Lax57.HouseDichotomy
    20
    21open Lax57.GraphDefinitions
    22
    23universe u
    24
    25/-- The structural dichotomy for finite house-free graphs. -/
    26axiom house_dichotomy :
    27 ∃ a : ℕ, 1 ≤ a ∧
    28 ∀ E : ℕ, 3 ≤ E →
    29 ∀ {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    30 [DecidableRel G.Adj],
    31 IsHouseFree G →
    32 (∃ X : Finset V,
    33 Fintype.card V ≤ E ^ a * X.card ∧ ERestricted G E X) ∨
    34 HasUniformBlockade G E a
    35
    36end Lax57.HouseDichotomy
    37
    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…