Lax Lean Archive

Deterministic undirected uniform flow–cut algorithm

Lax455465.RamUniformFlowCut · concepts/Lax455465/RamUniformFlowCut.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 undirected 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 undirected 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 undirected nn-vertex instance with n≥2n\ge2.
    12
    13# Formalization notes
    14
    15All input weights equal one. The proof specializes the undirected 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.RamUniformFlowCut
    23
    24open Lax455465.ProductNetwork Lax455465.ConcurrentFlow
    25open Lax455465.RationalEncoding Lax455465.FlowCutCertificate Lax759944.RamPolytime
    26
    27/-- The uniform undirected 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),
    31 I.network.IsUndirected → (∀ v, I.weight v = 1) → 2 ≤ n →
    32 ∃ certificate : Certificate n,
    33 solve (encodeInput .undirected I) = encodeCertificate certificate ∧
    34 AdmissibleCut I.weights certificate.cut ∧
    35 IsArcConcurrentFlow .undirected I.network I.weights
    36 (certificate.flow.value : ℝ≥0) certificate.flow.flow ∧
    37 (ratioCost I.network I.weights certificate.cut : ℝ) ≤
    38 C * logFactor n * (certificate.flow.value : ℝ)
    39
    40end Lax455465.RamUniformFlowCut
    41
    Show Proof
    Formalization notes

    All input weights equal one. The proof specializes the undirected 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…