Minimum universal collections of coloured cubes

theorem MacMahon.classification (a : Inventory) (hz : DiagonalZero a) (ht : total a = 12) : Universal a ↔ ∃ (b : Fin 10), a = winner b

Complete classification, including inventories with repeated physical cubes.

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

@[reducible, inline]

abbrev MacMahon.MinimumInventory : Type

Universal corner-matching inventories attaining size twelve.

Equations

• MacMahon.MinimumInventory = { a : MacMahon.Inventory // MacMahon.DiagonalZero a ∧ MacMahon.total a = 12 ∧ MacMahon.Universal a }

def MacMahon.minimumMap (b : Fin 10) : MinimumInventory

The minimum inventory supplied by one of the ten triple partitions.

Equations

• MacMahon.minimumMap b = ⟨MacMahon.winner b, ⋯⟩

noncomputable def MacMahon.minimumEquiv : Fin 10 ≃ MinimumInventory

Classify the labelled minimum inventories by the ten triple partitions.

Equations

• MacMahon.minimumEquiv = Equiv.ofBijective MacMahon.minimumMap MacMahon.minimumEquiv._proof_3

theorem MacMahon.exactly_ten : Nat.card MinimumInventory = 10

Exactly ten labelled minimum universal inventories exist.

theorem MacMahon.physical_minimum (a : Inventory) (hz : DiagonalZero a) (h : PhysicalUniversal a) : 12 ≤ total a

theorem MacMahon.physical_classification (a : Inventory) (hz : DiagonalZero a) (ht : total a = 12) : PhysicalUniversal a ↔ ∃ (b : Fin 10), a = winner b

theorem MacMahon.physical_iff_two_triangles (a : Inventory) (hz : DiagonalZero a) (ht : total a = 12) : PhysicalUniversal a ↔ ∃ (s : Finset Label), s.card = 3 ∧ a = twoTriangles s

The structural form of the classification: two disjoint triangles.

@[reducible, inline]

abbrev MacMahon.MinimumPhysicalInventory : Type

Physically universal inventories attaining size twelve.

Equations

• MacMahon.MinimumPhysicalInventory = { a : MacMahon.Inventory // MacMahon.DiagonalZero a ∧ MacMahon.total a = 12 ∧ MacMahon.PhysicalUniversal a }

theorem MacMahon.physical_exactly_ten : Nat.card MinimumPhysicalInventory = 10

theorem MacMahon.minimum_size : IsLeast {n : ℕ | ∃ (a : Inventory), DiagonalZero a ∧ PhysicalUniversal a ∧ total a = n} 12