Lax Lean Archive

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

Lax57.PreparedHouseBlockade

Prepared sparse-or-complete house blockades

concepts/Lax57/PreparedHouseBlockade.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

    This is the denominator-cleared preparation carried out in Claim 7.1.1 of Nguyen, Scott, and Seymour. Starting from the semisparse blockade of Lemma 6.2, one samples equal-sized subblocks, removes high cross-degree vertices, and takes large anticonnected components. Failure to find such a component already gives the complete-blockade alternative.

    Lean source view on GitHub

    1import Lax57.GraphDefinitions
    2
    3/-!
    4---
    5title: Prepared sparse-or-complete house blockades
    6type: theorem
    7---
    8This is the denominator-cleared preparation carried out in Claim 7.1.1 of
    9Nguyen, Scott, and Seymour. Starting from the semisparse blockade of Lemma 6.2,
    10one samples equal-sized subblocks, removes high cross-degree vertices, and
    11takes large anticonnected components. Failure to find such a component
    12already gives the complete-blockade alternative.
    13-/
    14
    15namespace Lax57.PreparedHouseBlockade
    16
    17open Finset
    18open scoped SimpleGraph
    19open Lax57.GraphDefinitions
    20
    21universe u
    22
    23/-- A very long equal-width blockade whose noncomplete pairs are sparse in
    24both vertexwise directions, or the desired complete blockade already. -/
    25axiom prepared_house_blockade :
    26 ∃ d : ℕ, 40 ≤ d ∧
    27 ∀ Q : ℕ, 8 ≤ Q →
    28 ∀ {V : Type u} [Fintype V] [DecidableEq V]
    29 (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V),
    30 IsHouseFree G → Q ^ (30 * d ^ 3) ≤ S.card →
    31 ( (∃ C : Blockade (V := V) Q,
    32 C.IsInside S ∧ C.IsComplete G ∧
    33 ∀ i : Fin Q,
    34 S.card ≤ Q ^ (33 * d ^ 3) * (C.block i).card) ∨
    35 (∃ (m : ℕ) (B : Blockade (V := V) (Q ^ (4 * d))),
    36 0 < m ∧ B.IsInside S ∧
    37 (∀ i, m ≤ (B.block i).card ∧
    38 (B.block i).card ≤ 8 * Q ^ 2 * m) ∧
    39 (∀ i, (Gᶜ.induce (B.block i : Set V)).Connected) ∧
    40 (∀ {i j}, i ≠ j →
    41 ((∀ x ∈ B.block i, ∀ y ∈ B.block j, G.Adj x y) ∨
    42 (ESparseTo G (Q ^ (4 * d)) (B.block i) (B.block j) ∧
    43 ESparseTo G (Q ^ (4 * d)) (B.block j) (B.block i)))) ∧
    44 Q * (∑ i, (B.block i).card) ≤ S.card ∧
    45 S.card ≤ Q ^ (30 * d ^ 3) * m) )
    46
    47end Lax57.PreparedHouseBlockade
    48
    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…