Counting rooted K₄ partners of a triangle edge

A low-degree vertex of a triangle bounds the possible fourth vertices of every rooted K₄ transfer. This is the combinatorial part of nonnegativity.

theorem LeanPool.DrossFractionalTriangleDecomposition.k4_partner_count_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (t : Finset V) (ht : t ∈ G.cliqueFinset 3) (z : V) (hzt : z ∈ t) (hzdeg : G.degree z ≤ G.minDegree + 1) (e : Sym2 V) : e ∈ triEdges t → ↑{e' : Sym2 V | K4pair G e e' ∧ ∃ v ∈ t, v ∈ e' ∧ v ∉ e}.card ≤ ↑G.minDegree - 1

For one edge of a triangle, the number of eligible rooted K₄ partners is at most the minimum degree minus one, provided the triangle has a vertex of degree at most the minimum degree plus one.