Lax Lean Archive

Classical product multicommodity flow–cut bound

Lax455465.ProductFlowCut · concepts/Lax455465/ProductFlowCut.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

    For one universal constant C>0C>0, every rational product-demand instance with p≥2p\ge2 positive-weight vertices satisfies

    sparsestCut⁡(G,π)≤Clog⁡2(p) maxFlow⁡(G,π).\operatorname{sparsestCut}(G,\pi) \le C\log_2(p)\,\operatorname{maxFlow}(G,\pi).

    The statement covers directed arcs with separate capacities and symmetric undirected edges with shared capacities. Uniform demand is the all-one specialization.

    Concept map
    10 concepts
    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.RamProductFlowCut
    2import Lax455465.ArcToPath
    3
    4/-!
    5---
    6title: Classical product multicommodity flow–cut bound
    7type: lemma
    8---
    9For one universal constant C>0C>0, every rational product-demand instance
    10with p≥2p\ge2 positive-weight vertices satisfies
    11sparsestCut⁡(G,π)≤Clog⁡2(p) maxFlow⁡(G,π).\operatorname{sparsestCut}(G,\pi) \le C\log_2(p)\,\operatorname{maxFlow}(G,\pi).
    12
    13The statement covers directed arcs with separate capacities and symmetric
    14undirected edges with shared capacities. Uniform demand is the all-one
    15specialization.
    16
    17# Formalization notes
    18
    19The maximum flow is the supremum over the real-valued simple-path flows
    20defined in `ConcurrentFlow`. This corollary uses the joint certificate
    21returned by the deterministic RAM algorithm and the public arc-to-path
    22conversion, connecting the algorithmic guarantee to the classical values.
    23-/
    24
    25namespace Lax455465.ProductFlowCut
    26open Lax455465.ProductNetwork Lax455465.ConcurrentFlow Lax455465.RationalEncoding
    27
    28/-- The classical flow–cut inequality follows from the constructive certificate. -/
    29axiom exists_flow_cut_bound :
    30 ∃ C : ℝ, 0 < C ∧
    31 ∀ (kind : EdgeKind) (n : ℕ) (I : RationalInstance n),
    32 (kind = .undirected → I.network.IsUndirected) →
    33 2 ≤ supportCount I.weights →
    34 (sparsestCut I.network I.weights : ℝ) ≤
    35 C * logFactor (supportCount I.weights) * (maxFlow kind I.network I.weights : ℝ)
    36
    37end Lax455465.ProductFlowCut
    38
    Show Proof
    Formalization notes

    The maximum flow is the supremum over the real-valued simple-path flows defined in ConcurrentFlowConcurrentFlow. This corollary uses the joint certificate returned by the deterministic RAM algorithm and the public arc-to-path conversion, connecting the algorithmic guarantee to the classical values.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…