Simple graph interface for the sum-zero triangle packing

This file translates the finite edge-set formulation of the sum-zero construction into Mathlib's SimpleGraph API. It leaves the constructive implementation in SumZeroTriangles.lean while providing graph-valued triangles, their union, and a complete-graph corollary stated using graph disjointness and degree.

def SumZeroTriangles.triangleGraph {V : Type u_1} [DecidableEq V] (t : Finset V) : SimpleGraph V

The simple graph consisting of the edges spanned by the vertices in t.

Equations

• SumZeroTriangles.triangleGraph t = SimpleGraph.fromEdgeSet ↑t.innerEdges

def SumZeroTriangles.packingGraph {V : Type u_1} [DecidableEq V] (P : Finset (Finset V)) : SimpleGraph V

The simple graph consisting of all edges covered by the triples in P.

Equations

• SumZeroTriangles.packingGraph P = SimpleGraph.fromEdgeSet ↑P.familyEdges

@[instance_reducible]

instance SumZeroTriangles.instDecidableAdjTriangleGraph {V : Type u_1} [DecidableEq V] (t : Finset V) : DecidableRel (triangleGraph t).Adj

Equations

• SumZeroTriangles.instDecidableAdjTriangleGraph t = id inferInstance

@[instance_reducible]

instance SumZeroTriangles.instDecidableAdjPackingGraph {V : Type u_1} [DecidableEq V] (P : Finset (Finset V)) : DecidableRel (packingGraph P).Adj

Equations

• SumZeroTriangles.instDecidableAdjPackingGraph P = id inferInstance

@[instance_reducible]

instance SumZeroTriangles.instFintypeEdgeSetTriangleGraph {V : Type u_1} [DecidableEq V] (t : Finset V) : Fintype ↑(triangleGraph t).edgeSet

Equations

• SumZeroTriangles.instFintypeEdgeSetTriangleGraph t = id inferInstance

@[instance_reducible]

instance SumZeroTriangles.instFintypeEdgeSetPackingGraph {V : Type u_1} [DecidableEq V] (P : Finset (Finset V)) : Fintype ↑(packingGraph P).edgeSet

Equations

• SumZeroTriangles.instFintypeEdgeSetPackingGraph P = id inferInstance

@[simp]

theorem SumZeroTriangles.edgeSet_triangleGraph {V : Type u_1} [DecidableEq V] (t : Finset V) : (triangleGraph t).edgeSet = ↑t.innerEdges

@[simp]

theorem SumZeroTriangles.edgeSet_packingGraph {V : Type u_1} [DecidableEq V] (P : Finset (Finset V)) : (packingGraph P).edgeSet = ↑P.familyEdges

@[simp]

theorem SumZeroTriangles.edgeFinset_triangleGraph {V : Type u_1} [DecidableEq V] (t : Finset V) : (triangleGraph t).edgeFinset = t.innerEdges

@[simp]

theorem SumZeroTriangles.edgeFinset_packingGraph {V : Type u_1} [DecidableEq V] (P : Finset (Finset V)) : (packingGraph P).edgeFinset = P.familyEdges

theorem SumZeroTriangles.exists_simpleGraph_triangle_packing {V : Type u_1} [DecidableEq V] [Fintype V] : ∃ (P : Finset (Finset V)), (∀ t ∈ P, ⊤.IsNClique 3 t) ∧ (∀ t ∈ P, ∀ t' ∈ P, t ≠ t' → Disjoint (triangleGraph t) (triangleGraph t')) ∧ ∀ (v : V), (⊤ \ packingGraph P).degree v ≤ 3

Every finite complete graph has a packing by edge-disjoint triangles whose uncovered graph has maximum degree at most three.