Bounded K₄ transfer

The partner count and arc capacities bound the total transfer from a triangle by twice its initial weight. No enlarged heartbeat limit is needed.

theorem LeanPool.DrossFractionalTriangleDecomposition.triWeight_transfer_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (hwΔ : 0 < wΔ) (hmd2 : 2 ≤ G.minDegree) (F : Contrib.MaxFlowMinCut.Flow (drossNet 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) (t : Finset V) (ht : t ∈ G.cliqueFinset 3) : (∑ 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) ≤ 2 * wΔ

If no triangle has all three vertices of degree at least δ(G)+2, the total rooted-K₄ flow transfer out of a triangle is at most 2 wΔ.

theorem LeanPool.DrossFractionalTriangleDecomposition.triWeight_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (hwΔ : 0 < wΔ) (hmd2 : 2 ≤ G.minDegree) (F : Contrib.MaxFlowMinCut.Flow (drossNet 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) (t : Finset V) : 0 ≤ triWeight G wΔ F t

Each reconstructed triangle weight is nonnegative.