Triangle and fractional triangle packings for Erdős Problem 81

Definition

Erdos81_triangle_packings

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

chordal-graphscombinatoricsfractional-packinggraph-theorytriangle-packing

For a finite graph $G$ , this bundle defines: (1) the number $m(G)$ of unordered edges; (2) an integral triangle packing, meaning a finite family of three-vertex cliques in which no graph edge lies in two selected triangles; (3) a fractional triangle packing, assigning nonnegative weights to triangles so that the total weight through each edge is at most one; and (4) the total fractional weight.

These notions isolate the packing interface used to reduce chordal clique partitions to fixed-triangle packing. The definitions are specialized to graphs on $\operatorname{Fin}(n)$ so every relevant sum is finite.

Formalization Note Fractional weights are functions on all vertex subsets; the definition forces the weight of every non-triangle to vanish.

Definition code

import Definitions.Def_erdos81_clique_partitions
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Finset.Powerset

namespace Erdos81

/-- The number of (unordered) edges of a finite graph. -/
noncomputable def edgeCount {n : ℕ} (G : SimpleGraph (Fin n)) : ℕ := by
  letI := Fintype.ofFinite G.edgeSet
  exact G.edgeFinset.card

/-- A family of edge-disjoint triangles in a finite graph. -/
def IsTrianglePacking {n : ℕ} (G : SimpleGraph (Fin n))
    (T : Finset (Finset (Fin n))) : Prop :=
  (∀ C ∈ T, C.card = 3 ∧ IsClique G C) ∧
  ∀ ⦃u v : Fin n⦄, G.Adj u v →
    ∀ ⦃C₁ C₂ : Finset (Fin n)⦄,
      C₁ ∈ T → u ∈ C₁ → v ∈ C₁ →
      C₂ ∈ T → u ∈ C₂ → v ∈ C₂ → C₁ = C₂

/-- A fractional packing of triangles, with total weight at most one through
any graph edge. Weights outside the triangles of `G` must vanish. -/
def IsFractionalTrianglePacking {n : ℕ} (G : SimpleGraph (Fin n))
    (w : Finset (Fin n) → ℝ) : Prop :=
  (∀ C, 0 ≤ w C) ∧
  (∀ C, w C ≠ 0 → C.card = 3 ∧ IsClique G C) ∧
  ∀ ⦃u v : Fin n⦄, G.Adj u v →
    (∑ C ∈ Finset.univ.powerset, if u ∈ C ∧ v ∈ C then w C else 0) ≤ 1

/-- Total weight of a fractional triangle packing. -/
def fractionalTrianglePackingWeight {n : ℕ}
    (w : Finset (Fin n) → ℝ) : ℝ :=
  ∑ C ∈ Finset.univ.powerset, w C

end Erdos81

Source

Raphael Yuster, Integer and fractional packing of families of graphs, arXiv:math/0305350v4, Section 1 definitions of integral and fractional F-packings, specialized to F = {K_3}; https://arxiv.org/html/math/0305350v4

View graph