Lax Lean Archive

Deterministic directed uniform flow–cut algorithm

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

    A deterministic polynomial-time word RAM returns a cut and a rational uniform concurrent flow satisfying

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

    on every rational directed nn-vertex instance with n≥2n\ge2.

    Concept map
    8 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.FlowCutCertificate
    2
    3/-!
    4---
    5title: Deterministic directed uniform flow–cut algorithm
    6type: lemma
    7---
    8A deterministic polynomial-time word RAM returns a cut and a rational
    9uniform concurrent flow satisfying
    10ratio⁡(S)≤Clog⁡2(n) f\operatorname{ratio}(S)\le C\log_2(n)\,f
    11on every rational directed nn-vertex instance with n≥2n\ge2.
    12
    13# Formalization notes
    14
    15All input weights equal one. The proof specializes the directed product
    16algorithm; every vertex has positive weight, so p=np=n. Its program, exact
    17output, and registered RAM polynomial-time guarantee are retained.
    18-/
    19
    20open scoped NNReal
    21
    22namespace Lax455465.RamDirectedUniformFlowCut
    23
    24open Lax455465.ProductNetwork Lax455465.ConcurrentFlow
    25open Lax455465.RationalEncoding Lax455465.FlowCutCertificate Lax759944.RamPolytime
    26
    27/-- The uniform directed specialization of the product algorithm. -/
    28axiom exists_polynomial_time_flow_cut :
    29 ∃ (solve : List ℕ → List ℕ) (C : ℝ), RamPolytime solve ∧ 0 < C ∧
    30 ∀ (n : ℕ) (I : RationalInstance n), (∀ v, I.weight v = 1) → 2 ≤ n →
    31 ∃ certificate : Certificate n,
    32 solve (encodeInput .directed I) = encodeCertificate certificate ∧
    33 AdmissibleCut I.weights certificate.cut ∧
    34 IsArcConcurrentFlow .directed I.network I.weights
    35 (certificate.flow.value : ℝ≥0) certificate.flow.flow ∧
    36 (ratioCost I.network I.weights certificate.cut : ℝ) ≤
    37 C * logFactor n * (certificate.flow.value : ℝ)
    38
    39end Lax455465.RamDirectedUniformFlowCut
    40
    Show Proof
    Formalization notes

    All input weights equal one. The proof specializes the directed product algorithm; every vertex has positive weight, so p=np=n. Its program, exact output, and registered RAM polynomial-time guarantee are retained.

    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…