Lax Lean Archive

Arc-to-path conversion for concurrent flows

Lax455465.ArcToPath · concepts/Lax455465/ArcToPath.lean · lax-455465

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

    Every feasible concurrent arc flow can be replaced by a finite simple-path flow of the same value. The conversion never increases the load on any directed arc, so it preserves both separate directed capacities and shared undirected capacities.

    Concept map
    3 concepts; 1 descendant hidden
    100%
    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 Lax455465.ConcurrentFlow
    2
    3/-!
    4---
    5title: Arc-to-path conversion for concurrent flows
    6type: lemma
    7---
    8Every feasible concurrent arc flow can be replaced by a finite simple-path
    9flow of the same value. The conversion never increases the load on any
    10directed arc, so it preserves both separate directed capacities and shared
    11undirected capacities.
    12
    13# Formalization notes
    14
    15Capacities, vertex weights, and flows may be arbitrary nonnegative reals.
    16Cycles and diagonal commodities can be discarded. No positivity, symmetry,
    17or rationality assumption is needed for this representation theorem.
    18-/
    19
    20open scoped NNReal
    21
    22namespace Lax455465.ArcToPath
    23open Lax455465.ProductNetwork Lax455465.ConcurrentFlow
    24
    25/-- Conservation and capacities in the arc formulation yield the public
    26simple-path formulation, with no increase in arc load. -/
    27axiom exists_path_flow {n : ℕ} (kind : EdgeKind) (N : Network n)
    28 (π : VertexWeight n) (f : ℝ≥0) (F : ArcFlow n)
    29 (hF : IsArcConcurrentFlow kind N π f F) :
    30 ∃ P : PathFlow n, IsConcurrentFlow kind N π f P ∧
    31 ∀ u v, arcLoad P u v ≤ totalArcLoad F u v
    32
    33end Lax455465.ArcToPath
    34
    Show Proof
    Formalization notes

    Capacities, vertex weights, and flows may be arbitrary nonnegative reals. Cycles and diagonal commodities can be discarded. No positivity, symmetry, or rationality assumption is needed for this representation theorem.

    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…