Lax Lean Archive

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

Real max-flow min-cut from residual reachability

Lax342547.FlowCuts · concepts/Lax342547/FlowCuts.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

    Internal skew flow cancels, conservation identifies cut divergence with source value, and the reachable residual cut is saturated. Its real capacity equals the maximum flow value, and every cut bounds every feasible flow.

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

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

    1 conserving_cut_value proven

    2 cut_indicator proven

    3 cut_upper_bound proven

    4 divergence_cut_sum proven

    5 internal_skew_sum proven

    6 real_max_flow_min_cut proven

    7 saturated_cut_value proven

    Lean source view on GitHub

    1import Lax342547.ResidualFlows
    2
    3/-!
    4---
    5title: Real max-flow min-cut from residual reachability
    6type: lemma
    7---
    8Internal skew flow cancels, conservation identifies cut divergence with source value, and the reachable residual cut is saturated. Its real capacity equals the maximum flow value, and every cut bounds every feasible flow.
    9-/
    10
    11namespace Lax342547.FlowCuts
    12
    13open Lax342547.RealFlows
    14open scoped BigOperators
    15
    16noncomputable def cutCapacity {V : Type} [Fintype V] (c : V → V → ℝ) (Z : Finset V) : ℝ := by
    17 classical
    18 exact ∑ a ∈ Z, ∑ b ∈ Zᶜ, c a b
    19
    20axiom cut_indicator {V : Type} [Fintype V] (c : V → V → ℝ) (Z : Finset V) : by
    21 classical
    22 exact cutCapacity c Z = ∑ a, ∑ b, if a ∈ Z ∧ b ∉ Z then c a b else 0
    23
    24axiom internal_skew_sum {V : Type} (f : V → V → ℝ) (Z : Finset V)
    25 (hskew : ∀ a b, f a b = -f b a) : (∑ a ∈ Z, ∑ b ∈ Z, f a b) = 0
    26
    27axiom divergence_cut_sum {V : Type} [Fintype V] (f : V → V → ℝ) (Z : Finset V)
    28 (hskew : ∀ a b, f a b = -f b a) : by
    29 classical
    30 exact (∑ a ∈ Z, divergence f a) = ∑ a ∈ Z, ∑ b ∈ Zᶜ, f a b
    31
    32axiom conserving_cut_value {V : Type} [Fintype V] (c f : V → V → ℝ) (s t : V)
    33 (hf : Feasible c f s t) (Z : Finset V) (hs : s ∈ Z) (ht : t ∉ Z) :
    34 (∑ a ∈ Z, divergence f a) = divergence f s
    35
    36axiom saturated_cut_value {V : Type} [Fintype V] (c f : V → V → ℝ) (s t : V)
    37 (hf : Feasible c f s t) (Z : Finset V) (hs : s ∈ Z) (ht : t ∉ Z)
    38 (hsat : ∀ a ∈ Z, ∀ b ∉ Z, f a b = c a b) :
    39 divergence f s = cutCapacity c Z
    40
    41axiom cut_upper_bound {V : Type} [Fintype V] (c f : V → V → ℝ) (s t : V)
    42 (hf : Feasible c f s t) (Z : Finset V) (hs : s ∈ Z) (ht : t ∉ Z) :
    43 divergence f s ≤ cutCapacity c Z
    44
    45axiom real_max_flow_min_cut {V : Type} [Fintype V] (c : V → V → ℝ) (s t : V)
    46 (hst : s ≠ t) (hc : ∀ a b, 0 ≤ c a b) :
    47 ∃ f Z, Feasible c f s t ∧ s ∈ Z ∧ t ∉ Z ∧ divergence f s = cutCapacity c Z ∧
    48 ∀ g, Feasible c g s t → divergence g s ≤ divergence f s
    49
    50end Lax342547.FlowCuts
    51
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    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…