Sufficiency of the ten candidate inventories

theorem MacMahon.witness_facts (b : Fin 10) (i j : Label) : i ≠ j → Function.Injective (witness b i j) ∧ ∀ (k : Slot), winner b (witness b i j k) = 1 ∧ HasCorner (witness b i j k) (cornerAt i j k)

theorem MacMahon.winner_universal (b : Fin 10) : Universal (winner b)

Every known set has an explicit eight-cube construction for every target.