Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Vertex splitting for the directed flow–cut algorithm

Lax263307.VertexSplitting · concepts/Lax263307/VertexSplitting.lean · lax-263307

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

    Replace each original vertex vv by two ports v−v^- and v+v^+. The capacity of v−→v+v^-\to v^+ is its cost xvx_v. Reverse port arcs and arcs v+→u−v^+\to u^- for graph edges receive a sufficiently large finite capacity. A directed cut of capacity less than this large capacity crosses none of these arcs and projects to a separation of the original graph. Its capacity equals the vertex cost of the projected separator.

    The registered directed uniform flow–cut algorithm applies to this rational split network with its actual RAM polynomial-time guarantee. Each original ordered pair uses the distinct split endpoints u−,v+u^-,v^+, also when u=vu=v.

    Concept map
    9 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.

    1 flow_or_separation proven

    2 separator_cost_bound proven

    3 small_cut_cost proven

    4 small_cut_separation proven

    5 split_certificate proven

    Lean source view on GitHub

    1import Lax455465.RamDirectedUniformFlowCut
    2import Mathlib.Combinatorics.SimpleGraph.Finite
    3import Mathlib.Tactic
    4
    5/-!
    6---
    7title: Vertex splitting for the directed flow–cut algorithm
    8type: theorem
    9---
    10Replace each original vertex vv by two ports v−v^- and v+v^+.
    11The capacity of v−→v+v^-\to v^+ is its cost xvx_v. Reverse port arcs and arcs
    12v+→u−v^+\to u^- for graph edges receive a sufficiently large finite capacity.
    13A directed cut of capacity less than this large capacity crosses none of
    14these arcs and projects to a separation of the original graph. Its capacity
    15equals the vertex cost of the projected separator.
    16
    17The registered directed uniform flow–cut algorithm applies to this rational
    18split network with its actual RAM polynomial-time guarantee. Each original
    19ordered pair uses the distinct split endpoints u−,v+u^-,v^+, also when u=vu=v.
    20
    21# Formalization notes
    22
    23Ports are numbered 2v2v and 2v+12v+1. The cut shores are the vertices whose
    24minus ports lie inside the cut and whose plus ports lie outside it.
    25The cut projection and the external solver's application are proved here;
    26flow projection and the RAM cost of constructing the split input are separate
    27steps of the reduction.
    28
    29# Attribution
    30
    31Bonnet–Chang, the vertex-splitting reduction in Lemma 7, using the registered
    32Leighton–Rao algorithm in Lax455465.
    33-/
    34
    35namespace Lax263307.VertexSplitting
    36
    37open scoped NNReal NNRat
    38open Lax455465.RationalEncoding Lax455465.ProductNetwork Lax455465.ConcurrentFlow
    39
    40/-- The input port of an original vertex. -/
    41def minus {n : ℕ} (v : Fin n) : Fin (2 * n) := ⟨2 * v.val, by omega⟩
    42/-- The output port of an original vertex. -/
    43def plus {n : ℕ} (v : Fin n) : Fin (2 * n) := ⟨2 * v.val + 1, by omega⟩
    44/-- Forget which of the two ports represents a vertex. -/
    45def original {n : ℕ} (v : Fin (2 * n)) : Fin n := ⟨v.val / 2, by omega⟩
    46
    47/-- Rational capacities and uniform demands on the split network. -/
    48def splitInstance {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    49 (x : Fin n → ℚ≥0) (large : ℚ≥0) : RationalInstance (2 * n) where
    50 capacity u v :=
    51 if u.val % 2 = 0 ∧ v.val = u.val + 1 then x (original u)
    52 else if u.val % 2 = 1 ∧ v.val + 1 = u.val then large
    53 else if u.val % 2 = 1 ∧ v.val % 2 = 0 ∧ G.Adj (original u) (original v) then large
    54 else 0
    55 loopless v := by
    56 have hforward : ¬(v.val % 2 = 0 ∧ v.val = v.val + 1) := by omega
    57 have hreverse : ¬(v.val % 2 = 1 ∧ v.val + 1 = v.val) := by omega
    58 have hedge : ¬(v.val % 2 = 1 ∧ v.val % 2 = 0 ∧ G.Adj (original v) (original v)) := by omega
    59 simp only [if_neg hforward, if_neg hreverse, if_neg hedge]
    60 weight _ := 1
    61
    62/-- Original vertices whose input ports lie inside the split cut. -/
    63def leftShore {n : ℕ} (U : Finset (Fin (2 * n))) : Finset (Fin n) :=
    64 Finset.univ.filter fun v => minus v ∈ U
    65
    66/-- Original vertices whose output ports lie outside the split cut. -/
    67def rightShore {n : ℕ} (U : Finset (Fin (2 * n))) : Finset (Fin n) :=
    68 Finset.univ.filter fun v => plus v ∉ U
    69
    70/-- A small split cut projects to a nontrivial separation with controlled shores. -/
    71axiom small_cut_separation {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    72 (x : Fin n → ℚ≥0) (large : ℚ≥0) (U : Finset (Fin (2 * n)))
    73 (small : cutCapacity (splitInstance G x large).network U < (large : ℝ≥0))
    74 (nonempty : U.Nonempty) (proper : Uᶜ.Nonempty) :
    75 (leftShore U).Nonempty ∧ (rightShore U).Nonempty ∧
    76 leftShore U ∪ rightShore U = Finset.univ ∧
    77 (∀ u ∈ leftShore U \ rightShore U, ∀ v ∈ rightShore U \ leftShore U, ¬G.Adj u v) ∧
    78 U.card ≤ 2 * (leftShore U).card ∧ Uᶜ.card ≤ 2 * (rightShore U).card
    79
    80/-- Only the vertex-capacity arcs contribute to a small split cut. -/
    81axiom small_cut_cost {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    82 (x : Fin n → ℚ≥0) (large : ℚ≥0) (U : Finset (Fin (2 * n)))
    83 (small : cutCapacity (splitInstance G x large).network U < (large : ℝ≥0)) :
    84 cutCapacity (splitInstance G x large).network U =
    85 ∑ v ∈ leftShore U ∩ rightShore U, (x v : ℝ≥0)
    86
    87/-- Translate a directed cut ratio into the original separator's vertex cost. -/
    88axiom separator_cost_bound {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    89 (x : Fin n → ℚ≥0) (large : ℚ≥0) (U : Finset (Fin (2 * n))) (ρ : ℝ)
    90 (nonnegative : 0 ≤ ρ)
    91 (small : cutCapacity (splitInstance G x large).network U < (large : ℝ≥0))
    92 (admissible : AdmissibleCut (splitInstance G x large).weights U)
    93 (ratio : (ratioCost (splitInstance G x large).network
    94 (splitInstance G x large).weights U : ℝ) ≤ ρ) :
    95 (∑ v ∈ leftShore U ∩ rightShore U, (x v : ℝ)) ≤
    96 4 * ρ * (leftShore U).card * (rightShore U).card
    97
    98/-- Apply the existing directed uniform solver to every split network. -/
    99axiom split_certificate :
    100 ∃ (solve : List ℕ → List ℕ) (C : ℝ), Lax759944.RamPolytime.RamPolytime solve ∧ 0 < C ∧
    101 ∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    102 (x : Fin n → ℚ≥0) (large : ℚ≥0), 0 < n →
    103 let I := splitInstance G x large
    104 ∃ certificate : Lax455465.FlowCutCertificate.Certificate (2 * n),
    105 solve (encodeInput .directed I) = Lax455465.FlowCutCertificate.encodeCertificate certificate ∧
    106 AdmissibleCut I.weights certificate.cut ∧
    107 IsArcConcurrentFlow .directed I.network I.weights
    108 (certificate.flow.value : ℝ≥0) certificate.flow.flow ∧
    109 (ratioCost I.network I.weights certificate.cut : ℝ) ≤
    110 C * logFactor (2 * n) * (certificate.flow.value : ℝ)
    111
    112/-- A split flow–cut certificate yields a high-value flow or a cheap separation. -/
    113axiom flow_or_separation {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    114 (x : Fin n → ℚ≥0) (large : ℚ≥0)
    115 (certificate : Lax455465.FlowCutCertificate.Certificate (2 * n)) (ρ γ : ℝ)
    116 (nonnegative : 0 ≤ ρ) (positive : 0 < γ)
    117 (admissible : AdmissibleCut (splitInstance G x large).weights certificate.cut)
    118 (flow_valid : IsArcConcurrentFlow .directed (splitInstance G x large).network
    119 (splitInstance G x large).weights (certificate.flow.value : ℝ≥0) certificate.flow.flow)
    120 (ratio : (ratioCost (splitInstance G x large).network
    121 (splitInstance G x large).weights certificate.cut : ℝ) ≤
    122 ρ * (certificate.flow.value : ℝ))
    123 (large_capacity : ρ * (2 * n : ℕ) ^ 2 / γ < (large : ℝ)) :
    124 ((1 / γ ≤ (certificate.flow.value : ℝ)) ∧
    125 IsArcConcurrentFlow .directed (splitInstance G x large).network
    126 (splitInstance G x large).weights (certificate.flow.value : ℝ≥0) certificate.flow.flow) ∨
    127 ((leftShore certificate.cut).Nonempty ∧ (rightShore certificate.cut).Nonempty ∧
    128 leftShore certificate.cut ∪ rightShore certificate.cut = Finset.univ ∧
    129 (∀ u ∈ leftShore certificate.cut \ rightShore certificate.cut,
    130 ∀ v ∈ rightShore certificate.cut \ leftShore certificate.cut, ¬G.Adj u v) ∧
    131 (∑ v ∈ leftShore certificate.cut ∩ rightShore certificate.cut, (x v : ℝ)) ≤
    132 4 * ρ * (leftShore certificate.cut).card * (rightShore certificate.cut).card / γ)
    133
    134end Lax263307.VertexSplitting
    135
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Formalization notes

    Ports are numbered 2v2v and 2v+12v+1. The cut shores are the vertices whose minus ports lie inside the cut and whose plus ports lie outside it. The cut projection and the external solver's application are proved here; flow projection and the RAM cost of constructing the split input are separate steps of the reduction.

    Attribution

    Bonnet–Chang, the vertex-splitting reduction in Lemma 7, using the registered Leighton–Rao algorithm in Lax455465.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…