Lax Lean Archive

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

Sparse bounded-load route distributions are impossible

Lax263307.NoBoundedLoadRoutes · concepts/Lax263307/NoBoundedLoadRoutes.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 a hereditary class has a uniform power bound on decomposition bags. There is a fixed positive integer KK such that a class member cannot support a uniform-endpoint route distribution with vertex loads at most ℓxv/k\ell x_v/k, costs in [0,1][0,1] of total mass at most kk, and edge cost at most k2/pk^2/p, when k≥K(ℓ+1)4a+2k\ge K(\ell+1)^{4a+2} and p≥2K(ℓ+1)4a+2p\ge2K(\ell+1)^{4a+2}.

    The registered source family supplies a graph large enough to contradict the sampled width upper bound, while its size overshoot keeps its edge count within the probability budgets.

    Concept map
    44 concepts; 8 descendants hidden
    100%
    TreewidthTreewidth transfer through analmost-embeddingConditioning graph routes on uniformendpointsBags meeting a connected vertex setTree-decomposition transfer throughconnected vertex representationsA width obstruction from sparse costs andbounded route loadsCoupled route sampling with shared verteximagesA good coupled sample with bounded totalroute sizeTreewidth loss under edge deletionEntropy and adjacency massFinite product sampling and coordinatemarginalsHereditary graph classesRestricting an induced almost-embedding toits route unionA class width bound obstructs induced routesamplingFew edges in the graph induced by shortroutesAlmost-embedding transfer with isolatedsource verticesSparse bounded-load route distributions areimpossibleCollision and length bounds forindependently sampled pathsInteger power bounds on class decompositionbagsGraph-route distributions from high-valuesplit flowsDiscarding long almost-embedding routesUniform endpoint normalization of finitepath flowsAn induced almost-embedding from a goodroute sampleChoosing a collision-free outcome withbounded total path lengthControlled-size subcubic source graphs oflinear treewidthProjecting split paths and preservingendpoint loadsVertex splitting for the directed flow–cutalgorithmPolynomial order bound from the sampledwidth inequalityConcurrent fractional flowExact flow–cut output certificatesProduct multicommodity networks andsparsest cutsDeterministic directed uniform flow–cutalgorithmRational flow instances and certificatesBinary encoding of finite wordsPolynomial-time computation by a wordRAMThe word RAMThe Constructor Meets the Requested OrderEdge Expansion and Subcubic GraphsThe Explicit Family Has Linear TreewidthSelecting and Encoding the ConstructedGraphsRotation Map of the Fixed Powered SeedDeterministic Search for a Fixed ExpanderSeedThe Explicit Graphs Are SubcubicExplicit Zig-Zag Family and PathReplacement
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax263307.CostSamplingObstruction
    2import Lax263307.PowerBagBounds
    3import Lax263307.SourceGraphs
    4import Lax263307.WidthGrowth
    5
    6/-!
    7---
    8title: Sparse bounded-load route distributions are impossible
    9type: theorem
    10---
    11Suppose a hereditary class has a uniform power bound on decomposition bags.
    12There is a fixed positive integer KK such that a class member cannot support
    13a uniform-endpoint route distribution with vertex loads at most
    14ℓxv/k\ell x_v/k, costs in [0,1][0,1] of total mass at most kk, and edge cost at
    15most k2/pk^2/p, when k≥K(ℓ+1)4a+2k\ge K(\ell+1)^{4a+2} and
    16p≥2K(ℓ+1)4a+2p\ge2K(\ell+1)^{4a+2}.
    17
    18The registered source family supplies a graph large enough to contradict
    19the sampled width upper bound, while its size overshoot keeps its edge count
    20within the probability budgets.
    21
    22# Formalization notes
    23
    24The power bag bound is an explicit hypothesis. Deriving it from strongly
    25edge-sublinear separators is a remaining part of the main proof. No source
    26graph construction is needed by the separator algorithm: this family is
    27used only in the contradiction that rules out its high-flow branch.
    28
    29# Attribution
    30
    31Bonnet–Chang, the sampled-path contradiction of Lemma 11, with the registered
    32subcubic source family from Lax920634.
    33-/
    34
    35namespace Lax263307.NoBoundedLoadRoutes
    36
    37open Lax263307.GraphClasses Lax263307.PowerBagBounds Lax228581.Treewidth
    38
    39axiom no_bounded_load_routes (C : GraphClass) (hereditary : IsHereditary C)
    40 (a A : ℕ) (a_positive : 0 < a) (A_positive : 0 < A) (class_bound : HasPowerBagBound C a A) :
    41 ∃ K : ℕ, 0 < K ∧ ∀ (n q : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
    42 G ∈ C n → ∀ (D : Lax263307.RouteDistributions.Distribution G q), 0 < n →
    43 ∀ (ℓ : ℕ), 0 < ℓ → ∀ (x : Fin n → ℝ) (k p : ℝ), 0 < k → 0 < p →
    44 (∀ v, 0 ≤ x v ∧ x v ≤ 1) → (∑ v, x v) ≤ k →
    45 (∀ v, Lax263307.PathSampling.load D.toSampling v ≤ (ℓ : ℝ) * x v / k) →
    46 Lax263307.Entropy.edgeCost G x ≤ k ^ 2 / p →
    47 (K : ℝ) * ((ℓ : ℝ) + 1) ^ (4 * a + 2) ≤ k →
    48 (2 * K : ℝ) * ((ℓ : ℝ) + 1) ^ (4 * a + 2) ≤ p → False
    49
    50end Lax263307.NoBoundedLoadRoutes
    51
    Show Proof
    Formalization notes

    The power bag bound is an explicit hypothesis. Deriving it from strongly edge-sublinear separators is a remaining part of the main proof. No source graph construction is needed by the separator algorithm: this family is used only in the contradiction that rules out its high-flow branch.

    Attribution

    Bonnet–Chang, the sampled-path contradiction of Lemma 11, with the registered subcubic source family from Lax920634.

    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…