Cancellation configurations for Dross's K₄ transfers

A configuration records a triangle, one of its non-root edges, and a K₄ partner. Swapping the two transfer edges preserves these configurations.

def LeanPool.DrossFractionalTriangleDecomposition.cancellationConfigs {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (e : Sym2 V) : Finset (Finset V × Sym2 V × Sym2 V)

Configurations contributing to the off-root K₄-transfer sum.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.DrossFractionalTriangleDecomposition.cancellationConfigs_swap_mem {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (e : Sym2 V) (p : Finset V × Sym2 V × Sym2 V) (hp : p ∈ cancellationConfigs G e) : (e.toFinset ∪ p.2.2.toFinset, p.2.2, p.2.1) ∈ cancellationConfigs G e

Interchanging the transfer edges gives another valid configuration.