Lax Lean Archive

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

Residual walk augmentation for real-capacity flows

Lax342547.ResidualFlows · concepts/Lax342547/ResidualFlows.lean · lax-342547

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 residual walk supplies a skew direction with the correct source and sink divergences. A sufficiently small positive real perturbation respects every capacity, so a maximum flow has no residual source-to-sink walk.

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

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

    1 edge_direction proven

    2 feasible_augmentation proven

    3 maximal_no_residual_path proven

    4 residual_walk_direction proven

    Lean source view on GitHub

    1import Lax342547.RealFlows
    2import Mathlib.Logic.Relation
    3
    4/-!
    5---
    6title: Residual walk augmentation for real-capacity flows
    7type: lemma
    8---
    9Every residual walk supplies a skew direction with the correct source and sink divergences. A sufficiently small positive real perturbation respects every capacity, so a maximum flow has no residual source-to-sink walk.
    10-/
    11
    12namespace Lax342547.ResidualFlows
    13
    14open Lax342547.RealFlows
    15open scoped BigOperators Topology
    16open Filter
    17
    18noncomputable def edgeDirection {V : Type} (u v : V) (a b : V) : ℝ := by
    19 classical
    20 exact (if a=u ∧ b=v then 1 else 0) - (if a=v ∧ b=u then 1 else 0)
    21
    22def Direction {V : Type} [Fintype V] (c f d : V → V → ℝ) (u v : V) : Prop := by
    23 classical
    24 exact (∀ a b, d a b = -d b a) ∧
    25 (∀ a, divergence d a = (if a=u then 1 else 0)-(if a=v then 1 else 0)) ∧
    26 (∀ a b, ¬ Residual c f a b → d a b ≤ 0)
    27
    28axiom edge_direction {V : Type} [Fintype V] (c f : V → V → ℝ) (u v : V)
    29 (huv : Residual c f u v) : Direction c f (edgeDirection u v) u v
    30
    31axiom residual_walk_direction {V : Type} [Fintype V] (c f : V → V → ℝ) (u v : V)
    32 (hpath : Relation.ReflTransGen (Residual c f) u v) :
    33 ∃ d, Direction c f d u v
    34
    35axiom feasible_augmentation {V : Type} [Fintype V]
    36 (c f d : V → V → ℝ) (s t : V) (hfeasible : Feasible c f s t)
    37 (hdir : Direction c f d s t) :
    38 ∃ δ : ℝ, 0 < δ ∧ Feasible c (fun a b => f a b+δ*d a b) s t
    39
    40axiom maximal_no_residual_path {V : Type} [Fintype V]
    41 (c f : V → V → ℝ) (s t : V) (hst : s ≠ t) (hf : Feasible c f s t)
    42 (hmax : ∀ g, Feasible c g s t → divergence g s ≤ divergence f s) :
    43 ¬ Relation.ReflTransGen (Residual c f) s t
    44
    45end Lax342547.ResidualFlows
    46
    Show ProofShow ProofShow ProofShow Proof
    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…