Convert a triangle packing into an exact clique partition

Proved

Erdos81.cliquePartitionAtMost_edges_sub_twice_trianglePacking

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

clique-partitioncombinatoricsgraph-theorytriangle-packing

Let $G$ have $m$ edges and let $T$ be a family of $t$ edge-disjoint triangles in $G$ . Then $G$ has an exact edge partition into at most

m-2t

cliques.

The statement packages the standard conversion in which the selected triangles are partition pieces and every uncovered edge is a two-vertex clique. Each selected triangle replaces three singleton-edge pieces by one triangle piece, saving two pieces.

Preamble

import Definitions.Def_Erdos81_triangle_packings

Formal statement

namespace Erdos81

/-- Edge-disjoint triangles, together with every uncovered edge as a two-vertex
clique, form an exact clique partition. Each selected triangle saves two pieces. -/
theorem cliquePartitionAtMost_edges_sub_twice_trianglePacking {n : ℕ}
    (G : SimpleGraph (Fin n)) (T : Finset (Finset (Fin n)))
    (hT : IsTrianglePacking G T) :
    HasCliquePartitionAtMost G
      ((edgeCount G : ℝ) - 2 * (T.card : ℝ)) := by
  sorry

end Erdos81

Source

G.-T. Chen, P. Erdős, and E. T. Ordman, Clique partitions of split graphs, Example 1 and its triangle-counting identity, pp. 21–22; https://ordman.net/MathResearch/CEOClique_Parts.pdf

View graph