The ten two-triangle inventories

def MacMahon.triple : Fin 10 → Finset Label

The ten unordered partitions, choosing the triple containing label 0.

Equations

• MacMahon.triple = ![{0, 1, 2}, {0, 1, 3}, {0, 1, 4}, {0, 1, 5}, {0, 2, 3}, {0, 2, 4}, {0, 2, 5}, {0, 3, 4}, {0, 3, 5}, {0, 4, 5}]

def MacMahon.twoTriangles (s : Finset Label) : Inventory

One copy of each directed edge within either triple.

Equations

• MacMahon.twoTriangles s p = if p.1 ≠ p.2 ∧ (p.1 ∈ s ∧ p.2 ∈ s ∨ p.1 ∉ s ∧ p.2 ∉ s) then 1 else 0

def MacMahon.winner (b : Fin 10) : Inventory

The ten candidates, defined structurally rather than by a matrix table.

Equations

• MacMahon.winner b = MacMahon.twoTriangles (MacMahon.triple b)

theorem MacMahon.triple_card (b : Fin 10) : (triple b).card = 3

theorem MacMahon.winner_two_triangles (b : Fin 10) : (triple b).card = 3 ∧ winner b = twoTriangles (triple b)

theorem MacMahon.partition_complete (s : Finset Label) : s.card = 3 → ∃ (b : Fin 10), twoTriangles s = winner b

theorem MacMahon.winners_iff_two_triangles (a : Inventory) : (∃ (b : Fin 10), a = winner b) ↔ ∃ (s : Finset Label), s.card = 3 ∧ a = twoTriangles s

theorem MacMahon.winner_properties (b : Fin 10) : DiagonalZero (winner b) ∧ total (winner b) = 12 ∧ ∀ (p : Pair), winner b p ≤ 1

theorem MacMahon.winners_distinct : Function.Injective winner