Lax Lean Archive

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

Lax57.HouseDichotomy

Restricted set or uniform blockade in a house-free graph

concepts/Lax57/HouseDichotomy.lean · lax-57

proven

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

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    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.

    Lean source view on GitHub

    1import Lax57.GraphDefinitions
    2
    3/-!
    4---
    5title: Restricted set or uniform blockade in a house-free graph
    6type: theorem
    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

    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…