Lax Lean Archive

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

A class width bound obstructs induced route sampling

Lax263307.InducedEmbeddingWidth · concepts/Lax263307/InducedEmbeddingWidth.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

    Suppose every graph in a hereditary class has a decomposition whose bag size is bounded by a monotone function WW of its edge count. An induced almost-embedding of a source graph of maximum degree dd, with routes of size at most LL, transfers this to source bags of size at most max⁡{1,2dW(d∣E(H)∣L2)}\max\{1,2dW(d|E(H)|L^2)\}.

    Discarding long routes adds at most their number to this bound on treewidth plus one. A good sample with total size at most 4M4M therefore gives a number qq of discarded edges with Lq≤4MLq\le4M and the resulting source width bound. This is the quantitative obstruction used with a source family of linear treewidth.

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

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

    1 sampled_width_bound proven

    2 transfer_class_bound proven

    3 treewidth_after_pruning proven

    Lean source view on GitHub

    1import Lax263307.HostRestriction
    2import Lax263307.IsolatedEmbeddingTransfer
    3import Lax263307.GraphClasses
    4import Lax263307.RoutePruning
    5import Lax263307.SampledAlmostEmbeddings
    6
    7/-!
    8---
    9title: A class width bound obstructs induced route sampling
    10type: theorem
    11---
    12Suppose every graph in a hereditary class has a decomposition whose bag
    13size is bounded by a monotone function WW of its edge count. An induced
    14almost-embedding of a source graph of maximum degree dd, with routes of
    15size at most LL, transfers this to source bags of size at most
    16max⁡{1,2dW(d∣E(H)∣L2)}\max\{1,2dW(d|E(H)|L^2)\}.
    17
    18Discarding long routes adds at most their number to this bound on treewidth
    19plus one. A good sample with total size at most 4M4M therefore gives a
    20number qq of discarded edges with Lq≤4MLq\le4M and the resulting source
    21width bound. This is the quantitative obstruction used with a source
    22family of linear treewidth.
    23
    24# Formalization notes
    25
    26The monotone class bag bound is an explicit hypothesis here. Its derivation
    27from the main theorem's separator hypothesis is a separate proof obligation.
    28
    29# Attribution
    30
    31Bonnet–Chang, the width contradiction after route sampling in Lemma 11.
    32-/
    33
    34namespace Lax263307.InducedEmbeddingWidth
    35
    36open Lax263307.AlmostEmbeddings Lax263307.InducedRouteEdges Lax228581.Treewidth
    37open Lax263307.GraphClasses
    38
    39def HasBagBound (C : GraphClass) (W : ℕ → ℕ) : Prop :=
    40 ∀ n (G : SimpleGraph (Fin n)), G ∈ C n →
    41 ∃ D : TreeDecomposition G, ∀ i, (D.bag i).card ≤ W G.edgeSet.ncard
    42
    43axiom transfer_class_bound {t n : ℕ} (C : GraphClass) (hereditary : IsHereditary C)
    44 (W : ℕ → ℕ) (monotone : Monotone W) (class_bound : HasBagBound C W)
    45 (H : SimpleGraph (Fin t)) [DecidableRel H.Adj] (G : SimpleGraph (Fin n))
    46 (member : G ∈ C n) (E : AlmostEmbedding H G) (induced : IsInduced E) (d L : ℕ)
    47 (degree_bound : ∀ v, H.degree v ≤ d) (length_bound : ∀ e, (E.route e).card ≤ L) :
    48 ∃ D : TreeDecomposition H, ∀ i, (D.bag i).card ≤
    49 max 1 (2 * d * W (d * H.edgeSet.ncard * L ^ 2))
    50
    51axiom treewidth_after_pruning {t n : ℕ} (C : GraphClass) (hereditary : IsHereditary C)
    52 (W : ℕ → ℕ) (monotone : Monotone W) (class_bound : HasBagBound C W)
    53 (H : SimpleGraph (Fin t)) [DecidableRel H.Adj] (G : SimpleGraph (Fin n))
    54 (member : G ∈ C n) (E : AlmostEmbedding H G) (induced : IsInduced E) (d L : ℕ)
    55 (degree_bound : ∀ v, H.degree v ≤ d) :
    56 treewidth H + 1 ≤ max 1 (2 * d * W (d * H.edgeSet.ncard * L ^ 2)) +
    57 (Lax263307.RoutePruning.longEdges E L).card
    58
    59axiom sampled_width_bound {t n q : ℕ} (C : GraphClass) (hereditary : IsHereditary C)
    60 (W : ℕ → ℕ) (monotone : Monotone W) (class_bound : HasBagBound C W)
    61 (H : SimpleGraph (Fin t)) [DecidableRel H.Adj] (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    62 (member : G ∈ C n) (D : Lax263307.RouteDistributions.Distribution G q) (hn : 0 < n)
    63 (d L : ℕ) (degree_bound : ∀ v, H.degree v ≤ d) (M : ℝ) (positive : 0 < M)
    64 (bad_budget : (H.edgeSet.ncard : ℝ) ^ 2 * (Lax263307.PathSampling.collisionProbability D.toSampling +
    65 Lax263307.PathSampling.adjacencyProbability G D.toSampling) ≤ 1 / 4)
    66 (length_budget : (H.edgeSet.ncard : ℝ) * Lax263307.PathSampling.expectedSize D.toSampling ≤ M) :
    67 ∃ removed : ℕ, (L : ℝ) * removed ≤ 4 * M ∧
    68 treewidth H + 1 ≤ max 1 (2 * d * W (d * H.edgeSet.ncard * L ^ 2)) + removed
    69
    70end Lax263307.InducedEmbeddingWidth
    71
    Show ProofShow ProofShow Proof
    Formalization notes

    The monotone class bag bound is an explicit hypothesis here. Its derivation from the main theorem's separator hypothesis is a separate proof obligation.

    Attribution

    Bonnet–Chang, the width contradiction after route sampling 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…