Lax Lean Archive

Polynomial-time RAM construction of a uniform short-path flow

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

    There is a polynomial-time word-RAM algorithm and universal constants A,B>0A,B>0 such that, on every rational undirected uniform instance with n≥2n\ge2 and positive sparsest-cut value S\mathcal S, it returns a rational fractional flow certificate meeting a common fraction ff of all demands, where

    S≤Alog⁡2(n)f,\mathcal S\le A\log_2(n)f,

    and every path carrying flow has length at most

    BCmax⁡log⁡2(n)nS.\frac{B C_{\max}\log_2(n)}{n\mathcal S}.
    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.RationalEncoding
    2import Lax455465.ShortPathFlow
    3
    4/-!
    5---
    6title: Polynomial-time RAM construction of a uniform short-path flow
    7type: theorem
    8---
    9There is a polynomial-time word-RAM algorithm and universal constants A,B>0A,B>0
    10such that, on every rational undirected uniform instance with n≥2n\ge2 and
    11positive sparsest-cut value S\mathcal S, it returns a rational fractional
    12flow certificate meeting a common fraction ff of all demands, where
    13S≤Alog⁡2(n)f,\mathcal S\le A\log_2(n)f,
    14and every path carrying flow has length at most
    15BCmax⁡log⁡2(n)nS.\frac{B C_{\max}\log_2(n)}{n\mathcal S}.
    16
    17# Formalization notes
    18
    19This states the algorithmic assertion accompanying Theorem 18 of Leighton
    20and Rao (1999). The same decoded certificate must satisfy capacities, every
    21commodity demand, the flow-value bound, and the path-length bound. Its exact
    22rational output is produced by a program certified by the registered RAM
    23polynomial-time predicate. All-one weights are required in the input encoding.
    24-/
    25
    26open scoped NNReal
    27
    28namespace Lax455465.RamUniformShortPathFlow
    29
    30open Lax455465.ProductNetwork Lax455465.ConcurrentFlow
    31open Lax455465.ShortPathFlow Lax455465.RationalEncoding Lax759944.RamPolytime
    32
    33/-- A polynomial-time RAM constructs a feasible uniform flow with the
    34value and path-length guarantees of Theorem 18. -/
    35axiom exists_polynomial_time_short_path_flow :
    36 ∃ (solve : List ℕ → List ℕ) (A B : ℝ),
    37 RamPolytime solve ∧ 0 < A ∧ 0 < B ∧
    38 ∀ (n : ℕ) (I : RationalInstance n),
    39 I.network.IsUndirected → (∀ v, I.weight v = 1) → 2 ≤ n →
    40 0 < sparsestCut I.network (uniformWeight n) →
    41 ∃ certificate : FlowCertificate n,
    42 solve (encodeInput .undirected I) = encodeFlow certificate ∧
    43 IsConcurrentFlow .undirected I.network (uniformWeight n)
    44 (certificate.value : ℝ≥0) certificate.flow ∧
    45 (sparsestCut I.network (uniformWeight n) : ℝ) ≤
    46 A * logFactor n * (certificate.value : ℝ) ∧
    47 HasPathLengthAtMost certificate.flow
    48 (B * (maxIncidentCapacity I.network : ℝ) * logFactor n /
    49 ((n : ℝ) * (sparsestCut I.network (uniformWeight n) : ℝ)))
    50
    51end Lax455465.RamUniformShortPathFlow
    52
    Show Proof
    Formalization notes

    This states the algorithmic assertion accompanying Theorem 18 of Leighton and Rao (1999). The same decoded certificate must satisfy capacities, every commodity demand, the flow-value bound, and the path-length bound. Its exact rational output is produced by a program certified by the registered RAM polynomial-time predicate. All-one weights are required in the input encoding.

    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…