Lax Lean Archive

Deterministic polynomial-time product flow–cut algorithm

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

    Theorem

    One deterministic polynomial-time word-RAM algorithm returns a rational concurrent flow and a positive-demand cut for every rational product-demand instance with p≥2p\ge2 positive-weight vertices. Their values satisfy

    ratio⁡(S)≤Clog⁡2(p) f\operatorname{ratio}(S)\le C\log_2(p)\,f

    for one universal constant C>0C>0. The input may have directed arcs with asymmetric capacities, or undirected edges with shared capacities.

    Concept map
    8 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.FlowCutCertificate
    2
    3/-!
    4---
    5title: Deterministic polynomial-time product flow–cut algorithm
    6type: theorem
    7---
    8One deterministic polynomial-time word-RAM algorithm returns a rational
    9concurrent flow and a positive-demand cut for every rational product-demand
    10instance with p≥2p\ge2 positive-weight vertices. Their values satisfy
    11ratio⁡(S)≤Clog⁡2(p) f\operatorname{ratio}(S)\le C\log_2(p)\,f
    12for one universal constant C>0C>0. The input may have directed arcs with
    13asymmetric capacities, or undirected edges with shared capacities.
    14
    15# Formalization notes
    16
    17This is the constructive form of Theorems 7 and 17 of Leighton and Rao
    18(1999). Zero-weight transit vertices and arbitrary rational capacities and
    19weights are allowed. Uniform instances and the two edge models are
    20specializations of this single statement. The edge model is supplied in the
    21input encoding; its symmetry hypothesis applies to undirected instances.
    22
    23The algorithm returns the exact joint certificate. The registered
    24`RamPolytime` predicate certifies a single deterministic program, measured
    25in binary input size, at every sufficiently large word length. Neither the
    26LP solution nor the rounding step is an assumed computational oracle.
    27-/
    28
    29namespace Lax455465.RamProductFlowCut
    30
    31open Lax455465.ProductNetwork Lax455465.RationalEncoding Lax455465.FlowCutCertificate
    32open Lax759944.RamPolytime
    33
    34/-- A uniform deterministic RAM constructs a logarithmic flow–cut certificate. -/
    35axiom exists_polynomial_time_flow_cut :
    36 ∃ (solve : List ℕ → List ℕ) (C : ℝ), RamPolytime solve ∧ 0 < C ∧
    37 ∀ (kind : EdgeKind) (n : ℕ) (I : RationalInstance n),
    38 (kind = .undirected → I.network.IsUndirected) →
    39 2 ≤ supportCount I.weights →
    40 ∃ certificate : Certificate n,
    41 solve (encodeInput kind I) = encodeCertificate certificate ∧
    42 IsValid kind I C certificate
    43
    44end Lax455465.RamProductFlowCut
    45
    Show Proof
    Formalization notes

    This is the constructive form of Theorems 7 and 17 of Leighton and Rao (1999). Zero-weight transit vertices and arbitrary rational capacities and weights are allowed. Uniform instances and the two edge models are specializations of this single statement. The edge model is supplied in the input encoding; its symmetry hypothesis applies to undirected instances.

    The algorithm returns the exact joint certificate. The registered RamPolytimeRamPolytime predicate certifies a single deterministic program, measured in binary input size, at every sufficiently large word length. Neither the LP solution nor the rounding step is an assumed computational oracle.

    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…