Cancellation of off-root K₄ transfers

The two configurations obtained by swapping transfer edges have opposite flow.

theorem LeanPool.DrossFractionalTriangleDecomposition.hkey_cancel {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)) (e : Sym2 V) : (∑ t ∈ G.cliqueFinset 3, if e ∈ triEdges t then ∑ e'' ∈ (triEdges t).erase e, ∑ 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) = 0

The off-root transfer terms cancel in pairs.