Lax Lean Archive

Asteroidal cycle triples obstruct induced minors

Lax762056.CycleObstruction · concepts/Lax762056/CycleObstruction.lean · lax-762056

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.

    Natural Language Statement

    Lemma

    No graph containing an asteroidal triple of cycles is an induced minor of a row and column graph. The 5×55\times5 grid contains such a triple.

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

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 asteroidalCycles_obstruction proven

    2 grid_five_has_asteroidalCycles proven

    In the paper

    • page 5 of this submission's paper
    • page 5 of this submission's paper

    Lean source view on GitHub

    1import Lax762056.AsteroidalCycles
    2import Lax762056.ColumnGraph
    3import Lax762056.Grid
    4
    5/-!
    6---
    7title: Asteroidal cycle triples obstruct induced minors
    8type: lemma
    9---
    10No graph containing an asteroidal triple of cycles is an induced minor of
    11a row and column graph. The 5×55\times5 grid contains such a triple.
    12-/
    13
    14namespace Lax762056.CycleObstruction
    15
    16open AsteroidalCycles ColumnGraph Grid InducedMinors
    17
    18axiom asteroidalCycles_obstruction (R W : Type*) (c : ℕ) (H : SimpleGraph W)
    19 (hH : HasAsteroidalCycleTriple H) :
    20 ¬ IsInducedMinor H (columnGraph R c)
    21
    22axiom grid_five_has_asteroidalCycles : HasAsteroidalCycleTriple (squareGrid 5)
    23
    24end Lax762056.CycleObstruction
    25
    Show ProofShow 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…