K₄ partners across a cut

The partners of a graph edge split disjointly between the two cut sides. One partition identity supplies both directional lower bounds.

theorem LeanPool.DrossFractionalTriangleDecomposition.k4count_cut_partition {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {u v : V} (huv : G.Adj u v) (wΔ : ℝ) (C : Contrib.MaxFlowMinCut.Cut (drossNet G wΔ)) : numK4Through G u v = {e' ∈ cutA G wΔ C | K4pair G s(u, v) e'}.card + {e' ∈ cutB G wΔ C | K4pair G s(u, v) e'}.card

The K₄ partners of an edge are partitioned by the cut.

theorem LeanPool.DrossFractionalTriangleDecomposition.k4count_cutB_ge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {u v : V} (huv : G.Adj u v) (wΔ : ℝ) (C : Contrib.MaxFlowMinCut.Cut (drossNet G wΔ)) : ↑(numK4Through G u v) - ↑(cutA G wΔ C).card ≤ ↑{e' ∈ cutB G wΔ C | K4pair G s(u, v) e'}.card

An A-side edge has at least its total partner count minus |A| partners in B.

theorem LeanPool.DrossFractionalTriangleDecomposition.k4count_cutA_ge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {u v : V} (huv : G.Adj u v) (wΔ : ℝ) (C : Contrib.MaxFlowMinCut.Cut (drossNet G wΔ)) : ↑(numK4Through G u v) - ↑(cutB G wΔ C).card ≤ ↑{e' ∈ cutA G wΔ C | K4pair G s(u, v) e'}.card

A B-side edge has at least its total partner count minus |B| partners in A.