Lax Lean Archive

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

Graph-route distributions from high-value split flows

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

    A feasible directed split flow of value at least 1/γ1/\gamma yields a finite distribution of simple original graph routes with uniform ordered endpoints. The probability that a route uses vertex vv is at most γxv/n2\gamma x_v/n^2. Both endpoints count toward this load; equal original endpoints are allowed and their route is a singleton.

    Concept map
    14 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 finite_routes proven

    2 split_arc_distribution proven

    Lean source view on GitHub

    1import Lax263307.RoutingNormalization
    2import Lax263307.SplitPathProjection
    3
    4/-!
    5---
    6title: Graph-route distributions from high-value split flows
    7type: theorem
    8---
    9A feasible directed split flow of value at least 1/γ1/\gamma yields a finite
    10distribution of simple original graph routes with uniform ordered endpoints.
    11The probability that a route uses vertex vv is at most
    12γxv/n2\gamma x_v/n^2. Both endpoints count toward this load; equal original
    13endpoints are allowed and their route is a singleton.
    14
    15# Formalization notes
    16
    17Routes carrying positive probability are simple graph paths. Zero-probability
    18outcomes may have empty routes. Arc-to-path conversion is used only for the
    19existence argument, so this statement imposes no algorithm for constructing
    20the distribution. The underlying solver still returns an arc-flow certificate.
    21
    22# Attribution
    23
    24Bonnet–Chang, flow normalization and endpoint-inclusive loads in Lemma 7.
    25-/
    26
    27namespace Lax263307.RouteDistributions
    28
    29open scoped NNReal NNRat
    30open Lax263307.RoutingNormalization Lax263307.VertexSplitting
    31open Lax455465.ConcurrentFlow
    32
    33structure Distribution {n : ℕ} (G : SimpleGraph (Fin n)) (q : ℕ) where
    34 probability : Fin q → ℝ
    35 nonnegative : ∀ i, 0 ≤ probability i
    36 normalized : (∑ i, probability i) = 1
    37 route : Fin q → List (Fin n)
    38 valid : ∀ i, 0 < probability i → (route i).Nodup ∧ (route i).IsChain G.Adj ∧ route i ≠ []
    39 uniform : ∀ u v, (∑ i, if (route i).head? = some u ∧ (route i).getLast? = some v then
    40 probability i else 0) = 1 / (n : ℝ) ^ 2
    41
    42noncomputable def Distribution.toSampling {n q : ℕ} {G : SimpleGraph (Fin n)}
    43 (D : Distribution G q) : Lax263307.PathSampling.Distribution n q where
    44 probability := D.probability
    45 nonnegative := D.nonnegative
    46 normalized := D.normalized
    47 vertices i := (D.route i).toFinset
    48
    49/-- Normalize finite graph routes commodity by commodity. -/
    50axiom finite_routes {n q : ℕ} (G : SimpleGraph (Fin n)) (hn : 0 < n)
    51 (w : Fin q → ℝ) (E : Fin n → Fin n → Fin q → Prop)
    52 (w_nonnegative : ∀ i, 0 ≤ w i) (γ : ℝ) (γ_positive : 0 < γ)
    53 (lower : ∀ u v, 1 / γ ≤ routed w E u v)
    54 (Q : Fin q → List (Fin n))
    55 (routes : ∀ u v i, E u v i → (Q i).Nodup ∧ (Q i).IsChain G.Adj ∧
    56 (Q i).head? = some u ∧ (Q i).getLast? = some v) :
    57 ∃ D : Distribution G (n * (n * q)), ∀ z,
    58 Lax263307.PathSampling.load D.toSampling z ≤ γ / (n : ℝ) ^ 2 *
    59 (∑ i, w i * (if z ∈ Q i then (1 : ℝ) else 0))
    60
    61/-- A high-value split arc-flow certificate yields a bounded-load route distribution. -/
    62axiom split_arc_distribution {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    63 (hn : 0 < n) (x : Fin n → ℚ≥0) (large : ℚ≥0) (γ : ℝ) (γ_positive : 0 < γ)
    64 (f : ℝ≥0) (high : 1 / γ ≤ (f : ℝ)) (F : ArcFlow (2 * n))
    65 (feasible : IsArcConcurrentFlow .directed (splitInstance G x large).network
    66 (splitInstance G x large).weights f F) :
    67 ∃ q, ∃ D : Distribution G q, ∀ z,
    68 Lax263307.PathSampling.load D.toSampling z ≤ γ * (x z : ℝ) / (n : ℝ) ^ 2
    69
    70end Lax263307.RouteDistributions
    71
    Show ProofShow Proof
    Formalization notes

    Routes carrying positive probability are simple graph paths. Zero-probability outcomes may have empty routes. Arc-to-path conversion is used only for the existence argument, so this statement imposes no algorithm for constructing the distribution. The underlying solver still returns an arc-flow certificate.

    Attribution

    Bonnet–Chang, flow normalization and endpoint-inclusive loads in Lemma 7.

    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…