Physical classification and geometric coverage

theorem MacMahon.physical_minimum_has_no_repeats (a : Inventory) (hz : DiagonalZero a) (ht : total a = 12) (h : PhysicalUniversal a) (p : Pair) : a p ≤ 1

The multiplicity conclusion expressed using physical face matching.

theorem MacMahon.face_assignment_coverage (f : Fin 6 → Fin 7) (hi : Function.Injective f) (hn : ∀ (d : Fin 6), f d ≠ 0) : ∃ (i : Label) (j : Label), i ≠ j ∧ ∃ (r : Fin 24), ∀ (d : Fin 6), f d = faceColours i j (rotations r d)

Every assignment of six distinct nonzero colours is represented by the tableau.

theorem MacMahon.face_assignment_unique (i j : Label) (hij : i ≠ j) (u v : Label) (huv : u ≠ v) (r s : Fin 24) (hf : ∀ (d : Fin 6), faceColours i j (rotations r d) = faceColours u v (rotations s d)) : i = u ∧ j = v ∧ r = s

The variety and rotation representing a face assignment are unique.