The sum-zero triple system: a near-perfect triangle packing of a complete graph

This file gives an explicit, constructive family of pairwise edge-disjoint triangles inside an arbitrary finite vertex set U which leaves at most 3 uncovered edges at each vertex.

The construction is a sum-zero triple system. Label the n = |U| vertices bijectively by the elements of the cyclic group ZMod n and take as triangles all triples of distinct vertices whose labels sum to 0. Two such triples sharing an edge share two labels, and the third label is then determined, so the triples are pairwise edge-disjoint. A pair of distinct labels x ≠ y fails to be covered only when the determined third label -(x + y) equals x or y, that is, only when y = -2x or 2y = -x; for fixed x there is at most one label y with y = -2x, and at most two labels y with 2y = -x, because the doubling map of ZMod n has fibres of size at most 2. Hence at most 3 edges at each vertex remain uncovered.

Main definitions

• Finset.innerEdges: the non-loop edges of the complete graph lying inside a finite set.
• Finset.familyEdges: the edges covered by a family of finite sets.
• Finset.edgeDegree: the number of edges of a given edge set incident to a vertex.
• SumZeroTriangles.sumZeroTriples: the triples of a labelled vertex set whose labels sum to zero.

Main results

• ZMod.card_filter_two_mul_eq_le: every fibre of the doubling map x ↦ 2 * x of ZMod n has at most two elements.
• SumZeroTriangles.sumZeroTriples_disjoint: sum-zero triples with an injective labelling are pairwise edge-disjoint.
• SumZeroTriangles.sumZeroTriples_edgeDegree_sdiff_le: the sum-zero triple system leaves at most three uncovered edges at every vertex.
• SumZeroTriangles.exists_triangle_packing_clique: every finite vertex set carries a family of pairwise edge-disjoint triangles leaving at most three uncovered edges at every vertex.

Implementation notes

Edges are modelled as elements of Sym2 V, and edge sets as Finset (Sym2 V); a triangle is a Finset V of cardinality 3 and the triangles of a family are required to have pairwise disjoint edge sets.

theorem ZMod.card_filter_two_mul_eq_zero_le (n : ℕ) [NeZero n] : {z : ZMod n | 2 * z = 0}.card ≤ 2

The kernel of the doubling map of ZMod n has at most two elements.

theorem ZMod.card_filter_two_mul_eq_le (n : ℕ) [NeZero n] (c : ZMod n) : {z : ZMod n | 2 * z = c}.card ≤ 2

Every fibre of the doubling map x ↦ 2 * x of ZMod n has at most two elements.

def Finset.innerEdges {V : Type u_1} [DecidableEq V] (s : Finset V) : Finset (Sym2 V)

The edges of the complete graph on V lying inside the finite set s, that is, the non-loop unordered pairs both of whose entries belong to s.

Equations

• s.innerEdges = {e ∈ s.sym2 | ¬e.IsDiag}

@[simp]

theorem Finset.mem_innerEdges {V : Type u_1} [DecidableEq V] {s : Finset V} {e : Sym2 V} : e ∈ s.innerEdges ↔ (∀ v ∈ e, v ∈ s) ∧ ¬e.IsDiag

def Finset.familyEdges {V : Type u_1} [DecidableEq V] (P : Finset (Finset V)) : Finset (Sym2 V)

The set of edges covered by a family P of finite vertex sets.

Equations

• P.familyEdges = P.biUnion Finset.innerEdges

theorem Finset.mem_familyEdges {V : Type u_1} [DecidableEq V] {P : Finset (Finset V)} {e : Sym2 V} : e ∈ P.familyEdges ↔ ∃ t ∈ P, e ∈ t.innerEdges

