Necessary corner and inventory bounds

theorem MacMahon.builds_usable_bound (a : Inventory) (i j : Label) (hij : i ≠ j) (hb : Builds a (i, j)) : 8 ≤ usableCount a (i, j)

A genuine solution supplies at least eight usable physical cubes.

theorem MacMahon.universal_corner (a : Inventory) (h : Universal a) (c : Corner) : ∃ (p : Pair), HasCorner p c ∧ 0 < a p

Universality must supply every one of the forty corner types.

theorem MacMahon.universal_partition_cover (a : Inventory) (h : Universal a) (b : Fin 10) : 0 < ∑ p : Pair, winner b p * a p