Saturation in Dross's auxiliary network

When a flow meets the network demand, the source and sink arcs of real graph edges are saturated. This is the accounting step before reconstructing weights.

theorem LeanPool.DrossFractionalTriangleDecomposition.card4_pairwise {V : Type u_1} [DecidableEq V] {a b c d : V} (h : {a, b, c, d}.card = 4) : a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

The four vertices of a four-element set are pairwise distinct.

theorem LeanPool.DrossFractionalTriangleDecomposition.k4pair_iff_clique {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (u v c d : V) : K4pair G s(u, v) s(c, d) ↔ G.IsNClique 4 {u, v, c, d}

A rooted-K₄ pair on uv is exactly a 4-clique on the four endpoints.

theorem LeanPool.DrossFractionalTriangleDecomposition.k4pair_symm {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (e₁ e₂ : Sym2 V) : K4pair G e₁ e₂ ↔ K4pair G e₂ e₁

The rooted-K₄ pair relation is symmetric.

theorem LeanPool.DrossFractionalTriangleDecomposition.not_K4pair_of_notMem {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] {e : Sym2 V} (he : e ∉ G.edgeFinset) (e' : Sym2 V) : ¬K4pair G e e'

A non-edge is in no rooted-K₄ pair.

theorem LeanPool.DrossFractionalTriangleDecomposition.sinkflow_zero_of_notMem {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) [Fintype V] (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)) {e : Sym2 V} (he : e ∉ G.edgeFinset) : F.f (Ghat.edge e) Ghat.snk = 0

At a non-edge node the flow to the sink vanishes.

theorem LeanPool.DrossFractionalTriangleDecomposition.sink_saturated {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) [Fintype V] (hbal : ∑ e ∈ G.edgeFinset, (↑(triThrough G e) * wΔ - 1) = 0) (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)) (hF : F.value = demand G wΔ) (e : Sym2 V) : e ∈ G.edgeFinset → F.f (Ghat.edge e) Ghat.snk = max (1 - ↑(triThrough G e) * wΔ) 0

If the flow meets the demand, every real-edge sink arc is saturated.

theorem LeanPool.DrossFractionalTriangleDecomposition.edgeNode_flow_sum {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) [Fintype V] (hbal : ∑ e ∈ G.edgeFinset, (↑(triThrough G e) * wΔ - 1) = 0) (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)) (hF : F.value = demand G wΔ) {f₀ : Sym2 V} (hf₀ : f₀ ∈ G.edgeFinset) : ∑ e' : Sym2 V, F.f (Ghat.edge f₀) (Ghat.edge e') = ↑(triThrough G f₀) * wΔ - 1

Conservation gives the signed source excess at each real edge node.