Complete a triangle packing with exact piece count

Proved

Erdos81.trianglePacking_completion_count

by Yuning · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

clique-partitioncombinatoricsgraph-theorytriangle-packing

Let $G$ be a finite graph with $m$ edges, and let $T$ be a family of $t$ pairwise edge-disjoint triangles in $G$ . There exists an exact edge partition $P$ into cliques satisfying

|P|+2t=m.

The intended partition consists of the selected triangles together with every uncovered edge as a two-vertex clique. Because the triangles are edge-disjoint, they cover exactly $3t$ distinct edges; replacing those $3t$ singleton-edge pieces by $t$ triangles saves exactly $2t$ pieces. The statement records the constructive natural-number identity separately from later real-valued asymptotic estimates.

Preamble

import Definitions.Def_Erdos81_triangle_packings

Formal statement

namespace Erdos81

/-- Completing an edge-disjoint triangle packing with all uncovered edges gives
an exact clique partition; each triangle saves exactly two pieces. -/
theorem trianglePacking_completion_count {n : ℕ}
    (G : SimpleGraph (Fin n)) (T : Finset (Finset (Fin n)))
    (hT : IsTrianglePacking G T) :
    ∃ P : Finset (Finset (Fin n)),
      IsEdgeCliquePartition G P ∧
      P.card + 2 * T.card = edgeCount G := by
  sorry

end Erdos81

Source

Standard packing-to-partition counting identity; see G.-T. Chen, P. Erdős, and E. T. Ordman, Clique partitions of split graphs, Example 1, pp. 21–22, https://ordman.net/MathResearch/CEOClique_Parts.pdf. Reduction child for Prove2Me theorem Erdos81.cliquePartitionAtMost_edges_sub_twice_trianglePacking.

View graph