Lax Lean Archive

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

Projecting split paths and preserving endpoint loads

Lax263307.SplitPathProjection · concepts/Lax263307/SplitPathProjection.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 simple path of positive-capacity arcs in the split network, starting at u−u^- and ending at v+v^+, is the expansion of a simple original path from uu to vv. Each original vertex expands to its consecutive input/output ports. A reverse port arc would repeat an input port, so simplicity excludes it. Successive original vertices must therefore be graph neighbors.

    For a simple original route QQ, the expanded route traverses the capacity arc w−→w+w^-\to w^+ exactly once when ww belongs to QQ, and zero times otherwise. This counts both endpoints and includes singleton routes.

    Concept map
    10 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 capacity_arc_count proven

    2 project_simple_path proven

    3 split_support_projection proven

    Lean source view on GitHub

    1import Lax263307.VertexSplitting
    2import Mathlib.Data.List.Chain
    3
    4/-!
    5---
    6title: Projecting split paths and preserving endpoint loads
    7type: theorem
    8---
    9A simple path of positive-capacity arcs in the split network, starting at
    10u−u^- and ending at v+v^+, is the expansion of a simple original path from
    11uu to vv. Each original vertex expands to its consecutive input/output
    12ports. A reverse port arc would repeat an input port, so simplicity excludes
    13it. Successive original vertices must therefore be graph neighbors.
    14
    15For a simple original route QQ, the expanded route traverses the capacity
    16arc w−→w+w^-\to w^+ exactly once when ww belongs to QQ, and zero times
    17otherwise. This counts both endpoints and includes singleton routes.
    18
    19# Attribution
    20
    21Bonnet–Chang, flow projection and endpoint-inclusive load accounting in
    22Lemma 7.
    23-/
    24
    25namespace Lax263307.SplitPathProjection
    26
    27open scoped NNReal NNRat
    28open VertexSplitting Lax455465.ProductNetwork Lax455465.ConcurrentFlow
    29
    30/-- Replace each original route vertex by its consecutive two split ports. -/
    31def expandRoute {n : ℕ} (Q : List (Fin n)) : List (Fin (2 * n)) :=
    32 Q.flatMap fun v => [minus v, plus v]
    33
    34/-- A positive simple split path projects to a simple original route. -/
    35axiom project_simple_path {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    36 (x : Fin n → ℚ≥0) (large : ℚ≥0) (P : List (Fin (2 * n))) (u v : Fin n)
    37 (simple : P.Nodup)
    38 (chain : P.IsChain (fun a b => 0 < (splitInstance G x large).capacity a b))
    39 (start : P.head? = some (minus u)) (finish : P.getLast? = some (plus v)) :
    40 ∃ Q : List (Fin n), P = expandRoute Q ∧ Q.Nodup ∧ Q.IsChain G.Adj ∧
    41 Q.head? = some u ∧ Q.getLast? = some v
    42
    43/-- Capacity-arc occurrence equals the original vertex-membership indicator. -/
    44axiom capacity_arc_count {n : ℕ} (Q : List (Fin n)) (simple : Q.Nodup) (v : Fin n) :
    45 ((expandRoute Q).zip (expandRoute Q).tail).count (minus v, plus v) =
    46 if v ∈ Q then 1 else 0
    47
    48/-- Every retained positive path in a feasible split flow has such a projection. -/
    49axiom split_support_projection {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    50 (x : Fin n → ℚ≥0) (large : ℚ≥0) (f : ℝ≥0) (F : PathFlow (2 * n))
    51 (feasible : IsConcurrentFlow .directed (splitInstance G x large).network
    52 (splitInstance G x large).weights f F)
    53 (P : List (Fin (2 * n))) (member : P ∈ F.support) (u v : Fin n)
    54 (start : P.head? = some (minus u)) (finish : P.getLast? = some (plus v)) :
    55 ∃ Q : List (Fin n), P = expandRoute Q ∧ Q.Nodup ∧ Q.IsChain G.Adj ∧
    56 Q.head? = some u ∧ Q.getLast? = some v
    57
    58end Lax263307.SplitPathProjection
    59
    Show ProofShow ProofShow Proof

    Attribution

    Bonnet–Chang, flow projection and endpoint-inclusive load accounting in Lemma 7.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…