Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Discarding long almost-embedding routes

Lax263307.RoutePruning · concepts/Lax263307/RoutePruning.lean · lax-263307

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

    Theorem

    Discard each source edge whose host route uses more than LL vertices. The number of discarded edges times LL is at most the original total route size. The remaining graph retains an induced almost-embedding with every route using at most LL vertices. Edge deletion may create isolated source vertices; the transfer with singleton bags handles them separately.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 long_edge_count proven

    2 prune_routes proven

    Lean source view on GitHub

    1import Lax263307.AlmostEmbeddings
    2import Lax263307.EdgeDeletionWidth
    3
    4/-!
    5---
    6title: Discarding long almost-embedding routes
    7type: theorem
    8---
    9Discard each source edge whose host route uses more than LL vertices. The
    10number of discarded edges times LL is at most the original total route
    11size. The remaining graph retains an induced almost-embedding with every
    12route using at most LL vertices. Edge deletion may create isolated source
    13vertices; the transfer with singleton bags handles them separately.
    14
    15# Attribution
    16
    17Bonnet–Chang, the long-route deletion step in Lemma 11.
    18-/
    19
    20namespace Lax263307.RoutePruning
    21
    22open Lax263307.AlmostEmbeddings
    23
    24noncomputable def longEdges {t n : ℕ} {H : SimpleGraph (Fin t)} [DecidableRel H.Adj]
    25 {G : SimpleGraph (Fin n)} (E : AlmostEmbedding H G) (L : ℕ) : Finset (Sym2 (Fin t)) := by
    26 classical
    27 exact (Finset.univ.filter fun e : H.edgeSet => L < (E.route e).card).image Subtype.val
    28
    29axiom long_edge_count {t n : ℕ} (H : SimpleGraph (Fin t)) [DecidableRel H.Adj]
    30 (G : SimpleGraph (Fin n)) (E : AlmostEmbedding H G) (L : ℕ) :
    31 L * (longEdges E L).card ≤ ∑ e : H.edgeSet, (E.route e).card
    32
    33axiom prune_routes {t n : ℕ} (H : SimpleGraph (Fin t)) [DecidableRel H.Adj]
    34 (G : SimpleGraph (Fin n)) (E : AlmostEmbedding H G) (induced : IsInduced E) (L : ℕ) :
    35 ∃ E' : AlmostEmbedding (H.deleteEdges (↑(longEdges E L) : Set (Sym2 (Fin t)))) G,
    36 IsInduced E' ∧ (∀ e, (E'.route e).card ≤ L)
    37
    38end Lax263307.RoutePruning
    39
    Show ProofShow Proof

    Attribution

    Bonnet–Chang, the long-route deletion step in Lemma 11.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…