Edge coverage by reconstructed triangle weights

The doubled on-edge transfer and off-edge cancellation reduce coverage to flow conservation at the edge node.

theorem LeanPool.DrossFractionalTriangleDecomposition.triWeight_transfer_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (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) (he : e ∈ G.edgeFinset) : (∑ t ∈ G.cliqueFinset 3, if e ∈ triEdges t then ∑ e'' ∈ triEdges t, ∑ e' : Sym2 V, if K4pair G e'' e' ∧ ∃ v ∈ t, v ∈ e' ∧ v ∉ e'' then F.f (Ghat.edge e'') (Ghat.edge e') else 0 else 0) = 2 * (↑(triThrough G e) * wΔ - 1)

The total K₄ transfer through a fixed graph edge is twice its flow excess.

theorem LeanPool.DrossFractionalTriangleDecomposition.triWeight_coverage {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (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) (he : e ∈ G.edgeFinset) : (∑ t ∈ G.cliqueFinset 3, if e ∈ triEdges t then triWeight G wΔ F t else 0) = 1

The reconstructed triangle weights sum to one on each graph edge.

theorem LeanPool.DrossFractionalTriangleDecomposition.decomp_of_maxflowM {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (hwΔ : 0 < wΔ) (hmd2 : 2 ≤ G.minDegree) (hbal : ∑ e ∈ G.edgeFinset, (↑(triThrough G e) * wΔ - 1) = 0) (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)) (hF : F.value = demand G wΔ) (hNoHDT : ∀ (u v w : V), G.Adj u v → G.Adj u w → G.Adj v w → G.minDegree + 2 ≤ G.degree u → G.minDegree + 2 ≤ G.degree v → G.minDegree + 2 ≤ G.degree w → False) : FractionalTriangleDecomp G

A demand-saturating flow yields a fractional triangle decomposition.