Lax Lean Archive

Deterministic undirected product flow–cut algorithm

Lax455465.RamUndirectedSparsestCut · concepts/Lax455465/RamUndirectedSparsestCut.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 concurrent flow satisfying

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

    Both certificates concern the same rational product-demand instance.

    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 product flow–cut algorithm
    6type: lemma
    7---
    8A deterministic polynomial-time word RAM returns a cut and a rational
    9concurrent flow satisfying
    10ratio⁡(S)≤Clog⁡2(p) f.\operatorname{ratio}(S)\le C\log_2(p)\,f.
    11Both certificates concern the same rational product-demand instance.
    12
    13# Formalization notes
    14
    15This specializes the general product flow–cut algorithm to undirected
    16capacities and demands, retaining its program, exact output, and binary-size
    17RAM bound. Undirected capacities are symmetric and shared between directions;
    18directed cuts count outgoing arcs and directed capacities may be asymmetric.
    19-/
    20
    21namespace Lax455465.RamUndirectedSparsestCut
    22
    23open Lax455465.ProductNetwork Lax455465.RationalEncoding Lax455465.FlowCutCertificate
    24open Lax759944.RamPolytime
    25
    26/-- The undirected product specialization returns the joint certificate. -/
    27axiom exists_polynomial_time_sparse_cut :
    28 ∃ (solve : List ℕ → List ℕ) (C : ℝ), RamPolytime solve ∧ 0 < C ∧
    29 ∀ (n : ℕ) (I : RationalInstance n),
    30 I.network.IsUndirected → 2 ≤ supportCount I.weights →
    31 ∃ certificate : Certificate n,
    32 solve (encodeInput .undirected I) = encodeCertificate certificate ∧
    33 IsValid .undirected I C certificate
    34
    35end Lax455465.RamUndirectedSparsestCut
    36
    Show Proof
    Formalization notes

    This specializes the general product flow–cut algorithm to undirected capacities and demands, retaining its program, exact output, and binary-size RAM bound. Undirected capacities are symmetric and shared between directions; directed cuts count outgoing arcs and directed capacities may be asymmetric.

    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…