Double counting rooted K₄ transfers

A K₄ partner has exactly two possible triangle apices over a fixed root edge.

theorem LeanPool.DrossFractionalTriangleDecomposition.two_apex_count {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (e e' : Sym2 V) : {t ∈ G.cliqueFinset 3 | K4pair G e e' ∧ e ∈ triEdges t ∧ ∃ v ∈ t, v ∈ e' ∧ v ∉ e}.card = if K4pair G e e' then 2 else 0

A rooted K₄ pair contributes exactly two triangles over its first edge.

theorem LeanPool.DrossFractionalTriangleDecomposition.flow_zero_off_k4pair {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)) (x y : Sym2 V) (hxy : ¬K4pair G x y) : F.f (Ghat.edge x) (Ghat.edge y) = 0

K₄-ineligible arcs have zero flow, by zero capacity in both directions.

theorem LeanPool.DrossFractionalTriangleDecomposition.hkey_double {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' : 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 * ∑ e' : Sym2 V, F.f (Ghat.edge e) (Ghat.edge e')

Summing over triangles through e, each K₄-partner contributes twice.

theorem LeanPool.DrossFractionalTriangleDecomposition.tri_eq_edge_union {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {t : Finset V} {e e2 : Sym2 V} (htc : t ∈ G.cliqueFinset 3) (het : e ∈ triEdges t) (he2 : e2 ∈ (triEdges t).erase e) : e.toFinset ∪ e2.toFinset = t