def Finset.edgeDegree {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (v : V) : ℕ

The number of edges of the edge set E that are incident to the vertex v.

Equations

• E.edgeDegree v = {e ∈ E | v ∈ e}.card

The sum-zero triple system

def SumZeroTriangles.sumZeroTriples {V : Type u_1} (n : ℕ) (U : Finset V) (psi : V → ZMod n) : Finset (Finset V)

The triples of the vertex set U, labelled by psi : V → ZMod n, whose labels sum to zero.

Equations

• SumZeroTriangles.sumZeroTriples n U psi = {t ∈ U.powerset | t.card = 3 ∧ ∑ v ∈ t, psi v = 0}

theorem SumZeroTriangles.mem_sumZeroTriples {V : Type u_1} {n : ℕ} {U : Finset V} {psi : V → ZMod n} {t : Finset V} : t ∈ sumZeroTriples n U psi ↔ t ⊆ U ∧ t.card = 3 ∧ ∑ v ∈ t, psi v = 0

Membership in sumZeroTriples: a triple of U with vanishing label sum.

theorem SumZeroTriangles.exists_sdiff_pair_eq_singleton {V : Type u_1} [DecidableEq V] {t : Finset V} (ht : t.card = 3) {a b : V} (ha : a ∈ t) (hb : b ∈ t) (hab : a ≠ b) : ∃ (c : V), t \ {a, b} = {c}

In a three-element set containing the distinct elements a and b there is a unique third element.

theorem SumZeroTriangles.third_label {V : Type u_1} [DecidableEq V] {n : ℕ} {U : Finset V} {psi : V → ZMod n} {t : Finset V} (ht : t ∈ sumZeroTriples n U psi) {a b c : V} (ha : a ∈ t) (hb : b ∈ t) (hab : a ≠ b) (hc : t \ {a, b} = {c}) : psi c = -(psi a + psi b)

The label of the third vertex of a sum-zero triple is determined by the other two.

theorem SumZeroTriangles.sumZeroTriples_disjoint {V : Type u_1} [DecidableEq V] {n : ℕ} {U : Finset V} {psi : V → ZMod n} (hinj : ∀ x ∈ U, ∀ y ∈ U, psi x = psi y → x = y) (t : Finset V) : t ∈ sumZeroTriples n U psi → ∀ t' ∈ sumZeroTriples n U psi, t ≠ t' → Disjoint t.innerEdges t'.innerEdges

The sum-zero triples of an injectively labelled vertex set are pairwise edge-disjoint.

theorem SumZeroTriangles.canonical_triple_mem {V : Type u_1} [DecidableEq V] {n : ℕ} {U : Finset V} {psi : V → ZMod n} (rho : ZMod n → V) (hrhoU : ∀ (z : ZMod n), rho z ∈ U) (hrho : ∀ (z : ZMod n), psi (rho z) = z) {a b : V} (ha : a ∈ U) (hb : b ∈ U) (hab : a ≠ b) (h1 : psi b ≠ -(2 * psi a)) (h2 : 2 * psi b ≠ -psi a) : {a, b, rho (-(psi a + psi b))} ∈ sumZeroTriples n U psi ∧ rho (-(psi a + psi b)) ≠ a ∧ rho (-(psi a + psi b)) ≠ b

The canonical sum-zero triple through an edge whose two labels are not exceptional: it is a genuine triple of U and its third vertex is distinct from the two endpoints.

theorem SumZeroTriangles.mem_innerEdges_triple {V : Type u_1} [DecidableEq V] {a b c : V} (hab : a ≠ b) : s(a, b) ∈ {a, b, c}.innerEdges

The edge s(a, b) belongs to the edge set of the triple {a, b, c}.

theorem SumZeroTriangles.mem_familyEdges_sumZeroTriples {V : Type u_1} [DecidableEq V] {n : ℕ} {U : Finset V} {psi : V → ZMod n} (rho : ZMod n → V) (hrhoU : ∀ (z : ZMod n), rho z ∈ U) (hrho : ∀ (z : ZMod n), psi (rho z) = z) {a b : V} (ha : a ∈ U) (hb : b ∈ U) (hab : a ≠ b) (h1 : psi b ≠ -(2 * psi a)) (h2 : 2 * psi b ≠ -psi a) : s(a, b) ∈ (sumZeroTriples n U psi).familyEdges

Every edge whose two labels are not in the exceptional relation is covered by the sum-zero triple system.

theorem SumZeroTriangles.card_exceptional_le {V : Type u_1} {n : ℕ} {U : Finset V} {psi : V → ZMod n} [NeZero n] (hinj : ∀ x ∈ U, ∀ y ∈ U, psi x = psi y → x = y) (v : V) : {u ∈ U | psi u = -(2 * psi v) ∨ 2 * psi u = -psi v}.card ≤ 3

There are at most three exceptional partners of a vertex, that is, vertices u ∈ U whose label satisfies psi u = -2 * psi v or 2 * psi u = -psi v.

theorem SumZeroTriangles.sumZeroTriples_edgeDegree_sdiff_le {V : Type u_1} [DecidableEq V] {n : ℕ} {U : Finset V} {psi : V → ZMod n} [NeZero n] (rho : ZMod n → V) (hrhoU : ∀ (z : ZMod n), rho z ∈ U) (hrho : ∀ (z : ZMod n), psi (rho z) = z) (hinj : ∀ x ∈ U, ∀ y ∈ U, psi x = psi y → x = y) (v : V) : (U.innerEdges \ (sumZeroTriples n U psi).familyEdges).edgeDegree v ≤ 3

The uncovered degree of the sum-zero triple system is at most 3 at every vertex.

The near-perfect triangle packing of a clique

theorem SumZeroTriangles.exists_triangle_packing_clique {V : Type u_1} [DecidableEq V] (U : Finset V) : ∃ (P : Finset (Finset V)), (∀ t ∈ P, t.card = 3) ∧ (∀ t ∈ P, t ⊆ U) ∧ (∀ t ∈ P, ∀ t' ∈ P, t ≠ t' → Disjoint t.innerEdges t'.innerEdges) ∧ ∀ (v : V), (U.innerEdges \ P.familyEdges).edgeDegree v ≤ 3

A near-perfect triangle packing of a complete graph.

For every finite set U of vertices there is a family of pairwise edge-disjoint triangles inside U which leaves at most three uncovered edges at every vertex. (For |U| ≡ 1, 3 [MOD 6] a Steiner triple system leaves no uncovered edge at all; the sum-zero construction used here is uniform in |U| and gives the bound 3 in all cases.)