The three families of arcs crossing a Dross cut

Every cut has at least the capacity contributed by source-to-B, A-to-sink, and rooted-K₄ arcs from A to B.

def LeanPool.DrossFractionalTriangleDecomposition.cutA {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (C : Contrib.MaxFlowMinCut.Cut (drossNet G wΔ)) : Finset (Sym2 V)

Real graph edges whose network nodes lie on the source side.

Equations

• LeanPool.DrossFractionalTriangleDecomposition.cutA G wΔ C = {e ∈ G.edgeFinset | LeanPool.DrossFractionalTriangleDecomposition.Ghat.edge e ∈ C.S}

def LeanPool.DrossFractionalTriangleDecomposition.cutB {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (C : Contrib.MaxFlowMinCut.Cut (drossNet G wΔ)) : Finset (Sym2 V)

Edges of G whose node lies on the sink side B of the cut.

Equations

• LeanPool.DrossFractionalTriangleDecomposition.cutB G wΔ C = {e ∈ G.edgeFinset | LeanPool.DrossFractionalTriangleDecomposition.Ghat.edge e ∉ C.S}

theorem LeanPool.DrossFractionalTriangleDecomposition.capacity_lower_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (C : Contrib.MaxFlowMinCut.Cut (drossNet G wΔ)) : (∑ e ∈ cutB G wΔ C, max (↑(triThrough G e) * wΔ - 1) 0 + ∑ e ∈ cutA G wΔ C, max (1 - ↑(triThrough G e) * wΔ) 0 + ∑ e ∈ cutA G wΔ C, ∑ e' ∈ cutB G wΔ C, if K4pair G e e' then max (cc G wΔ) 0 else 0) ≤ C.capacity

Capacity decomposition (lower bound). The capacity of any s–t cut is at least the sum of its three arc families: source→B, A→sink, and the K₄ arcs from A to B. (Non-edge nodes and the src→snk arc only add nonnegative slack, hence a lower bound.)