diff --git a/LeanPool/MacMahon.lean b/LeanPool/MacMahon.lean
new file mode 100644
index 0000000000..e57993c5a4
--- /dev/null
+++ b/LeanPool/MacMahon.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+module
+
+public import LeanPool.MacMahon.Submission
+
+/-!
+# The ten minimum universal collections of MacMahon cubes
+
+Source: url:https://github.com/jasondavies/macmahon-min-universal-sets/tree/d8856c97e43e6fa66383c81b8ac4f5bd1c285bc8
+Authors: Jason Davies
+Status: verified
+Main declarations: `MacMahon.minimum_size`, `MacMahon.physical_exactly_ten`
+Tags: combinatorics, coloured-cubes, classification, finite-geometry
+MSC: 05A15, 05C70, 68V15, 00A08
+-/
+
+/-!
+## Attribution
+
+Adapted for Lean Pool from Jason Davies's Apache-2.0 formalization at
+https://github.com/jasondavies/macmahon-min-universal-sets, commit
+`d8856c97e43e6fa66383c81b8ac4f5bd1c285bc8`. Module paths and proof engineering
+have been adapted for the pool. Proofs were primarily AI generated under the
+author's direction; see the upstream `formalization.yaml`.
+
+The original conjectures are Conjectures 4 and 8 of Inga Johnson and Erika Roldán,
+*Solution Numbers for Eight Blocks to Madness Puzzle* (arXiv:2407.13208v1).
+Kazuya Haraguchi proved the minimum size twelve (arXiv:1408.3696v2).
+The formalization uses finite signed-axis geometry. The upstream computational
+target-count histograms are not part of these Lean theorems.
+-/
diff --git a/LeanPool/MacMahon/Arithmetic.lean b/LeanPool/MacMahon/Arithmetic.lean
new file mode 100644
index 0000000000..f1f1720f2c
--- /dev/null
+++ b/LeanPool/MacMahon/Arithmetic.lean
@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Counting
+
+public import Mathlib.Algebra.BigOperators.Fin
+public import Mathlib.Data.Fintype.BigOperators
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.NormNum
+
+/-!
+# The minimum inventory size and tight degree bounds
+-/
+
+@[expose] public section
+namespace MacMahon
+open scoped BigOperators
+
+lemma usable_count_identity (a : Inventory) (hz : DiagonalZero a)
+    (i j : Label) (hij : i ≠ j) :
+    usableCount a (i, j) + row a i + col a j + a (j, i) = total a + 2 * a (i, j) := by
+  unfold usableCount
+  simp_rw [usable_rule i j hij]
+  simp only [DiagonalZero, Fin.forall_fin_succ] at hz
+  fin_cases i <;> fin_cases j <;>
+    norm_num [row, col, total, Fintype.sum_prod_type, Fin.sum_univ_succ] at * <;> omega
+
+lemma universal_pair_bound (a : Inventory) (hz : DiagonalZero a) (h : Universal a)
+    (i j : Label) (hij : i ≠ j) :
+    row a i + col a j + a (j, i) + 8 ≤ total a + 2 * a (i, j) := by
+  have := builds_usable_bound a i j hij (h i j hij)
+  have := usable_count_identity a hz i j hij
+  omega
+
+lemma total_rows (a : Inventory) : total a = ∑ i, row a i := by
+  simp [total, row, Fintype.sum_prod_type]
+lemma total_cols (a : Inventory) : total a = ∑ j, col a j := by
+  simp only [total, col, Fintype.sum_prod_type]
+  exact Finset.sum_comm
+
+lemma universal_row_bound (a : Inventory) (hz : DiagonalZero a) (h : Universal a)
+    (i : Label) : 3 * row a i + 40 ≤ 4 * total a := by
+  have hp := universal_pair_bound a hz h i
+  have ht := total_cols a
+  have hr : row a i = ∑ j, a (i, j) := rfl
+  have hc : col a i = ∑ j, a (j, i) := rfl
+  have hd := hz i
+  fin_cases i <;> norm_num [Fin.forall_fin_succ, Fin.sum_univ_succ] at * <;> omega
+
+lemma universal_col_bound (a : Inventory) (hz : DiagonalZero a) (h : Universal a)
+    (j : Label) : 3 * col a j + 40 ≤ 4 * total a := by
+  have hp : ∀ i : Label, i ≠ j →
+      row a i + col a j + a (j, i) + 8 ≤ total a + 2 * a (i, j) :=
+    fun i hij => universal_pair_bound a hz h i j hij
+  have ht := total_rows a
+  have hr : row a j = ∑ i, a (j, i) := rfl
+  have hc : col a j = ∑ i, a (i, j) := rfl
+  have hd := hz j
+  fin_cases j <;> norm_num [Fin.forall_fin_succ, Fin.sum_univ_succ] at * <;> omega
+
+theorem universal_minimum (a : Inventory) (hz : DiagonalZero a) (h : Universal a) :
+    12 ≤ total a := by
+  have hb := universal_row_bound a hz h
+  have ht := total_rows a
+  norm_num [Fin.forall_fin_succ, Fin.sum_univ_succ] at hb ht
+  omega
+
+/-- If a finite sum attains the sum of pointwise upper bounds, all bounds are tight. -/
+lemma eq_two_of_le_of_sum (f : Label → ℕ) (hb : ∀ i, f i ≤ 2)
+    (hs : ∑ i, f i = 12) : ∀ i, f i = 2 := by
+  have hh : (∑ i, f i) = ∑ _i : Label, 2 := by simpa using hs
+  intro i
+  exact (Finset.sum_eq_sum_iff_of_le (fun j _ => hb j)).mp hh i (Finset.mem_univ i)
+
+lemma rows_two (a : Inventory) (hz : DiagonalZero a) (h : Universal a)
+    (ht : total a = 12) : ∀ i, row a i = 2 := by
+  have hb : ∀ i, row a i ≤ 2 := by
+    intro i
+    have := universal_row_bound a hz h i
+    omega
+  exact eq_two_of_le_of_sum (row a) hb ((total_rows a).symm.trans ht)
+
+lemma cols_two (a : Inventory) (hz : DiagonalZero a) (h : Universal a)
+    (ht : total a = 12) : ∀ i, col a i = 2 := by
+  have hb : ∀ i, col a i ≤ 2 := by
+    intro i
+    have := universal_col_bound a hz h i
+    omega
+  exact eq_two_of_le_of_sum (col a) hb ((total_cols a).symm.trans ht)
+
+lemma reverse_bound (a : Inventory) (hz : DiagonalZero a) (h : Universal a)
+    (ht : total a = 12) : ∀ i j, a (j, i) ≤ 2 * a (i, j) := by
+  intro i j
+  by_cases hij : i = j
+  · subst j; omega
+  have := universal_pair_bound a hz h i j hij
+  rw [rows_two a hz h ht i, cols_two a hz h ht j, ht] at this
+  omega
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Classification.lean b/LeanPool/MacMahon/Classification.lean
new file mode 100644
index 0000000000..dff8d0e119
--- /dev/null
+++ b/LeanPool/MacMahon/Classification.lean
@@ -0,0 +1,182 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Structure
+public import LeanPool.MacMahon.Partitions
+
+public import Mathlib.Logic.Equiv.Fintype
+public import Mathlib.Tactic.FinCases
+public import Mathlib.Tactic.NormNum
+
+public import Mathlib.Algebra.BigOperators.Fin
+public import Mathlib.Data.Fintype.BigOperators
+
+/-!
+# Classification of minimum universal inventories
+-/
+
+@[expose] public section
+namespace MacMahon
+open scoped BigOperators
+
+/-!
+The first row of a symmetric degree-two inventory has either one doubled edge
+or two distinct neighbours. Relabel these to 01 or to 01 and 02. The ten
+partition-cover inequalities exclude the doubled edge and force 12 in the
+second case. The degree equations then force the two triangles completely.
+-/
+
+/-- Pull an inventory back along a permutation of the tableau labels. -/
+def relabel (e : Equiv.Perm Label) (a : Inventory) : Inventory :=
+  fun p => a (e p.1, e p.2)
+
+lemma row_relabel (e : Equiv.Perm Label) (a : Inventory) (i : Label) :
+    row (relabel e a) i = row a (e i) :=
+  Equiv.sum_comp e (fun j => a (e i, j))
+
+lemma partition_sum_relabel (e : Equiv.Perm Label) (a : Inventory) (s : Finset Label) :
+    (∑ p, twoTriangles s p * relabel e a p) =
+      ∑ p, twoTriangles (s.map e.toEmbedding) p * a p := by
+  rw [← (e.prodCongr e).sum_comp (fun p => twoTriangles (s.map e.toEmbedding) p * a p)]
+  apply Finset.sum_congr rfl
+  intro p _
+  simp [twoTriangles, relabel, Prod.map]
+
+lemma partition_cover_relabel (e : Equiv.Perm Label) (a : Inventory)
+    (hp : ∀ b : Fin 10, 0 < ∑ p : Pair, winner b p * a p) :
+    ∀ b : Fin 10, 0 < ∑ p : Pair, winner b p * relabel e a p := by
+  intro b
+  obtain ⟨c, hc⟩ := partition_complete ((triple b).map e.toEmbedding)
+    (by simp [(winner_two_triangles b).1])
+  change 0 < ∑ p, twoTriangles (triple b) p * relabel e a p
+  rw [partition_sum_relabel, hc]
+  exact hp c
+
+private lemma row_shape (f : Label → ℕ) (hz : f 0 = 0) (hs : ∑ i, f i = 2) :
+    (∃ i, i ≠ 0 ∧ f i = 2) ∨
+    (∃ i j, i ≠ 0 ∧ j ≠ 0 ∧ i ≠ j ∧ f i = 1 ∧ f j = 1) := by
+  obtain ⟨i, _, hi⟩ := Finset.sum_pos_iff.mp (show 0 < ∑ i, f i by omega)
+  have hi0 : i ≠ 0 := by rintro rfl; omega
+  have hib : f i ≤ 2 := by
+    calc f i ≤ ∑ j, f j := Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i)
+         _ = 2 := hs
+  by_cases hi2 : f i = 2
+  · exact Or.inl ⟨i, hi0, hi2⟩
+  have hi1 : f i = 1 := by omega
+  have hrest : ∑ j ∈ Finset.univ.erase i, f j = 1 := by
+    have := Finset.sum_erase_add (Finset.univ) f (Finset.mem_univ i)
+    omega
+  obtain ⟨j, hj, hjp⟩ := Finset.sum_pos_iff.mp
+    (show 0 < ∑ j ∈ Finset.univ.erase i, f j by omega)
+  have hj0 : j ≠ 0 := by rintro rfl; omega
+  have hjb : f j ≤ 1 := by
+    calc f j ≤ ∑ k ∈ Finset.univ.erase i, f k :=
+           Finset.single_le_sum (fun _ _ => Nat.zero_le _) hj
+         _ = 1 := hrest
+  exact Or.inr ⟨i, j, hi0, hj0, (Finset.mem_erase.mp hj).1.symm, hi1, by omega⟩
+
+/-- Partition cover excludes a doubled edge at the normalized position 01. -/
+lemma no_normalized_doubled_edge (a : Inventory) (hz : DiagonalZero a)
+    (hr : ∀ i, row a i = 2) (hs : ∀ i j, a (i, j) = a (j, i))
+    (hp : ∀ b : Fin 10, 0 < ∑ p : Pair, winner b p * a p) : a (0, 1) ≠ 2 := by
+  norm_num [DiagonalZero, row, Fin.forall_fin_succ, Fin.sum_univ_succ] at hz hr hs
+  norm_num [Fin.forall_fin_succ, winner, twoTriangles, triple,
+    Fintype.sum_prod_type, Fin.sum_univ_succ, -add_pos_iff] at hp
+  omega
+
+/-- Two unit edges from 0 must close to the triangle on labels 0, 1 and 2. -/
+lemma normalized_triangle_closes (a : Inventory) (hz : DiagonalZero a)
+    (hr : ∀ i, row a i = 2) (hs : ∀ i j, a (i, j) = a (j, i))
+    (hp : ∀ b : Fin 10, 0 < ∑ p : Pair, winner b p * a p)
+    (h01 : a (0, 1) = 1) (h02 : a (0, 2) = 1) : a (1, 2) = 1 := by
+  norm_num [DiagonalZero, row, Fin.forall_fin_succ, Fin.sum_univ_succ] at hz hr hs
+  norm_num [Fin.forall_fin_succ, winner, twoTriangles, triple,
+    Fintype.sum_prod_type, Fin.sum_univ_succ, -add_pos_iff] at hp
+  omega
+
+private lemma winner_zero_matrix : ∀ i j : Label, winner 0 (i, j) =
+    ![![0, 1, 1, 0, 0, 0], ![1, 0, 1, 0, 0, 0], ![1, 1, 0, 0, 0, 0],
+      ![0, 0, 0, 0, 1, 1], ![0, 0, 0, 1, 0, 1], ![0, 0, 0, 1, 1, 0]] i j := by
+  decide +kernel
+
+/-- Two local configurations suffice after permuting the labels. -/
+private lemma classify_normalized (a : Inventory) (hz : DiagonalZero a)
+    (hr : ∀ i, row a i = 2) (hs : ∀ i j, a (i, j) = a (j, i))
+    (hp : ∀ b : Fin 10, 0 < ∑ p : Pair, winner b p * a p)
+    (hn : a (0, 1) = 2 ∨ (a (0, 1) = 1 ∧ a (0, 2) = 1)) : a = winner 0 := by
+  rcases hn with hdouble | ⟨h01, h02⟩
+  · exact (no_normalized_doubled_edge a hz hr hs hp hdouble).elim
+  have h12 := normalized_triangle_closes a hz hr hs hp h01 h02
+  clear hp
+  have hrow := hr
+  have hsym := hs
+  have r0 := row_eq_of_two_unit_entries a 0 1 2 (by decide) (hr 0) h01 h02
+  have r1 := row_eq_of_two_unit_entries a 1 0 2 (by decide) (hr 1)
+    ((hs 1 0).trans h01) h12
+  have r2 := row_eq_of_two_unit_entries a 2 0 1 (by decide) (hr 2)
+    ((hs 2 0).trans h02) ((hs 2 1).trans h12)
+  norm_num [DiagonalZero, row, Fin.forall_fin_succ, Fin.sum_univ_succ] at hz hr hs
+  have hzero : a (0, 3) = 0 ∧ a (0, 4) = 0 ∧ a (0, 5) = 0 ∧
+      a (1, 3) = 0 ∧ a (1, 4) = 0 ∧ a (1, 5) = 0 ∧
+      a (2, 3) = 0 ∧ a (2, 4) = 0 ∧ a (2, 5) = 0 := by omega
+  have hone : a (3, 4) = 1 ∧ a (3, 5) = 1 ∧ a (4, 5) = 1 := by omega
+  obtain ⟨h34, h35, h45⟩ := hone
+  have r3 := row_eq_of_two_unit_entries a 3 4 5 (by decide) (hrow 3) h34 h35
+  have r4 := row_eq_of_two_unit_entries a 4 3 5 (by decide) (hrow 4)
+    ((hsym 4 3).trans h34) h45
+  have r5 := row_eq_of_two_unit_entries a 5 3 4 (by decide) (hrow 5)
+    ((hsym 5 3).trans h35) ((hsym 5 4).trans h45)
+  funext ⟨i, j⟩
+  rw [winner_zero_matrix]
+  fin_cases i
+  · fin_cases j <;> exact r0 _
+  · fin_cases j <;> exact r1 _
+  · fin_cases j <;> exact r2 _
+  · fin_cases j <;> exact r3 _
+  · fin_cases j <;> exact r4 _
+  · fin_cases j <;> exact r5 _
+
+/-- Complete classification using two local configurations, up to relabelling. -/
+lemma classify_degree_two (a : Inventory) (hz : DiagonalZero a)
+    (hr : ∀ i, row a i = 2) (hs : ∀ i j, a (i, j) = a (j, i))
+    (hp : ∀ b : Fin 10, 0 < ∑ p : Pair, winner b p * a p) :
+    ∃ b : Fin 10, a = winner b := by
+  suffices he : ∃ e : Equiv.Perm Label, relabel e a = winner 0 by
+    obtain ⟨e, he⟩ := he
+    apply (winners_iff_two_triangles a).mpr
+    refine ⟨(triple 0).map e.toEmbedding, by simp [(winner_two_triangles 0).1], ?_⟩
+    funext p
+    have hh := congrFun he (e.symm p.1, e.symm p.2)
+    simpa [relabel, winner, twoTriangles] using hh
+  have normalize (e : Equiv.Perm Label)
+      (hn : relabel e a (0, 1) = 2 ∨
+        (relabel e a (0, 1) = 1 ∧ relabel e a (0, 2) = 1)) :
+      relabel e a = winner 0 :=
+    classify_normalized (relabel e a) (fun i => hz (e i))
+      (fun i => (row_relabel e a i).trans (hr (e i)))
+      (fun i j => hs (e i) (e j)) (partition_cover_relabel e a hp) hn
+  rcases row_shape (fun j => a (0, j)) (hz 0) (hr 0) with
+    ⟨i, hi0, hi⟩ | ⟨i, j, hi0, hj0, hij, hi, hj⟩
+  · let e : Equiv.Perm Label := Equiv.swap 1 i
+    have he0 : e 0 = 0 := Equiv.swap_apply_of_ne_of_ne (by decide) hi0.symm
+    refine ⟨e, normalize e (Or.inl ?_)⟩
+    simpa [relabel, he0, e] using hi
+  · let f : Fin 3 → Label := ![0, 1, 2]
+    let g : Fin 3 → Label := ![0, i, j]
+    have hf : Function.Injective f := by decide +kernel
+    have hg : Function.Injective g := by
+      simp [Function.Injective, Fin.forall_fin_succ, g,
+        hi0, hj0, hij, hi0.symm, hj0.symm, hij.symm]
+    obtain ⟨e, he⟩ := Equiv.Perm.exists_extending_pair f g hf hg
+    have he0 : e 0 = 0 := he 0
+    have he1 : e 1 = i := he 1
+    have he2 : e 2 = j := he 2
+    refine ⟨e, normalize e (Or.inr ?_)⟩
+    simpa [relabel, he0, he1, he2] using And.intro hi hj
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Colourings.lean b/LeanPool/MacMahon/Colourings.lean
new file mode 100644
index 0000000000..a3234ad6ff
--- /dev/null
+++ b/LeanPool/MacMahon/Colourings.lean
@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Rotations
+
+public import Mathlib.Data.Fintype.Perm
+public import Mathlib.Tactic.NormNum
+
+/-!
+# Completeness of the six-colour cube varieties
+-/
+
+@[expose] public section
+namespace MacMahon
+
+/-- The six physical face colours; zero is reserved for invalid tableau entries. -/
+abbrev NonzeroColour := {c : Fin 7 // c ≠ 0}
+/-- Identify the six indices with the six nonzero face colours. -/
+def colourEquiv : Fin 6 ≃ NonzeroColour where
+  toFun i := ⟨i.succ, i.succ_ne_zero⟩
+  invFun c := c.val.pred c.property
+  left_inv i := Fin.pred_succ i
+  right_inv c := Subtype.ext (Fin.succ_pred c.val c.property)
+
+/-- Arbitrary assignments using each of the six colours exactly once. -/
+abbrev Colouring := Fin 6 ≃ NonzeroColour
+/-- The thirty off-diagonal entries of Conway's tableau. -/
+abbrev Variety := {p : Pair // p.1 ≠ p.2}
+
+/-- The face colouring of a tableau variety after a proper rotation. -/
+noncomputable def orientedColouring (p : Variety × Fin 24) : Colouring :=
+  Equiv.ofBijective
+    (fun f => ⟨faceColours p.1.val.1 p.1.val.2 (rotations p.2 f),
+      (face_colours_valid _ _ p.1.property).2 _⟩)
+    ((Fintype.bijective_iff_injective_and_card _).mpr ⟨by
+      intro f g h
+      exact (rotations_bijective p.2).1
+        ((face_colours_valid _ _ p.1.property).1 (congrArg Subtype.val h)),
+      Fintype.card_congr colourEquiv⟩)
+
+lemma orientedColouring_injective : Function.Injective orientedColouring := by
+  rintro ⟨⟨⟨i, j⟩, hij⟩, r⟩ ⟨⟨⟨u, v⟩, huv⟩, s⟩ heq
+  have hf : ∀ f : Fin 6, faceColours i j (rotations r f) =
+      faceColours u v (rotations s f) :=
+    fun f => congrArg (fun e : Colouring => (e f).val) heq
+  obtain ⟨si, hsi⟩ := rotation_inverse s
+  obtain ⟨t, ht⟩ := rotation_composition r si
+  have hvar : i = u ∧ j = v := varieties_distinct i j hij u v huv t (by
+    intro f
+    rw [ht f]
+    have hh := hf (rotations si f)
+    rwa [hsi f] at hh)
+  obtain ⟨rfl, rfl⟩ := hvar
+  have hrs : r = s := rotations_distinct (funext (fun f =>
+    (face_colours_valid _ _ hij).1 (hf f)))
+  subst s
+  rfl
+
+lemma card_variety : Fintype.card Variety = 30 := by decide +kernel
+lemma card_colourings : Fintype.card Colouring = 720 := by
+  rw [Fintype.card_equiv colourEquiv]
+  norm_num [Nat.factorial]
+
+/-- Every six-colour face assignment has a unique labelled variety and rotation. -/
+theorem all_colourings : Function.Bijective orientedColouring := by
+  apply (Fintype.bijective_iff_injective_and_card _).mpr
+  refine ⟨orientedColouring_injective, ?_⟩
+  rw [Fintype.card_prod, card_variety, Fintype.card_fin, card_colourings]
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Counting.lean b/LeanPool/MacMahon/Counting.lean
new file mode 100644
index 0000000000..c4ad2a2bb1
--- /dev/null
+++ b/LeanPool/MacMahon/Counting.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Incidence
+
+public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
+public import Mathlib.Data.Fintype.Card
+
+public import Mathlib.Data.Fintype.Sigma
+public import Mathlib.Data.Fintype.BigOperators
+public import Mathlib.Algebra.Order.BigOperators.Group.Finset
+
+/-!
+# Necessary corner and inventory bounds
+-/
+
+@[expose] public section
+namespace MacMahon
+open scoped BigOperators
+
+/-- A genuine solution supplies at least eight usable physical cubes. -/
+theorem builds_usable_bound (a : Inventory) (i j : Label) (hij : i ≠ j)
+    (hb : Builds a (i, j)) : 8 ≤ usableCount a (i, j) := by
+  obtain ⟨f, hf⟩ := hb
+  let U := {p : Pair // Usable (i, j) p}
+  let g : Slot → ((p : U) × Fin (a p.1)) := fun k =>
+    ⟨⟨(f k).1, ⟨cornerAt i j k, cornerAt_mem i j hij k, hf k⟩⟩, (f k).2⟩
+  have hg : Function.Injective g := by
+    intro k l h
+    apply f.injective
+    exact congrArg (fun z : ((p : U) × Fin (a p.1)) => (⟨z.1.1, z.2⟩ : Stock a)) h
+  have hc := Fintype.card_le_of_injective g hg
+  simp only [Fintype.card_fin, Fintype.card_sigma] at hc
+  change 8 ≤ ∑ p : U, a p.1 at hc
+  have hs : (∑ p : U, a p.1) = usableCount a (i, j) := by
+    rw [← Finset.sum_subtype (Finset.univ.filter (Usable (i, j))) (by simp)]
+    simp [usableCount, Finset.sum_filter]
+  exact hs ▸ hc
+
+/-- Universality must supply every one of the forty corner types. -/
+theorem universal_corner (a : Inventory) (h : Universal a) (c : Corner) :
+    ∃ p : Pair, HasCorner p c ∧ 0 < a p := by
+  obtain ⟨i, j, hij, k, hk⟩ := every_corner c
+  obtain ⟨f, hf⟩ := h i j hij
+  refine ⟨(f k).1, ?_, Nat.zero_lt_of_lt (f k).2.isLt⟩
+  simpa [hk] using hf k
+
+theorem universal_partition_cover (a : Inventory) (h : Universal a) (b : Fin 10) :
+    0 < ∑ p : Pair, winner b p * a p := by
+  obtain ⟨p, hp, ha⟩ := universal_corner a h (partitionCorner b)
+  have hw := partition_corner_support b p hp
+  have hs : winner b p * a p ≤ ∑ q : Pair, winner b q * a q :=
+    Finset.single_le_sum (f := fun q => winner b q * a q) (fun _ _ => Nat.zero_le _)
+      (Finset.mem_univ p)
+  have hpos : 0 < winner b p * a p := by simpa only [hw, one_mul] using ha
+  exact lt_of_lt_of_le hpos hs
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Data.lean b/LeanPool/MacMahon/Data.lean
new file mode 100644
index 0000000000..79780c3e82
--- /dev/null
+++ b/LeanPool/MacMahon/Data.lean
@@ -0,0 +1,218 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Types
+
+/-!
+# Geometric tables for the thirty cube varieties
+-/
+
+@[expose] public section
+-- Generated upstream by scripts/generate_lean_data.py at the pinned source revision.
+-- Numeric entries are unchanged; see the source card in LeanPool.MacMahon.
+namespace MacMahon
+/-- The oriented corner exposed at a position of a target variety. -/
+def cornerAt : Label → Label → Slot → Corner :=
+  ![
+    ![
+      ![0, 0, 0, 0, 0, 0, 0, 0],
+      ![3, 4, 18, 9, 28, 21, 39, 32],
+      ![2, 8, 13, 5, 31, 25, 35, 36],
+      ![0, 12, 7, 19, 23, 27, 33, 38],
+      ![1, 16, 10, 15, 20, 29, 34, 37],
+      ![6, 17, 14, 11, 26, 22, 24, 30]
+    ],
+    ![
+      ![0, 16, 5, 11, 26, 31, 34, 38],
+      ![0, 0, 0, 0, 0, 0, 0, 0],
+      ![7, 9, 19, 14, 29, 20, 28, 24],
+      ![1, 4, 10, 13, 30, 22, 39, 35],
+      ![3, 12, 17, 6, 25, 27, 36, 32],
+      ![2, 8, 15, 18, 21, 23, 37, 33]
+    ],
+    ![
+      ![1, 12, 9, 6, 30, 28, 33, 37],
+      ![5, 17, 10, 15, 23, 22, 27, 31],
+      ![0, 0, 0, 0, 0, 0, 0, 0],
+      ![2, 16, 14, 11, 21, 29, 32, 36],
+      ![0, 8, 7, 18, 26, 24, 35, 39],
+      ![3, 4, 19, 13, 25, 20, 38, 34]
+    ],
+    ![
+      ![2, 4, 15, 17, 24, 20, 39, 36],
+      ![0, 8, 6, 14, 29, 25, 37, 38],
+      ![3, 12, 18, 10, 22, 26, 33, 34],
+      ![0, 0, 0, 0, 0, 0, 0, 0],
+      ![5, 13, 11, 19, 23, 21, 30, 28],
+      ![1, 16, 9, 7, 27, 31, 32, 35]
+    ],
+    ![
+      ![3, 8, 19, 14, 22, 23, 35, 32],
+      ![2, 16, 13, 7, 24, 30, 34, 33],
+      ![1, 4, 11, 17, 27, 21, 38, 37],
+      ![6, 9, 15, 18, 26, 20, 31, 25],
+      ![0, 0, 0, 0, 0, 0, 0, 0],
+      ![0, 12, 5, 10, 29, 28, 36, 39]
+    ],
+    ![
+      ![7, 13, 18, 10, 29, 21, 25, 27],
+      ![1, 12, 11, 19, 20, 26, 36, 35],
+      ![0, 16, 6, 15, 23, 30, 32, 39],
+      ![3, 8, 17, 5, 28, 24, 37, 34],
+      ![2, 4, 14, 9, 31, 22, 38, 33],
+      ![0, 0, 0, 0, 0, 0, 0, 0]
+    ]
+  ]
+/-- The eight oriented corners of each valid variety; diagonal entries are empty. -/
+def cornerList : Label → Label → List Corner :=
+  ![
+    ![
+      [],
+      [3, 4, 9, 18, 21, 28, 32, 39],
+      [2, 5, 8, 13, 25, 31, 35, 36],
+      [0, 7, 12, 19, 23, 27, 33, 38],
+      [1, 10, 15, 16, 20, 29, 34, 37],
+      [6, 11, 14, 17, 22, 24, 26, 30]
+    ],
+    ![
+      [0, 5, 11, 16, 26, 31, 34, 38],
+      [],
+      [7, 9, 14, 19, 20, 24, 28, 29],
+      [1, 4, 10, 13, 22, 30, 35, 39],
+      [3, 6, 12, 17, 25, 27, 32, 36],
+      [2, 8, 15, 18, 21, 23, 33, 37]
+    ],
+    ![
+      [1, 6, 9, 12, 28, 30, 33, 37],
+      [5, 10, 15, 17, 22, 23, 27, 31],
+      [],
+      [2, 11, 14, 16, 21, 29, 32, 36],
+      [0, 7, 8, 18, 24, 26, 35, 39],
+      [3, 4, 13, 19, 20, 25, 34, 38]
+    ],
+    ![
+      [2, 4, 15, 17, 20, 24, 36, 39],
+      [0, 6, 8, 14, 25, 29, 37, 38],
+      [3, 10, 12, 18, 22, 26, 33, 34],
+      [],
+      [5, 11, 13, 19, 21, 23, 28, 30],
+      [1, 7, 9, 16, 27, 31, 32, 35]
+    ],
+    ![
+      [3, 8, 14, 19, 22, 23, 32, 35],
+      [2, 7, 13, 16, 24, 30, 33, 34],
+      [1, 4, 11, 17, 21, 27, 37, 38],
+      [6, 9, 15, 18, 20, 25, 26, 31],
+      [],
+      [0, 5, 10, 12, 28, 29, 36, 39]
+    ],
+    ![
+      [7, 10, 13, 18, 21, 25, 27, 29],
+      [1, 11, 12, 19, 20, 26, 35, 36],
+      [0, 6, 15, 16, 23, 30, 32, 39],
+      [3, 5, 8, 17, 24, 28, 34, 37],
+      [2, 4, 9, 14, 22, 31, 33, 38],
+      []
+    ]
+  ]
+/-- Face colours of the tableau representatives, with zero placeholders on the diagonal. -/
+def faceColours : Label → Label → Fin 6 → Fin 7 :=
+  ![
+    ![
+      ![0, 0, 0, 0, 0, 0],
+      ![1, 5, 2, 4, 6, 3],
+      ![1, 6, 2, 3, 5, 4],
+      ![1, 4, 2, 6, 3, 5],
+      ![1, 3, 2, 5, 4, 6],
+      ![1, 2, 3, 4, 5, 6]
+    ],
+    ![
+      ![1, 5, 2, 4, 3, 6],
+      ![0, 0, 0, 0, 0, 0],
+      ![1, 2, 3, 5, 6, 4],
+      ![1, 6, 2, 5, 4, 3],
+      ![1, 4, 2, 3, 6, 5],
+      ![1, 3, 2, 6, 5, 4]
+    ],
+    ![
+      ![1, 6, 2, 3, 4, 5],
+      ![1, 2, 3, 5, 4, 6],
+      ![0, 0, 0, 0, 0, 0],
+      ![1, 3, 2, 4, 5, 6],
+      ![1, 5, 2, 6, 3, 4],
+      ![1, 4, 2, 5, 6, 3]
+    ],
+    ![
+      ![1, 4, 2, 6, 5, 3],
+      ![1, 6, 2, 5, 3, 4],
+      ![1, 3, 2, 4, 6, 5],
+      ![0, 0, 0, 0, 0, 0],
+      ![1, 2, 3, 6, 4, 5],
+      ![1, 5, 2, 3, 4, 6]
+    ],
+    ![
+      ![1, 3, 2, 5, 6, 4],
+      ![1, 4, 2, 3, 5, 6],
+      ![1, 5, 2, 6, 4, 3],
+      ![1, 2, 3, 6, 5, 4],
+      ![0, 0, 0, 0, 0, 0],
+      ![1, 6, 2, 4, 3, 5]
+    ],
+    ![
+      ![1, 2, 3, 4, 6, 5],
+      ![1, 3, 2, 6, 4, 5],
+      ![1, 4, 2, 5, 3, 6],
+      ![1, 5, 2, 3, 6, 4],
+      ![1, 6, 2, 4, 5, 3],
+      ![0, 0, 0, 0, 0, 0]
+    ]
+  ]
+/-- The three outward coordinate faces at each assembly position. -/
+def exposedFaces : Slot → Fin 3 → Fin 6 :=
+  ![
+    ![0, 2, 4],
+    ![0, 2, 5],
+    ![0, 3, 4],
+    ![0, 3, 5],
+    ![1, 2, 4],
+    ![1, 2, 5],
+    ![1, 3, 4],
+    ![1, 3, 5]
+  ]
+/-- The twenty-four proper rotations as permutations of the six coordinate face directions. -/
+def rotations : Fin 24 → Fin 6 → Fin 6 :=
+  ![
+    ![0, 1, 2, 3, 4, 5],
+    ![0, 1, 3, 2, 5, 4],
+    ![0, 1, 4, 5, 3, 2],
+    ![0, 1, 5, 4, 2, 3],
+    ![1, 0, 2, 3, 5, 4],
+    ![1, 0, 3, 2, 4, 5],
+    ![1, 0, 4, 5, 2, 3],
+    ![1, 0, 5, 4, 3, 2],
+    ![2, 3, 0, 1, 5, 4],
+    ![2, 3, 1, 0, 4, 5],
+    ![2, 3, 4, 5, 0, 1],
+    ![2, 3, 5, 4, 1, 0],
+    ![3, 2, 0, 1, 4, 5],
+    ![3, 2, 1, 0, 5, 4],
+    ![3, 2, 4, 5, 1, 0],
+    ![3, 2, 5, 4, 0, 1],
+    ![4, 5, 0, 1, 2, 3],
+    ![4, 5, 1, 0, 3, 2],
+    ![4, 5, 2, 3, 1, 0],
+    ![4, 5, 3, 2, 0, 1],
+    ![5, 4, 0, 1, 3, 2],
+    ![5, 4, 1, 0, 2, 3],
+    ![5, 4, 2, 3, 0, 1],
+    ![5, 4, 3, 2, 1, 0]
+  ]
+/-- A distinguished corner used in the covering obstruction for a triple partition. -/
+def partitionCorner : Fin 10 → Corner :=
+  ![5, 0, 3, 11, 2, 1, 6, 15, 7, 10]
+end MacMahon
diff --git a/LeanPool/MacMahon/Definitions.lean b/LeanPool/MacMahon/Definitions.lean
new file mode 100644
index 0000000000..c52e7aa8ea
--- /dev/null
+++ b/LeanPool/MacMahon/Definitions.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Data
+
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+
+/-!
+# Inventories and physical constructions
+-/
+
+@[expose] public section
+
+namespace MacMahon
+open scoped BigOperators
+
+/-- A variety offers a specified oriented corner. -/
+def HasCorner (p : Pair) (c : Corner) : Prop := c ∈ cornerList p.1 p.2
+instance (p : Pair) (c : Corner) : Decidable (HasCorner p c) :=
+  inferInstanceAs (Decidable (c ∈ cornerList p.1 p.2))
+/-- A physical cube shares at least one oriented corner with the target variety. -/
+def Usable (t p : Pair) : Prop := ∃ c : Corner, HasCorner t c ∧ HasCorner p c
+instance (t p : Pair) : Decidable (Usable t p) :=
+  inferInstanceAs (Decidable (∃ c : Corner, HasCorner t c ∧ HasCorner p c))
+
+/-- After a specified proper rotation, a cube matches the target on all three outward faces. -/
+def FaceFits (t p : Pair) (k : Slot) (r : Fin 24) : Prop :=
+  ∀ f : Fin 3, faceColours p.1 p.2 (rotations r (exposedFaces k f)) =
+    faceColours t.1 t.2 (exposedFaces k f)
+instance (t p : Pair) (k : Slot) (r : Fin 24) : Decidable (FaceFits t p k r) :=
+  inferInstanceAs (Decidable (∀ f : Fin 3,
+    faceColours p.1 p.2 (rotations r (exposedFaces k f)) =
+      faceColours t.1 t.2 (exposedFaces k f)))
+
+/-- Distinct physical copies of the varieties with the prescribed multiplicities. -/
+abbrev Stock (a : Inventory) := (p : Pair) × Fin (a p)
+/-- An injective allocation of eight physical copies matching the target corners. -/
+def Builds (a : Inventory) (t : Pair) : Prop :=
+  ∃ f : Slot ↪ Stock a, ∀ k, HasCorner (f k).1 (cornerAt t.1 t.2 k)
+/-- Eight distinct cubes with proper rotations matching all outward target faces. -/
+def PhysicalBuilds (a : Inventory) (t : Pair) : Prop :=
+  ∃ f : Slot ↪ Stock a, ∀ k, ∃ r : Fin 24, FaceFits t (f k).1 k r
+/-- Every valid target variety admits a physical assembly from the inventory. -/
+def PhysicalUniversal (a : Inventory) : Prop :=
+  ∀ i j : Label, i ≠ j → PhysicalBuilds a (i, j)
+/-- Every valid target variety admits a corner-matching assembly from the inventory. -/
+def Universal (a : Inventory) : Prop := ∀ i j : Label, i ≠ j → Builds a (i, j)
+/-- The invalid diagonal tableau entries have zero multiplicity. -/
+def DiagonalZero (a : Inventory) : Prop := ∀ i : Label, a (i, i) = 0
+/-- The number of physical cubes in an inventory. -/
+def total (a : Inventory) : ℕ := ∑ p, a p
+/-- The total multiplicity in a fixed Conway tableau row. -/
+def row (a : Inventory) (i : Label) : ℕ := ∑ j, a (i, j)
+/-- The total multiplicity in a fixed Conway tableau column. -/
+def col (a : Inventory) (j : Label) : ℕ := ∑ i, a (i, j)
+/-- The number of physical copies sharing a corner with a given target. -/
+def usableCount (a : Inventory) (t : Pair) : ℕ :=
+  ∑ p : Pair, if Usable t p then a p else 0
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Geometry.lean b/LeanPool/MacMahon/Geometry.lean
new file mode 100644
index 0000000000..347cb72957
--- /dev/null
+++ b/LeanPool/MacMahon/Geometry.lean
@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Geometry.TargetZero
+public import LeanPool.MacMahon.Geometry.TargetOne
+public import LeanPool.MacMahon.Geometry.TargetTwo
+public import LeanPool.MacMahon.Geometry.TargetThree
+public import LeanPool.MacMahon.Geometry.TargetFour
+public import LeanPool.MacMahon.Geometry.TargetFive
+
+public import Mathlib.Tactic.FinCases
+
+/-!
+# Equivalence of physical faces and corner matching
+-/
+
+@[expose] public section
+namespace MacMahon
+
+theorem face_corner_equivalence : ∀ i j : Label, i ≠ j → ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt i j k) ↔ ∃ r : Fin 24, FaceFits (i, j) p k r := by
+  intro i j hij
+  fin_cases i <;> fin_cases j
+  · exact (hij rfl).elim
+  · exact face_corner_01
+  · exact face_corner_02
+  · exact face_corner_03
+  · exact face_corner_04
+  · exact face_corner_05
+  · exact face_corner_10
+  · exact (hij rfl).elim
+  · exact face_corner_12
+  · exact face_corner_13
+  · exact face_corner_14
+  · exact face_corner_15
+  · exact face_corner_20
+  · exact face_corner_21
+  · exact (hij rfl).elim
+  · exact face_corner_23
+  · exact face_corner_24
+  · exact face_corner_25
+  · exact face_corner_30
+  · exact face_corner_31
+  · exact face_corner_32
+  · exact (hij rfl).elim
+  · exact face_corner_34
+  · exact face_corner_35
+  · exact face_corner_40
+  · exact face_corner_41
+  · exact face_corner_42
+  · exact face_corner_43
+  · exact (hij rfl).elim
+  · exact face_corner_45
+  · exact face_corner_50
+  · exact face_corner_51
+  · exact face_corner_52
+  · exact face_corner_53
+  · exact face_corner_54
+  · exact (hij rfl).elim
+
+/-- Corner matching is exactly matching the exposed faces by proper rotations. -/
+theorem builds_iff_physical (a : Inventory) (i j : Label) (h : i ≠ j) :
+    Builds a (i, j) ↔ PhysicalBuilds a (i, j) := by
+  constructor <;> rintro ⟨f, hf⟩ <;> refine ⟨f, ?_⟩ <;> intro k
+  · exact (face_corner_equivalence i j h (f k).1 k).mp (hf k)
+  · exact (face_corner_equivalence i j h (f k).1 k).mpr (hf k)
+
+theorem universal_iff_physical (a : Inventory) : Universal a ↔ PhysicalUniversal a := by
+  constructor <;> intro h i j hij
+  · exact (builds_iff_physical a i j hij).mp (h i j hij)
+  · exact (builds_iff_physical a i j hij).mpr (h i j hij)
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Geometry/TargetFive.lean b/LeanPool/MacMahon/Geometry/TargetFive.lean
new file mode 100644
index 0000000000..06f282c21b
--- /dev/null
+++ b/LeanPool/MacMahon/Geometry/TargetFive.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Definitions
+
+/-!
+# Face and corner matching for targets in tableau row 5
+-/
+
+@[expose] public section
+
+namespace MacMahon
+
+theorem face_corner_50 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 5 0 k) ↔ ∃ r : Fin 24, FaceFits (5, 0) p k r := by
+  decide +kernel
+
+theorem face_corner_51 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 5 1 k) ↔ ∃ r : Fin 24, FaceFits (5, 1) p k r := by
+  decide +kernel
+
+theorem face_corner_52 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 5 2 k) ↔ ∃ r : Fin 24, FaceFits (5, 2) p k r := by
+  decide +kernel
+
+theorem face_corner_53 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 5 3 k) ↔ ∃ r : Fin 24, FaceFits (5, 3) p k r := by
+  decide +kernel
+
+theorem face_corner_54 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 5 4 k) ↔ ∃ r : Fin 24, FaceFits (5, 4) p k r := by
+  decide +kernel
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Geometry/TargetFour.lean b/LeanPool/MacMahon/Geometry/TargetFour.lean
new file mode 100644
index 0000000000..312efa28b7
--- /dev/null
+++ b/LeanPool/MacMahon/Geometry/TargetFour.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Definitions
+
+/-!
+# Face and corner matching for targets in tableau row 4
+-/
+
+@[expose] public section
+
+namespace MacMahon
+
+theorem face_corner_40 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 4 0 k) ↔ ∃ r : Fin 24, FaceFits (4, 0) p k r := by
+  decide +kernel
+
+theorem face_corner_41 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 4 1 k) ↔ ∃ r : Fin 24, FaceFits (4, 1) p k r := by
+  decide +kernel
+
+theorem face_corner_42 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 4 2 k) ↔ ∃ r : Fin 24, FaceFits (4, 2) p k r := by
+  decide +kernel
+
+theorem face_corner_43 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 4 3 k) ↔ ∃ r : Fin 24, FaceFits (4, 3) p k r := by
+  decide +kernel
+
+theorem face_corner_45 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 4 5 k) ↔ ∃ r : Fin 24, FaceFits (4, 5) p k r := by
+  decide +kernel
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Geometry/TargetOne.lean b/LeanPool/MacMahon/Geometry/TargetOne.lean
new file mode 100644
index 0000000000..12f0e306f4
--- /dev/null
+++ b/LeanPool/MacMahon/Geometry/TargetOne.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Definitions
+
+/-!
+# Face and corner matching for targets in tableau row 1
+-/
+
+@[expose] public section
+
+namespace MacMahon
+
+theorem face_corner_10 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 1 0 k) ↔ ∃ r : Fin 24, FaceFits (1, 0) p k r := by
+  decide +kernel
+
+theorem face_corner_12 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 1 2 k) ↔ ∃ r : Fin 24, FaceFits (1, 2) p k r := by
+  decide +kernel
+
+theorem face_corner_13 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 1 3 k) ↔ ∃ r : Fin 24, FaceFits (1, 3) p k r := by
+  decide +kernel
+
+theorem face_corner_14 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 1 4 k) ↔ ∃ r : Fin 24, FaceFits (1, 4) p k r := by
+  decide +kernel
+
+theorem face_corner_15 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 1 5 k) ↔ ∃ r : Fin 24, FaceFits (1, 5) p k r := by
+  decide +kernel
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Geometry/TargetThree.lean b/LeanPool/MacMahon/Geometry/TargetThree.lean
new file mode 100644
index 0000000000..4ae7d3748a
--- /dev/null
+++ b/LeanPool/MacMahon/Geometry/TargetThree.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Definitions
+
+/-!
+# Face and corner matching for targets in tableau row 3
+-/
+
+@[expose] public section
+
+namespace MacMahon
+
+theorem face_corner_30 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 3 0 k) ↔ ∃ r : Fin 24, FaceFits (3, 0) p k r := by
+  decide +kernel
+
+theorem face_corner_31 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 3 1 k) ↔ ∃ r : Fin 24, FaceFits (3, 1) p k r := by
+  decide +kernel
+
+theorem face_corner_32 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 3 2 k) ↔ ∃ r : Fin 24, FaceFits (3, 2) p k r := by
+  decide +kernel
+
+theorem face_corner_34 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 3 4 k) ↔ ∃ r : Fin 24, FaceFits (3, 4) p k r := by
+  decide +kernel
+
+theorem face_corner_35 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 3 5 k) ↔ ∃ r : Fin 24, FaceFits (3, 5) p k r := by
+  decide +kernel
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Geometry/TargetTwo.lean b/LeanPool/MacMahon/Geometry/TargetTwo.lean
new file mode 100644
index 0000000000..cc788e5a4d
--- /dev/null
+++ b/LeanPool/MacMahon/Geometry/TargetTwo.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Definitions
+
+/-!
+# Face and corner matching for targets in tableau row 2
+-/
+
+@[expose] public section
+
+namespace MacMahon
+
+theorem face_corner_20 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 2 0 k) ↔ ∃ r : Fin 24, FaceFits (2, 0) p k r := by
+  decide +kernel
+
+theorem face_corner_21 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 2 1 k) ↔ ∃ r : Fin 24, FaceFits (2, 1) p k r := by
+  decide +kernel
+
+theorem face_corner_23 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 2 3 k) ↔ ∃ r : Fin 24, FaceFits (2, 3) p k r := by
+  decide +kernel
+
+theorem face_corner_24 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 2 4 k) ↔ ∃ r : Fin 24, FaceFits (2, 4) p k r := by
+  decide +kernel
+
+theorem face_corner_25 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 2 5 k) ↔ ∃ r : Fin 24, FaceFits (2, 5) p k r := by
+  decide +kernel
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Geometry/TargetZero.lean b/LeanPool/MacMahon/Geometry/TargetZero.lean
new file mode 100644
index 0000000000..17347f0e32
--- /dev/null
+++ b/LeanPool/MacMahon/Geometry/TargetZero.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Definitions
+
+/-!
+# Face and corner matching for targets in tableau row 0
+-/
+
+@[expose] public section
+
+namespace MacMahon
+
+theorem face_corner_01 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 0 1 k) ↔ ∃ r : Fin 24, FaceFits (0, 1) p k r := by
+  decide +kernel
+
+theorem face_corner_02 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 0 2 k) ↔ ∃ r : Fin 24, FaceFits (0, 2) p k r := by
+  decide +kernel
+
+theorem face_corner_03 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 0 3 k) ↔ ∃ r : Fin 24, FaceFits (0, 3) p k r := by
+  decide +kernel
+
+theorem face_corner_04 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 0 4 k) ↔ ∃ r : Fin 24, FaceFits (0, 4) p k r := by
+  decide +kernel
+
+theorem face_corner_05 : ∀ p : Pair, ∀ k : Slot,
+    HasCorner p (cornerAt 0 5 k) ↔ ∃ r : Fin 24, FaceFits (0, 5) p k r := by
+  decide +kernel
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Imports.lean b/LeanPool/MacMahon/Imports.lean
new file mode 100644
index 0000000000..d3b9b0a058
--- /dev/null
+++ b/LeanPool/MacMahon/Imports.lean
@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+module  -- shake: keep-all --deprecated_module: ignore
+
+-- Generated project imports; run `lake exe mk_all`.
+public import LeanPool.MacMahon
+public import LeanPool.MacMahon.Arithmetic
+public import LeanPool.MacMahon.Classification
+public import LeanPool.MacMahon.Colourings
+public import LeanPool.MacMahon.Counting
+public import LeanPool.MacMahon.Data
+public import LeanPool.MacMahon.Definitions
+public import LeanPool.MacMahon.Geometry
+public import LeanPool.MacMahon.Geometry.TargetFive
+public import LeanPool.MacMahon.Geometry.TargetFour
+public import LeanPool.MacMahon.Geometry.TargetOne
+public import LeanPool.MacMahon.Geometry.TargetThree
+public import LeanPool.MacMahon.Geometry.TargetTwo
+public import LeanPool.MacMahon.Geometry.TargetZero
+public import LeanPool.MacMahon.Incidence
+public import LeanPool.MacMahon.Partitions
+public import LeanPool.MacMahon.Rotations
+public import LeanPool.MacMahon.Structure
+public import LeanPool.MacMahon.Submission
+public import LeanPool.MacMahon.Theorems
+public import LeanPool.MacMahon.Types
+public import LeanPool.MacMahon.Witness
+public import LeanPool.MacMahon.WitnessData
diff --git a/LeanPool/MacMahon/Incidence.lean b/LeanPool/MacMahon/Incidence.lean
new file mode 100644
index 0000000000..79ce6814b7
--- /dev/null
+++ b/LeanPool/MacMahon/Incidence.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Partitions
+
+/-!
+# Corner incidence and usable varieties
+-/
+
+@[expose] public section
+namespace MacMahon
+theorem cornerAt_mem : ∀ i j : Label, i ≠ j → ∀ k : Slot,
+    HasCorner (i, j) (cornerAt i j k) := by decide +kernel
+
+theorem every_corner : ∀ c : Corner, ∃ i j : Label, i ≠ j ∧
+    ∃ k : Slot, cornerAt i j k = c := by decide +kernel
+
+theorem usable_rule : ∀ i j : Label, i ≠ j → ∀ p : Pair,
+    Usable (i, j) p ↔ p.1 ≠ p.2 ∧
+      (p = (i, j) ∨ (p.1 ≠ i ∧ p.2 ≠ j ∧ p ≠ (j, i))) := by decide +kernel
+
+theorem partition_corner_support : ∀ b : Fin 10, ∀ p : Pair,
+    HasCorner p (partitionCorner b) → winner b p = 1 := by decide +kernel
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Partitions.lean b/LeanPool/MacMahon/Partitions.lean
new file mode 100644
index 0000000000..684236b575
--- /dev/null
+++ b/LeanPool/MacMahon/Partitions.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Definitions
+
+public import Mathlib.Data.Fintype.Powerset
+
+/-!
+# The ten two-triangle inventories
+-/
+
+@[expose] public section
+namespace MacMahon
+
+/-- The ten unordered partitions, choosing the triple containing label 0. -/
+def triple : Fin 10 → Finset Label :=
+  ![{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}]
+
+/-- One copy of each directed edge within either triple. -/
+def twoTriangles (s : Finset Label) : Inventory := fun p =>
+  if p.1 ≠ p.2 ∧ ((p.1 ∈ s ∧ p.2 ∈ s) ∨ (p.1 ∉ s ∧ p.2 ∉ s)) then 1 else 0
+
+/-- The ten candidates, defined structurally rather than by a matrix table. -/
+def winner (b : Fin 10) : Inventory := twoTriangles (triple b)
+
+lemma triple_card : ∀ b : Fin 10, (triple b).card = 3 := by decide +kernel
+
+lemma winner_two_triangles : ∀ b : Fin 10,
+    (triple b).card = 3 ∧ winner b = twoTriangles (triple b) :=
+  fun b => ⟨triple_card b, rfl⟩
+
+lemma partition_complete : ∀ s : Finset Label, s.card = 3 →
+    ∃ b : Fin 10, twoTriangles s = winner b := by decide +kernel
+
+lemma winners_iff_two_triangles (a : Inventory) :
+    (∃ b : Fin 10, a = winner b) ↔
+    ∃ s : Finset Label, s.card = 3 ∧ a = twoTriangles s := by
+  constructor
+  · rintro ⟨b, rfl⟩
+    exact ⟨triple b, winner_two_triangles b⟩
+  · rintro ⟨s, hs, rfl⟩
+    exact partition_complete s hs
+lemma winner_properties : ∀ b : Fin 10,
+    DiagonalZero (winner b) ∧ total (winner b) = 12 ∧ ∀ p, winner b p ≤ 1 := by
+  unfold DiagonalZero total
+  decide +kernel
+
+theorem winners_distinct : Function.Injective winner := by decide +kernel
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Rotations.lean b/LeanPool/MacMahon/Rotations.lean
new file mode 100644
index 0000000000..fd82fb7bd3
--- /dev/null
+++ b/LeanPool/MacMahon/Rotations.lean
@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Definitions
+
+/-!
+# Proper rotations and cube varieties
+-/
+
+@[expose] public section
+namespace MacMahon
+
+/-- Faces are +x, -x, +y, -y, +z, -z. -/
+theorem faceOne_bound : 1 < 6 := by decide
+
+/-- The face in the opposite coordinate direction. -/
+def opposite (f : Fin 6) : Fin 6 :=
+  if f.val % 2 = 0 then f + ⟨1, faceOne_bound⟩ else f - ⟨1, faceOne_bound⟩
+/-- The face map determined by the images of the three positive coordinate axes. -/
+def fromAxes (a b c : Fin 6) : Fin 6 → Fin 6 :=
+  ![a, opposite a, b, opposite b, c, opposite c]
+
+/-- Distinct coordinate axes and determinant +1. -/
+def ValidAxes (a b c : Fin 6) : Prop :=
+  a.val / 2 ≠ b.val / 2 ∧ a.val / 2 ≠ c.val / 2 ∧ b.val / 2 ≠ c.val / 2 ∧
+  (a.val % 2 + b.val % 2 + c.val % 2) % 2 =
+    ((if a.val / 2 > b.val / 2 then 1 else 0) +
+     (if a.val / 2 > c.val / 2 then 1 else 0) +
+     (if b.val / 2 > c.val / 2 then 1 else 0)) % 2
+instance (a b c : Fin 6) : Decidable (ValidAxes a b c) := by
+  unfold ValidAxes; infer_instance
+
+/-- A face map induced by a determinant-positive signed-axis permutation. -/
+def ProperRotation (r : Fin 6 → Fin 6) : Prop :=
+  ∃ a b c, ValidAxes a b c ∧ r = fromAxes a b c
+
+theorem rotation_table_valid : ∀ n : Fin 24,
+    ValidAxes (rotations n 0) (rotations n 2) (rotations n 4) ∧
+    rotations n = fromAxes (rotations n 0) (rotations n 2) (rotations n 4) := by
+  decide +kernel
+
+theorem rotation_table_complete : ∀ a b c : Fin 6, ValidAxes a b c →
+    ∃ n : Fin 24, fromAxes a b c = rotations n := by decide +kernel
+
+theorem proper_rotation_iff (r : Fin 6 → Fin 6) :
+    ProperRotation r ↔ ∃ n : Fin 24, r = rotations n := by
+  constructor
+  · rintro ⟨a, b, c, h, rfl⟩
+    exact rotation_table_complete a b c h
+  · rintro ⟨n, rfl⟩
+    exact ⟨_, _, _, rotation_table_valid n⟩
+
+theorem rotations_bijective : ∀ n : Fin 24, Function.Bijective (rotations n) := by
+  decide +kernel
+
+theorem rotations_distinct : Function.Injective rotations := by decide +kernel
+
+theorem face_colours_valid : ∀ i j : Label, i ≠ j →
+    Function.Injective (faceColours i j) ∧ ∀ f : Fin 6, faceColours i j f ≠ 0 := by
+  decide +kernel
+
+/-- Different Conway labels represent different rotation classes. -/
+theorem varieties_distinct : ∀ i j : Label, i ≠ j → ∀ u v : Label, u ≠ v →
+    ∀ r : Fin 24, (∀ f : Fin 6, faceColours i j (rotations r f) = faceColours u v f) →
+    i = u ∧ j = v := by decide +kernel
+
+theorem rotation_inverse : ∀ r : Fin 24, ∃ s : Fin 24,
+    ∀ f : Fin 6, rotations r (rotations s f) = f := by decide +kernel
+
+theorem rotation_composition : ∀ r s : Fin 24, ∃ t : Fin 24,
+    ∀ f : Fin 6, rotations t f = rotations r (rotations s f) := by decide +kernel
+
+/-- The three outward faces at each of the eight binary cube positions. -/
+theorem exposed_face_rule : ∀ k : Slot, ∀ d : Fin 3,
+    (exposedFaces k d).val = 2 * d.val + (k.val / 2^(2-d.val)) % 2 := by decide +kernel
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Structure.lean b/LeanPool/MacMahon/Structure.lean
new file mode 100644
index 0000000000..46d82d48ed
--- /dev/null
+++ b/LeanPool/MacMahon/Structure.lean
@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Definitions
+
+public import Mathlib.Algebra.Order.BigOperators.Group.Finset
+
+/-!
+# Symmetry of degree-two inventories
+-/
+
+@[expose] public section
+namespace MacMahon
+open scoped BigOperators
+
+lemma entry_le_row (a : Inventory) (i j : Label) : a (i, j) ≤ row a i :=
+  Finset.single_le_sum (f := fun j => a (i, j)) (fun _ _ => Nat.zero_le _) (Finset.mem_univ j)
+
+/-- Two unit entries exhaust a row of total multiplicity two. -/
+lemma row_eq_of_two_unit_entries (a : Inventory) (i j k : Label) (hjk : j ≠ k)
+    (hr : row a i = 2) (hj : a (i, j) = 1) (hk : a (i, k) = 1) :
+    ∀ l, a (i, l) = if l = j ∨ l = k then 1 else 0 := by
+  intro l
+  by_cases hlj : l = j
+  · subst l
+    simp [hj]
+  by_cases hlk : l = k
+  · subst l
+    simp [hk]
+  have hsum : a (i, j) + a (i, k) + a (i, l) ≤ row a i := by
+    simpa [row, Finset.sum_insert, hjk, Ne.symm hlj, Ne.symm hlk, Nat.add_assoc] using
+      (Finset.sum_le_sum_of_subset (f := fun n : Label => a (i, n))
+        (Finset.subset_univ ({j, k, l} : Finset Label)))
+  simp only [hlj, hlk, or_self, ite_false]
+  omega
+
+/-- Degree two and reciprocal support force reciprocal multiplicities. -/
+lemma symmetric_of_degree_two (a : Inventory)
+    (hr : ∀ i, row a i = 2) (hc : ∀ i, col a i = 2)
+    (hb : ∀ i j, a (j, i) ≤ 2 * a (i, j)) : ∀ i j, a (i, j) = a (j, i) := by
+  have ht : ∀ i j, a (i, j) = 2 → a (j, i) = 2 := by
+    intro i j hij
+    have hzero : ∀ k, k ≠ j → a (k, i) = 0 := by
+      intro k hkj
+      have hsum : a (i, j) + a (i, k) ≤ row a i :=
+        Finset.add_le_sum (f := fun j => a (i, j)) (fun _ _ => Nat.zero_le _) (Finset.mem_univ j)
+          (Finset.mem_univ k) hkj.symm
+      have := hb i k
+      rw [hr i, hij] at hsum
+      omega
+    have hsum : col a i = a (j, i) :=
+      Finset.sum_eq_single j (fun k _ hk => hzero k hk) (by simp)
+    have := hc i
+    omega
+  intro i j
+  have hi := entry_le_row a i j
+  have hj := entry_le_row a j i
+  rw [hr i] at hi
+  rw [hr j] at hj
+  have hb1 := hb i j
+  have hb2 := hb j i
+  have ht1 := ht i j
+  have ht2 := ht j i
+  omega
+end MacMahon
diff --git a/LeanPool/MacMahon/Submission.lean b/LeanPool/MacMahon/Submission.lean
new file mode 100644
index 0000000000..572e412e36
--- /dev/null
+++ b/LeanPool/MacMahon/Submission.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Theorems
+
+/-!
+# Physical classification and geometric coverage
+-/
+
+@[expose] public section
+namespace MacMahon
+
+/-- The multiplicity conclusion expressed using physical face matching. -/
+theorem physical_minimum_has_no_repeats (a : Inventory) (hz : DiagonalZero a)
+    (ht : total a = 12) (h : PhysicalUniversal a) : ∀ p, a p ≤ 1 :=
+  minimum_has_no_repeats a hz ht ((universal_iff_physical a).mpr h)
+
+/-- Every assignment of six distinct nonzero colours is represented by the tableau. -/
+theorem face_assignment_coverage (f : Fin 6 → Fin 7) (hi : Function.Injective f)
+    (hn : ∀ d, f d ≠ 0) :
+    ∃ i j : Label, i ≠ j ∧ ∃ r : Fin 24,
+      ∀ d : Fin 6, f d = faceColours i j (rotations r d) := by
+  let g : Fin 6 → NonzeroColour := fun d => ⟨f d, hn d⟩
+  have hg : Function.Injective g := by
+    intro d e h
+    exact hi (congrArg Subtype.val h)
+  let e : Colouring := Equiv.ofBijective g
+    ((Fintype.bijective_iff_injective_and_card g).mpr ⟨hg, Fintype.card_congr colourEquiv⟩)
+  obtain ⟨⟨⟨⟨i, j⟩, hij⟩, r⟩, he⟩ := all_colourings.2 e
+  refine ⟨i, j, hij, r, ?_⟩
+  intro d
+  exact (congrArg (fun x : Colouring => (x d).val) he).symm
+
+/-- The variety and rotation representing a face assignment are unique. -/
+theorem 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 := by
+  have he : orientedColouring (⟨(i, j), hij⟩, r) = orientedColouring (⟨(u, v), huv⟩, s) := by
+    ext d
+    exact congrArg Fin.val (hf d)
+  have hp := orientedColouring_injective he
+  have hq := congrArg (fun x : Variety × Fin 24 => x.1.val) hp
+  exact ⟨congrArg Prod.fst hq, congrArg Prod.snd hq, congrArg Prod.snd hp⟩
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Theorems.lean b/LeanPool/MacMahon/Theorems.lean
new file mode 100644
index 0000000000..09e4ae28ed
--- /dev/null
+++ b/LeanPool/MacMahon/Theorems.lean
@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import Mathlib.SetTheory.Cardinal.Finite
+
+public import LeanPool.MacMahon.Arithmetic
+public import LeanPool.MacMahon.Classification
+public import LeanPool.MacMahon.Colourings
+public import LeanPool.MacMahon.Geometry
+public import LeanPool.MacMahon.Witness
+
+/-!
+# Minimum universal collections of coloured cubes
+-/
+
+@[expose] public section
+namespace MacMahon
+
+/-- Complete classification, including inventories with repeated physical cubes. -/
+theorem classification (a : Inventory) (hz : DiagonalZero a) (ht : total a = 12) :
+    Universal a ↔ ∃ b : Fin 10, a = winner b := by
+  constructor
+  · intro h
+    have hr := rows_two a hz h ht
+    have hc := cols_two a hz h ht
+    have hs := symmetric_of_degree_two a hr hc (reverse_bound a hz h ht)
+    exact classify_degree_two a hz hr hs (universal_partition_cover a h)
+  · rintro ⟨b, rfl⟩
+    exact winner_universal b
+
+theorem minimum_has_no_repeats (a : Inventory) (hz : DiagonalZero a)
+    (ht : total a = 12) (h : Universal a) : ∀ p, a p ≤ 1 := by
+  obtain ⟨b, rfl⟩ := (classification a hz ht).mp h
+  exact (winner_properties b).2.2
+
+/-- Universal corner-matching inventories attaining size twelve. -/
+abbrev MinimumInventory := {a : Inventory // DiagonalZero a ∧ total a = 12 ∧ Universal a}
+
+/-- The minimum inventory supplied by one of the ten triple partitions. -/
+def minimumMap (b : Fin 10) : MinimumInventory :=
+  ⟨winner b, (winner_properties b).1, (winner_properties b).2.1, winner_universal b⟩
+
+/-- Classify the labelled minimum inventories by the ten triple partitions. -/
+noncomputable def minimumEquiv : Fin 10 ≃ MinimumInventory :=
+  Equiv.ofBijective minimumMap ⟨by
+    intro b c h
+    exact winners_distinct (congrArg Subtype.val h), by
+    rintro ⟨a, hz, ht, hu⟩
+    obtain ⟨b, hb⟩ := (classification a hz ht).mp hu
+    exact ⟨b, Subtype.ext hb.symm⟩⟩
+
+/-- Exactly ten labelled minimum universal inventories exist. -/
+theorem exactly_ten : Nat.card MinimumInventory = 10 := by
+  rw [← Nat.card_congr minimumEquiv]
+  simp
+
+theorem physical_minimum (a : Inventory) (hz : DiagonalZero a)
+    (h : PhysicalUniversal a) : 12 ≤ total a :=
+  universal_minimum a hz ((universal_iff_physical a).mpr h)
+
+theorem physical_classification (a : Inventory) (hz : DiagonalZero a) (ht : total a = 12) :
+    PhysicalUniversal a ↔ ∃ b : Fin 10, a = winner b := by
+  rw [← universal_iff_physical, classification a hz ht]
+
+/-- The structural form of the classification: two disjoint triangles. -/
+theorem physical_iff_two_triangles (a : Inventory) (hz : DiagonalZero a)
+    (ht : total a = 12) : PhysicalUniversal a ↔
+    ∃ s : Finset Label, s.card = 3 ∧ a = twoTriangles s := by
+  rw [physical_classification a hz ht, winners_iff_two_triangles]
+
+/-- Physically universal inventories attaining size twelve. -/
+abbrev MinimumPhysicalInventory :=
+  {a : Inventory // DiagonalZero a ∧ total a = 12 ∧ PhysicalUniversal a}
+
+theorem physical_exactly_ten : Nat.card MinimumPhysicalInventory = 10 := by
+  have e : MinimumInventory ≃ MinimumPhysicalInventory :=
+    Equiv.subtypeEquivRight (fun a => by rw [universal_iff_physical])
+  rw [← Nat.card_congr e]
+  exact exactly_ten
+
+theorem minimum_size : IsLeast
+    {n : ℕ | ∃ a : Inventory, DiagonalZero a ∧ PhysicalUniversal a ∧ total a = n} 12 := by
+  constructor
+  · exact ⟨winner 0, (winner_properties 0).1,
+      (universal_iff_physical _).mp (winner_universal 0), (winner_properties 0).2.1⟩
+  · rintro n ⟨a, hz, hu, rfl⟩
+    exact physical_minimum a hz hu
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Types.lean b/LeanPool/MacMahon/Types.lean
new file mode 100644
index 0000000000..a5ad10c7ad
--- /dev/null
+++ b/LeanPool/MacMahon/Types.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import Mathlib.Data.Fin.VecNotation
+public import Mathlib.Data.Fintype.Prod
+
+/-!
+# Finite domains for coloured cubes
+-/
+
+@[expose] public section
+namespace MacMahon
+
+/-- Conway tableau labels, distinct from the six face colours. -/
+abbrev Label := Fin 6
+/-- Ordered coordinates in Conway's tableau; diagonal entries are reserved. -/
+abbrev Pair := Label × Label
+/-- The forty oriented corner types formed from the six distinct face colours. -/
+abbrev Corner := Fin 40
+/-- The eight positions in a two-by-two-by-two assembly. -/
+abbrev Slot := Fin 8
+/-- Natural-number multiplicities of the tableau entries. -/
+abbrev Inventory := Pair → ℕ
+
+end MacMahon
diff --git a/LeanPool/MacMahon/Witness.lean b/LeanPool/MacMahon/Witness.lean
new file mode 100644
index 0000000000..de194eaa21
--- /dev/null
+++ b/LeanPool/MacMahon/Witness.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Partitions
+public import LeanPool.MacMahon.WitnessData
+
+/-!
+# Sufficiency of the ten candidate inventories
+-/
+
+@[expose] public section
+namespace MacMahon
+theorem 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) := by decide +kernel
+
+/-- Every known set has an explicit eight-cube construction for every target. -/
+theorem winner_universal (b : Fin 10) : Universal (winner b) := by
+  intro i j hij
+  obtain ⟨hinj, hfit⟩ := witness_facts b i j hij
+  let f : Slot → Stock (winner b) := fun k =>
+    ⟨witness b i j k, ⟨0, by rw [(hfit k).1]; decide⟩⟩
+  refine ⟨⟨f, ?_⟩, fun k => (hfit k).2⟩
+  intro k l heq
+  exact hinj (congrArg Sigma.fst heq)
+
+end MacMahon
diff --git a/LeanPool/MacMahon/WitnessData.lean b/LeanPool/MacMahon/WitnessData.lean
new file mode 100644
index 0000000000..d1018cb4fa
--- /dev/null
+++ b/LeanPool/MacMahon/WitnessData.lean
@@ -0,0 +1,523 @@
+/-
+Copyright (c) 2026 Jason Davies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jason Davies
+-/
+-- Modified for Lean Pool integration.
+module
+
+public import LeanPool.MacMahon.Types
+
+/-!
+# Explicit eight-cube construction certificates
+-/
+
+@[expose] public section
+-- Generated upstream by scripts/generate_lean_data.py at the pinned source revision.
+-- Numeric entries are unchanged; see the source card in LeanPool.MacMahon.
+namespace MacMahon
+/-- Construction data for the ten candidate inventories and thirty valid target varieties. -/
+def witness : Fin 10 → Label → Label → Slot → Pair :=
+  ![
+    ![
+      ![
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 3), (5, 4), (4, 3), (2, 0), (1, 2), (3, 4), (4, 5), (0, 1)],
+        ![(5, 4), (5, 3), (3, 4), (2, 1), (1, 0), (4, 3), (3, 5), (0, 2)],
+        ![(4, 5), (2, 0), (3, 5), (1, 2), (3, 4), (2, 1), (5, 4), (1, 0)],
+        ![(3, 5), (1, 0), (4, 5), (2, 1), (4, 3), (1, 2), (5, 3), (2, 0)],
+        ![(4, 3), (5, 3), (5, 4), (3, 4), (1, 0), (2, 1), (1, 2), (2, 0)]
+      ],
+      ![
+        ![(4, 5), (3, 5), (0, 2), (3, 4), (4, 3), (2, 1), (5, 3), (1, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(3, 5), (0, 1), (3, 4), (5, 4), (4, 5), (4, 3), (2, 0), (1, 2)],
+        ![(3, 5), (5, 4), (4, 5), (3, 4), (2, 0), (2, 1), (0, 1), (0, 2)],
+        ![(5, 3), (4, 5), (2, 1), (2, 0), (4, 3), (3, 5), (0, 2), (0, 1)],
+        ![(5, 4), (0, 2), (4, 3), (0, 1), (3, 4), (2, 1), (5, 3), (2, 0)]
+      ],
+      ![
+        ![(3, 5), (4, 5), (1, 2), (4, 3), (3, 4), (0, 1), (5, 4), (2, 0)],
+        ![(1, 0), (5, 3), (4, 5), (4, 3), (3, 4), (5, 4), (2, 1), (0, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 4), (3, 5), (1, 2), (1, 0), (3, 4), (4, 5), (0, 1), (0, 2)],
+        ![(4, 5), (5, 3), (3, 5), (4, 3), (1, 0), (1, 2), (0, 2), (0, 1)],
+        ![(5, 3), (0, 1), (3, 4), (0, 2), (4, 3), (1, 2), (5, 4), (1, 0)]
+      ],
+      ![
+        ![(5, 4), (0, 1), (4, 3), (2, 1), (5, 3), (1, 2), (4, 5), (0, 2)],
+        ![(4, 5), (5, 3), (4, 3), (5, 4), (1, 2), (0, 2), (2, 0), (1, 0)],
+        ![(5, 3), (4, 5), (0, 1), (2, 1), (5, 4), (4, 3), (2, 0), (1, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(4, 5), (0, 2), (1, 0), (1, 2), (2, 1), (3, 4), (2, 0), (0, 1)],
+        ![(2, 0), (3, 5), (4, 3), (1, 2), (2, 1), (1, 0), (0, 1), (0, 2)]
+      ],
+      ![
+        ![(5, 3), (0, 2), (3, 4), (1, 2), (5, 4), (2, 1), (3, 5), (0, 1)],
+        ![(5, 4), (3, 5), (0, 2), (1, 2), (5, 3), (3, 4), (1, 0), (2, 0)],
+        ![(3, 5), (5, 4), (3, 4), (5, 3), (2, 1), (0, 1), (1, 0), (2, 0)],
+        ![(2, 0), (3, 5), (2, 1), (0, 1), (4, 3), (1, 2), (1, 0), (0, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(1, 0), (2, 0), (3, 4), (2, 1), (4, 5), (1, 2), (0, 2), (0, 1)]
+      ],
+      ![
+        ![(3, 5), (3, 4), (4, 3), (4, 5), (1, 2), (0, 1), (0, 2), (2, 1)],
+        ![(3, 5), (2, 0), (3, 4), (1, 2), (4, 3), (1, 0), (4, 5), (0, 2)],
+        ![(4, 5), (1, 0), (4, 3), (2, 1), (3, 4), (2, 0), (3, 5), (0, 1)],
+        ![(0, 1), (5, 3), (2, 1), (0, 2), (3, 4), (1, 2), (2, 0), (1, 0)],
+        ![(0, 2), (5, 4), (1, 2), (0, 1), (3, 5), (2, 1), (1, 0), (2, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)]
+      ]
+    ],
+    ![
+      ![
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(2, 5), (3, 0), (2, 4), (5, 4), (4, 5), (4, 2), (1, 3), (0, 1)],
+        ![(5, 4), (2, 4), (2, 5), (4, 5), (1, 0), (3, 1), (1, 3), (3, 0)],
+        ![(1, 0), (4, 5), (2, 4), (2, 5), (5, 2), (4, 2), (5, 4), (0, 3)],
+        ![(4, 2), (5, 2), (1, 3), (3, 0), (2, 5), (4, 5), (1, 0), (3, 1)],
+        ![(5, 2), (3, 0), (3, 1), (4, 2), (1, 0), (5, 4), (2, 4), (1, 3)]
+      ],
+      ![
+        ![(1, 0), (5, 2), (4, 5), (4, 2), (2, 4), (5, 4), (2, 5), (0, 3)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(0, 3), (5, 4), (2, 5), (3, 1), (4, 5), (3, 0), (0, 1), (2, 4)],
+        ![(4, 2), (0, 1), (4, 5), (2, 5), (5, 2), (5, 4), (2, 4), (1, 3)],
+        ![(2, 5), (4, 5), (4, 2), (5, 2), (3, 1), (0, 3), (3, 0), (0, 1)],
+        ![(5, 4), (2, 4), (3, 0), (0, 1), (4, 2), (5, 2), (3, 1), (0, 3)]
+      ],
+      ![
+        ![(4, 2), (4, 5), (5, 4), (5, 2), (1, 3), (0, 1), (0, 3), (3, 1)],
+        ![(4, 5), (4, 2), (1, 3), (3, 0), (5, 2), (5, 4), (0, 3), (1, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 4), (5, 2), (3, 1), (1, 0), (4, 2), (4, 5), (0, 1), (3, 0)],
+        ![(4, 5), (3, 1), (0, 3), (2, 4), (1, 0), (3, 0), (1, 3), (0, 1)],
+        ![(0, 1), (4, 2), (2, 5), (1, 3), (3, 1), (3, 0), (0, 3), (1, 0)]
+      ],
+      ![
+        ![(5, 4), (1, 3), (5, 2), (4, 2), (2, 4), (2, 5), (0, 1), (3, 0)],
+        ![(1, 0), (2, 4), (5, 2), (5, 4), (4, 5), (2, 5), (3, 1), (0, 3)],
+        ![(2, 5), (4, 5), (0, 1), (1, 3), (5, 4), (2, 4), (0, 3), (1, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(4, 5), (2, 5), (1, 0), (0, 3), (5, 2), (4, 2), (1, 3), (0, 1)],
+        ![(4, 2), (5, 2), (5, 4), (2, 4), (0, 3), (1, 0), (0, 1), (1, 3)]
+      ],
+      ![
+        ![(2, 5), (2, 4), (0, 3), (3, 1), (5, 4), (5, 2), (1, 3), (0, 1)],
+        ![(5, 4), (5, 2), (2, 5), (2, 4), (3, 0), (1, 3), (1, 0), (0, 3)],
+        ![(1, 3), (2, 5), (1, 0), (3, 0), (4, 2), (0, 1), (0, 3), (3, 1)],
+        ![(3, 1), (5, 4), (5, 2), (0, 1), (2, 4), (3, 0), (1, 0), (2, 5)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(2, 4), (0, 3), (1, 0), (1, 3), (3, 1), (4, 5), (3, 0), (0, 1)]
+      ],
+      ![
+        ![(2, 4), (1, 3), (0, 1), (4, 5), (3, 1), (4, 2), (2, 5), (0, 3)],
+        ![(4, 2), (4, 5), (1, 0), (0, 3), (2, 5), (2, 4), (3, 0), (1, 3)],
+        ![(2, 4), (1, 0), (3, 1), (3, 0), (0, 3), (1, 3), (5, 2), (0, 1)],
+        ![(2, 5), (2, 4), (4, 2), (4, 5), (0, 1), (3, 0), (3, 1), (1, 0)],
+        ![(3, 0), (2, 5), (3, 1), (0, 1), (5, 4), (1, 3), (1, 0), (0, 3)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)]
+      ]
+    ],
+    ![
+      ![
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(1, 4), (2, 5), (3, 2), (3, 5), (5, 3), (2, 3), (5, 2), (0, 1)],
+        ![(2, 3), (4, 0), (4, 1), (5, 3), (1, 0), (2, 5), (3, 5), (1, 4)],
+        ![(5, 2), (1, 4), (4, 1), (2, 5), (4, 0), (3, 5), (3, 2), (1, 0)],
+        ![(3, 5), (4, 1), (3, 2), (5, 2), (2, 5), (2, 3), (1, 0), (0, 4)],
+        ![(5, 2), (1, 4), (4, 0), (2, 3), (1, 0), (3, 2), (5, 3), (4, 1)]
+      ],
+      ![
+        ![(5, 2), (0, 4), (5, 3), (2, 3), (3, 2), (3, 5), (2, 5), (1, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(3, 5), (0, 1), (2, 5), (4, 0), (2, 3), (0, 4), (5, 3), (4, 1)],
+        ![(0, 4), (2, 5), (3, 2), (4, 1), (5, 2), (4, 0), (0, 1), (3, 5)],
+        ![(1, 4), (3, 2), (5, 3), (5, 2), (2, 5), (3, 5), (2, 3), (0, 1)],
+        ![(4, 1), (5, 3), (5, 2), (0, 1), (2, 3), (4, 0), (0, 4), (3, 2)]
+      ],
+      ![
+        ![(3, 5), (1, 4), (0, 1), (5, 2), (4, 1), (5, 3), (3, 2), (0, 4)],
+        ![(5, 3), (1, 4), (0, 4), (5, 2), (4, 0), (3, 2), (3, 5), (1, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(4, 1), (3, 5), (4, 0), (1, 0), (2, 3), (0, 4), (0, 1), (1, 4)],
+        ![(5, 2), (4, 0), (4, 1), (3, 2), (1, 0), (5, 3), (3, 5), (0, 1)],
+        ![(3, 2), (0, 1), (4, 0), (4, 1), (1, 4), (2, 5), (1, 0), (0, 4)]
+      ],
+      ![
+        ![(2, 3), (2, 5), (5, 2), (5, 3), (4, 1), (0, 4), (0, 1), (1, 4)],
+        ![(5, 2), (5, 3), (1, 4), (4, 0), (2, 3), (2, 5), (0, 4), (1, 0)],
+        ![(2, 5), (1, 4), (0, 1), (3, 2), (4, 0), (1, 0), (4, 1), (0, 4)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 3), (2, 5), (1, 0), (4, 0), (5, 2), (2, 3), (4, 1), (0, 1)],
+        ![(0, 4), (5, 2), (0, 1), (4, 1), (1, 4), (1, 0), (2, 3), (3, 5)]
+      ],
+      ![
+        ![(1, 4), (5, 3), (2, 5), (2, 3), (3, 2), (4, 0), (3, 5), (0, 1)],
+        ![(2, 3), (1, 0), (2, 5), (3, 5), (5, 3), (4, 1), (0, 4), (3, 2)],
+        ![(3, 5), (2, 5), (2, 3), (5, 3), (1, 4), (0, 1), (1, 0), (0, 4)],
+        ![(5, 2), (3, 5), (0, 4), (0, 1), (3, 2), (2, 5), (1, 0), (1, 4)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 2), (3, 2), (1, 0), (0, 4), (2, 3), (5, 3), (1, 4), (0, 1)]
+      ],
+      ![
+        ![(3, 5), (4, 1), (3, 2), (0, 4), (2, 3), (0, 1), (2, 5), (1, 4)],
+        ![(0, 4), (3, 2), (2, 3), (4, 0), (2, 5), (1, 0), (1, 4), (3, 5)],
+        ![(1, 0), (2, 3), (5, 2), (0, 4), (4, 0), (4, 1), (1, 4), (0, 1)],
+        ![(2, 5), (4, 0), (1, 4), (1, 0), (0, 1), (4, 1), (5, 3), (0, 4)],
+        ![(4, 1), (2, 5), (2, 3), (0, 1), (3, 5), (4, 0), (1, 0), (3, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)]
+      ]
+    ],
+    ![
+      ![
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(3, 2), (4, 2), (1, 5), (4, 3), (3, 4), (2, 3), (2, 4), (0, 1)],
+        ![(1, 5), (2, 4), (5, 0), (3, 4), (1, 0), (4, 3), (5, 1), (2, 3)],
+        ![(2, 4), (3, 2), (5, 0), (5, 1), (3, 4), (4, 2), (1, 5), (1, 0)],
+        ![(4, 2), (2, 3), (3, 2), (4, 3), (5, 1), (5, 0), (1, 0), (1, 5)],
+        ![(4, 3), (4, 2), (2, 3), (3, 4), (1, 0), (3, 2), (2, 4), (0, 5)]
+      ],
+      ![
+        ![(2, 4), (2, 3), (3, 4), (4, 2), (0, 5), (4, 3), (3, 2), (1, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(2, 4), (4, 3), (3, 4), (2, 3), (5, 0), (5, 1), (0, 1), (0, 5)],
+        ![(5, 1), (4, 2), (3, 2), (5, 0), (3, 4), (0, 5), (0, 1), (2, 4)],
+        ![(3, 2), (5, 1), (0, 5), (4, 3), (5, 0), (4, 2), (2, 3), (0, 1)],
+        ![(2, 3), (2, 4), (4, 3), (3, 2), (0, 1), (3, 4), (4, 2), (1, 5)]
+      ],
+      ![
+        ![(4, 2), (5, 1), (4, 3), (0, 5), (3, 4), (0, 1), (3, 2), (1, 5)],
+        ![(3, 4), (0, 5), (5, 0), (4, 3), (1, 5), (3, 2), (4, 2), (1, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(1, 5), (1, 0), (0, 5), (4, 2), (3, 4), (5, 0), (0, 1), (2, 3)],
+        ![(1, 0), (2, 4), (5, 0), (1, 5), (3, 2), (0, 5), (5, 1), (0, 1)],
+        ![(3, 2), (0, 1), (5, 1), (3, 4), (5, 0), (4, 3), (4, 2), (1, 0)]
+      ],
+      ![
+        ![(1, 5), (4, 2), (4, 3), (0, 5), (2, 4), (5, 1), (0, 1), (2, 3)],
+        ![(2, 4), (1, 5), (0, 5), (2, 3), (5, 0), (4, 3), (4, 2), (1, 0)],
+        ![(0, 1), (5, 1), (2, 4), (5, 0), (3, 2), (0, 5), (1, 5), (1, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(1, 0), (5, 0), (2, 3), (5, 1), (3, 4), (1, 5), (0, 5), (0, 1)],
+        ![(5, 1), (2, 3), (4, 3), (5, 0), (4, 2), (1, 0), (0, 1), (2, 4)]
+      ],
+      ![
+        ![(3, 2), (1, 5), (5, 1), (2, 3), (0, 5), (3, 4), (2, 4), (0, 1)],
+        ![(2, 3), (1, 0), (3, 4), (5, 0), (2, 4), (0, 5), (3, 2), (1, 5)],
+        ![(5, 1), (4, 2), (2, 3), (0, 5), (5, 0), (0, 1), (1, 0), (1, 5)],
+        ![(0, 5), (0, 1), (1, 5), (3, 2), (2, 4), (5, 1), (1, 0), (4, 3)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(2, 4), (5, 1), (1, 0), (3, 2), (5, 0), (3, 4), (2, 3), (0, 1)]
+      ],
+      ![
+        ![(2, 4), (3, 4), (1, 5), (3, 2), (2, 3), (0, 1), (4, 3), (4, 2)],
+        ![(4, 2), (3, 2), (1, 0), (3, 4), (4, 3), (0, 5), (2, 3), (2, 4)],
+        ![(2, 4), (1, 0), (4, 3), (1, 5), (3, 4), (0, 5), (2, 3), (0, 1)],
+        ![(3, 2), (2, 4), (4, 2), (3, 4), (0, 1), (0, 5), (1, 5), (1, 0)],
+        ![(2, 3), (4, 2), (0, 5), (0, 1), (4, 3), (3, 2), (1, 0), (1, 5)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)]
+      ]
+    ],
+    ![
+      ![
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(3, 2), (5, 4), (1, 5), (2, 0), (4, 5), (2, 3), (3, 0), (1, 4)],
+        ![(2, 3), (1, 5), (4, 1), (4, 5), (5, 4), (1, 4), (5, 1), (0, 2)],
+        ![(4, 5), (3, 2), (4, 1), (5, 1), (1, 5), (1, 4), (2, 0), (0, 3)],
+        ![(2, 0), (4, 1), (4, 5), (3, 0), (5, 1), (2, 3), (3, 2), (1, 5)],
+        ![(1, 4), (3, 0), (5, 4), (2, 3), (5, 1), (3, 2), (4, 1), (2, 0)]
+      ],
+      ![
+        ![(4, 5), (4, 1), (0, 2), (2, 3), (5, 1), (5, 4), (3, 2), (0, 3)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(4, 1), (5, 4), (0, 3), (2, 3), (4, 5), (5, 1), (2, 0), (3, 0)],
+        ![(5, 1), (5, 4), (4, 5), (4, 1), (2, 0), (3, 2), (3, 0), (0, 2)],
+        ![(3, 2), (4, 5), (3, 0), (2, 0), (0, 2), (0, 3), (2, 3), (1, 4)],
+        ![(4, 1), (0, 2), (3, 0), (3, 2), (2, 3), (1, 5), (2, 0), (0, 3)]
+      ],
+      ![
+        ![(5, 1), (1, 4), (5, 4), (2, 0), (4, 1), (4, 5), (0, 3), (1, 5)],
+        ![(4, 5), (1, 4), (3, 2), (3, 0), (1, 5), (5, 4), (0, 3), (0, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(1, 5), (4, 1), (5, 4), (5, 1), (2, 3), (4, 5), (1, 4), (0, 2)],
+        ![(4, 5), (1, 5), (0, 3), (3, 2), (5, 1), (4, 1), (0, 2), (3, 0)],
+        ![(1, 4), (5, 4), (5, 1), (4, 1), (0, 2), (3, 0), (0, 3), (3, 2)]
+      ],
+      ![
+        ![(1, 5), (5, 4), (3, 0), (1, 4), (4, 1), (5, 1), (4, 5), (0, 2)],
+        ![(4, 5), (0, 2), (2, 0), (5, 4), (2, 3), (1, 4), (1, 5), (0, 3)],
+        ![(1, 4), (0, 3), (1, 5), (4, 5), (5, 4), (5, 1), (2, 0), (3, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(4, 5), (0, 2), (2, 3), (5, 1), (0, 3), (1, 5), (4, 1), (2, 0)],
+        ![(5, 1), (2, 3), (2, 0), (4, 1), (0, 3), (5, 4), (1, 4), (0, 2)]
+      ],
+      ![
+        ![(3, 2), (1, 5), (5, 1), (2, 3), (5, 4), (0, 3), (0, 2), (1, 4)],
+        ![(1, 5), (2, 3), (0, 2), (4, 1), (3, 0), (2, 0), (3, 2), (0, 3)],
+        ![(2, 0), (5, 4), (5, 1), (3, 0), (1, 4), (2, 3), (0, 3), (1, 5)],
+        ![(1, 4), (2, 0), (1, 5), (3, 2), (5, 1), (3, 0), (5, 4), (0, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(0, 3), (1, 4), (4, 5), (3, 2), (2, 3), (2, 0), (0, 2), (3, 0)]
+      ],
+      ![
+        ![(4, 1), (0, 2), (3, 2), (4, 5), (2, 3), (1, 5), (1, 4), (0, 3)],
+        ![(2, 0), (0, 3), (2, 3), (5, 1), (3, 0), (3, 2), (1, 4), (0, 2)],
+        ![(4, 5), (2, 3), (2, 0), (1, 5), (0, 3), (4, 1), (1, 4), (3, 0)],
+        ![(1, 4), (0, 2), (3, 0), (4, 5), (2, 0), (4, 1), (1, 5), (3, 2)],
+        ![(1, 5), (3, 0), (2, 3), (2, 0), (0, 2), (3, 2), (5, 4), (0, 3)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)]
+      ]
+    ],
+    ![
+      ![
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(4, 0), (4, 2), (2, 4), (2, 0), (5, 3), (1, 5), (1, 3), (3, 5)],
+        ![(1, 5), (4, 0), (1, 3), (5, 3), (3, 5), (3, 1), (2, 4), (0, 2)],
+        ![(2, 4), (2, 0), (3, 5), (5, 1), (4, 0), (4, 2), (1, 5), (3, 1)],
+        ![(2, 0), (3, 5), (1, 3), (1, 5), (5, 1), (3, 1), (5, 3), (0, 4)],
+        ![(2, 0), (5, 3), (3, 1), (4, 2), (5, 1), (4, 0), (2, 4), (1, 3)]
+      ],
+      ![
+        ![(2, 4), (3, 5), (5, 3), (4, 2), (5, 1), (0, 2), (0, 4), (3, 1)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(3, 5), (2, 0), (5, 1), (4, 0), (3, 1), (0, 4), (5, 3), (2, 4)],
+        ![(3, 5), (4, 2), (0, 4), (1, 3), (2, 0), (4, 0), (2, 4), (0, 2)],
+        ![(4, 0), (5, 1), (5, 3), (2, 0), (3, 1), (4, 2), (0, 2), (3, 5)],
+        ![(0, 2), (3, 1), (0, 4), (2, 4), (4, 2), (4, 0), (2, 0), (1, 5)]
+      ],
+      ![
+        ![(1, 3), (5, 1), (3, 5), (3, 1), (2, 0), (5, 3), (1, 5), (0, 4)],
+        ![(5, 3), (4, 2), (0, 4), (1, 5), (4, 0), (1, 3), (3, 5), (0, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(1, 5), (0, 4), (4, 0), (5, 1), (4, 2), (3, 1), (3, 5), (0, 2)],
+        ![(3, 1), (1, 5), (3, 5), (2, 4), (5, 1), (5, 3), (0, 2), (1, 3)],
+        ![(5, 3), (4, 2), (4, 0), (1, 3), (0, 2), (5, 1), (3, 1), (0, 4)]
+      ],
+      ![
+        ![(1, 5), (4, 2), (0, 4), (5, 3), (2, 4), (5, 1), (1, 3), (0, 2)],
+        ![(2, 4), (5, 3), (2, 0), (4, 0), (0, 4), (0, 2), (1, 5), (3, 1)],
+        ![(5, 3), (2, 0), (2, 4), (1, 3), (4, 0), (5, 1), (1, 5), (0, 4)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 3), (0, 2), (4, 2), (5, 1), (4, 0), (1, 5), (1, 3), (2, 0)],
+        ![(1, 3), (0, 4), (2, 0), (2, 4), (4, 2), (3, 5), (4, 0), (0, 2)]
+      ],
+      ![
+        ![(5, 3), (1, 5), (5, 1), (3, 1), (1, 3), (4, 0), (0, 2), (3, 5)],
+        ![(0, 2), (3, 5), (1, 3), (2, 4), (5, 3), (2, 0), (0, 4), (1, 5)],
+        ![(1, 3), (4, 2), (5, 1), (5, 3), (3, 5), (1, 5), (3, 1), (0, 4)],
+        ![(3, 1), (2, 0), (1, 5), (2, 4), (5, 1), (0, 4), (3, 5), (0, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(2, 4), (5, 1), (5, 3), (0, 4), (3, 1), (2, 0), (0, 2), (1, 3)]
+      ],
+      ![
+        ![(2, 4), (1, 3), (1, 5), (0, 4), (3, 1), (4, 2), (0, 2), (3, 5)],
+        ![(1, 3), (2, 0), (4, 2), (4, 0), (0, 4), (2, 4), (5, 1), (0, 2)],
+        ![(2, 4), (0, 4), (3, 1), (1, 5), (4, 0), (2, 0), (3, 5), (1, 3)],
+        ![(4, 0), (0, 2), (4, 2), (5, 3), (2, 0), (2, 4), (1, 5), (0, 4)],
+        ![(0, 2), (4, 2), (4, 0), (2, 0), (3, 5), (1, 3), (3, 1), (1, 5)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)]
+      ]
+    ],
+    ![
+      ![
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(2, 5), (1, 3), (5, 0), (4, 3), (2, 0), (3, 4), (5, 2), (1, 4)],
+        ![(4, 1), (3, 1), (2, 5), (3, 4), (4, 3), (1, 4), (1, 3), (0, 2)],
+        ![(3, 1), (1, 4), (4, 1), (3, 4), (5, 2), (5, 0), (2, 0), (2, 5)],
+        ![(1, 3), (4, 1), (5, 0), (5, 2), (4, 3), (3, 1), (2, 5), (2, 0)],
+        ![(2, 0), (1, 4), (3, 1), (3, 4), (4, 3), (1, 3), (4, 1), (0, 5)]
+      ],
+      ![
+        ![(3, 1), (5, 2), (3, 4), (0, 5), (4, 3), (0, 2), (4, 1), (2, 5)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(4, 1), (4, 3), (3, 4), (3, 1), (5, 0), (2, 5), (2, 0), (0, 5)],
+        ![(2, 0), (2, 5), (5, 0), (1, 3), (3, 4), (0, 5), (5, 2), (0, 2)],
+        ![(2, 5), (2, 0), (0, 5), (4, 3), (3, 1), (5, 0), (0, 2), (1, 4)],
+        ![(4, 1), (0, 2), (5, 2), (4, 3), (5, 0), (3, 4), (3, 1), (2, 0)]
+      ],
+      ![
+        ![(1, 3), (1, 4), (4, 3), (3, 1), (0, 5), (3, 4), (4, 1), (2, 0)],
+        ![(3, 4), (0, 5), (5, 0), (4, 3), (5, 2), (1, 3), (1, 4), (0, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(4, 1), (5, 2), (0, 5), (3, 4), (5, 0), (3, 1), (1, 4), (0, 2)],
+        ![(5, 2), (3, 1), (4, 1), (5, 0), (4, 3), (0, 5), (0, 2), (1, 3)],
+        ![(1, 4), (1, 3), (3, 4), (4, 1), (0, 2), (4, 3), (3, 1), (2, 5)]
+      ],
+      ![
+        ![(4, 1), (2, 5), (5, 2), (1, 4), (0, 5), (4, 3), (1, 3), (0, 2)],
+        ![(5, 2), (3, 1), (1, 4), (0, 5), (5, 0), (0, 2), (2, 0), (2, 5)],
+        ![(1, 4), (2, 0), (4, 3), (5, 0), (1, 3), (0, 5), (4, 1), (2, 5)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(0, 2), (1, 3), (3, 4), (2, 5), (5, 2), (5, 0), (0, 5), (2, 0)],
+        ![(1, 3), (5, 2), (2, 0), (4, 1), (5, 0), (4, 3), (1, 4), (0, 2)]
+      ],
+      ![
+        ![(2, 5), (3, 1), (3, 4), (0, 5), (1, 3), (5, 2), (0, 2), (1, 4)],
+        ![(0, 2), (5, 2), (1, 3), (5, 0), (4, 1), (0, 5), (2, 5), (2, 0)],
+        ![(1, 3), (2, 5), (0, 5), (1, 4), (5, 0), (3, 4), (3, 1), (2, 0)],
+        ![(1, 4), (2, 0), (5, 2), (5, 0), (0, 5), (2, 5), (4, 3), (0, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 2), (1, 4), (3, 4), (5, 0), (3, 1), (2, 0), (0, 2), (1, 3)]
+      ],
+      ![
+        ![(4, 1), (1, 3), (4, 3), (5, 0), (3, 1), (3, 4), (0, 2), (1, 4)],
+        ![(1, 3), (2, 0), (3, 4), (2, 5), (4, 3), (0, 5), (1, 4), (0, 2)],
+        ![(3, 1), (4, 1), (1, 4), (4, 3), (3, 4), (0, 5), (5, 2), (1, 3)],
+        ![(1, 4), (3, 1), (0, 5), (0, 2), (3, 4), (4, 1), (2, 0), (2, 5)],
+        ![(4, 1), (1, 3), (3, 1), (4, 3), (0, 2), (0, 5), (2, 5), (2, 0)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)]
+      ]
+    ],
+    ![
+      ![
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(2, 5), (3, 0), (4, 3), (1, 2), (3, 4), (1, 5), (5, 2), (4, 0)],
+        ![(1, 5), (4, 0), (3, 4), (2, 1), (4, 3), (2, 5), (5, 1), (3, 0)],
+        ![(5, 2), (5, 1), (1, 2), (2, 5), (3, 4), (2, 1), (1, 5), (0, 3)],
+        ![(5, 1), (5, 2), (2, 1), (1, 5), (3, 0), (1, 2), (2, 5), (0, 4)],
+        ![(5, 2), (3, 0), (4, 0), (5, 1), (4, 3), (2, 1), (1, 2), (3, 4)]
+      ],
+      ![
+        ![(5, 2), (0, 4), (3, 4), (5, 1), (4, 3), (2, 1), (2, 5), (0, 3)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(0, 3), (4, 3), (2, 5), (4, 0), (0, 4), (3, 0), (3, 4), (1, 2)],
+        ![(5, 1), (2, 5), (0, 4), (3, 4), (5, 2), (2, 1), (3, 0), (4, 0)],
+        ![(2, 5), (5, 1), (2, 1), (5, 2), (4, 3), (0, 3), (3, 0), (4, 0)],
+        ![(3, 0), (4, 0), (2, 1), (4, 3), (3, 4), (1, 5), (0, 4), (0, 3)]
+      ],
+      ![
+        ![(5, 1), (0, 3), (4, 3), (5, 2), (3, 4), (1, 2), (1, 5), (0, 4)],
+        ![(3, 4), (3, 0), (0, 4), (1, 5), (5, 2), (4, 0), (0, 3), (2, 1)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(1, 5), (5, 2), (1, 2), (5, 1), (3, 4), (0, 4), (4, 0), (3, 0)],
+        ![(5, 2), (1, 5), (0, 3), (4, 3), (5, 1), (1, 2), (4, 0), (3, 0)],
+        ![(4, 0), (3, 0), (0, 3), (3, 4), (4, 3), (1, 2), (2, 5), (0, 4)]
+      ],
+      ![
+        ![(1, 5), (2, 5), (0, 4), (2, 1), (1, 2), (4, 3), (5, 2), (3, 0)],
+        ![(5, 2), (1, 5), (4, 3), (4, 0), (1, 2), (2, 5), (0, 4), (0, 3)],
+        ![(2, 5), (5, 1), (1, 5), (2, 1), (4, 0), (4, 3), (0, 3), (0, 4)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(2, 1), (2, 5), (5, 1), (0, 3), (1, 5), (3, 4), (5, 2), (1, 2)],
+        ![(5, 1), (0, 4), (4, 3), (1, 2), (0, 3), (2, 1), (5, 2), (4, 0)]
+      ],
+      ![
+        ![(2, 5), (1, 5), (0, 3), (1, 2), (2, 1), (3, 4), (5, 1), (4, 0)],
+        ![(1, 5), (5, 2), (2, 5), (1, 2), (3, 0), (3, 4), (0, 4), (0, 3)],
+        ![(5, 1), (2, 5), (3, 4), (3, 0), (2, 1), (1, 5), (0, 3), (0, 4)],
+        ![(5, 2), (1, 2), (1, 5), (4, 3), (5, 1), (0, 4), (2, 1), (2, 5)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 2), (0, 3), (3, 4), (2, 1), (0, 4), (1, 2), (5, 1), (3, 0)]
+      ],
+      ![
+        ![(1, 2), (3, 4), (4, 3), (2, 1), (0, 4), (1, 5), (2, 5), (0, 3)],
+        ![(5, 1), (0, 3), (3, 4), (1, 2), (0, 4), (4, 3), (3, 0), (4, 0)],
+        ![(5, 2), (0, 4), (4, 3), (1, 5), (0, 3), (3, 4), (4, 0), (3, 0)],
+        ![(2, 5), (4, 0), (3, 0), (2, 1), (3, 4), (1, 2), (1, 5), (0, 4)],
+        ![(1, 5), (3, 0), (4, 0), (1, 2), (4, 3), (2, 1), (2, 5), (0, 3)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)]
+      ]
+    ],
+    ![
+      ![
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 3), (3, 0), (5, 0), (3, 5), (1, 2), (4, 2), (2, 4), (1, 4)],
+        ![(3, 0), (5, 3), (4, 1), (2, 1), (3, 5), (5, 0), (2, 4), (1, 4)],
+        ![(2, 4), (1, 4), (3, 5), (1, 2), (2, 1), (4, 2), (4, 1), (0, 3)],
+        ![(3, 5), (4, 1), (5, 0), (2, 1), (3, 0), (1, 2), (5, 3), (4, 2)],
+        ![(1, 4), (5, 3), (1, 2), (4, 2), (2, 4), (2, 1), (3, 0), (0, 5)]
+      ],
+      ![
+        ![(2, 4), (3, 5), (5, 3), (4, 2), (0, 5), (2, 1), (4, 1), (0, 3)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(2, 4), (3, 5), (0, 3), (1, 2), (5, 0), (3, 0), (5, 3), (0, 5)],
+        ![(3, 5), (4, 2), (2, 1), (5, 0), (4, 1), (0, 5), (3, 0), (2, 4)],
+        ![(5, 3), (0, 3), (2, 1), (0, 5), (5, 0), (3, 5), (3, 0), (1, 4)],
+        ![(4, 1), (5, 3), (3, 0), (2, 4), (5, 0), (2, 1), (4, 2), (0, 3)]
+      ],
+      ![
+        ![(3, 5), (1, 4), (1, 2), (0, 5), (4, 1), (5, 3), (0, 3), (4, 2)],
+        ![(5, 3), (4, 2), (5, 0), (3, 0), (0, 3), (0, 5), (1, 4), (2, 1)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(3, 0), (4, 1), (0, 5), (4, 2), (5, 0), (1, 2), (3, 5), (1, 4)],
+        ![(0, 3), (5, 3), (1, 2), (5, 0), (0, 5), (3, 0), (3, 5), (2, 4)],
+        ![(5, 3), (4, 2), (1, 2), (5, 0), (1, 4), (3, 0), (0, 3), (4, 1)]
+      ],
+      ![
+        ![(4, 1), (4, 2), (2, 1), (0, 5), (1, 2), (3, 0), (2, 4), (1, 4)],
+        ![(2, 4), (5, 3), (0, 5), (1, 2), (5, 0), (1, 4), (4, 2), (0, 3)],
+        ![(5, 3), (1, 4), (2, 4), (5, 0), (2, 1), (0, 5), (0, 3), (4, 1)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 3), (4, 1), (4, 2), (0, 3), (2, 1), (5, 0), (0, 5), (1, 2)],
+        ![(4, 2), (4, 1), (3, 5), (1, 2), (0, 3), (2, 1), (1, 4), (2, 4)]
+      ],
+      ![
+        ![(5, 3), (2, 4), (1, 2), (0, 5), (2, 1), (0, 3), (3, 5), (1, 4)],
+        ![(3, 0), (3, 5), (5, 0), (1, 2), (0, 5), (4, 1), (5, 3), (0, 3)],
+        ![(3, 5), (3, 0), (0, 5), (1, 4), (2, 1), (5, 0), (0, 3), (4, 2)],
+        ![(0, 5), (3, 5), (3, 0), (5, 0), (2, 4), (1, 2), (2, 1), (1, 4)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(0, 3), (1, 4), (5, 3), (2, 1), (5, 0), (1, 2), (3, 0), (2, 4)]
+      ],
+      ![
+        ![(1, 2), (4, 1), (2, 4), (2, 1), (5, 0), (4, 2), (1, 4), (0, 3)],
+        ![(3, 5), (0, 3), (4, 2), (1, 2), (3, 0), (0, 5), (1, 4), (2, 4)],
+        ![(0, 3), (3, 5), (0, 5), (3, 0), (2, 1), (4, 1), (1, 4), (2, 4)],
+        ![(5, 3), (2, 4), (1, 4), (2, 1), (1, 2), (0, 5), (4, 2), (4, 1)],
+        ![(4, 1), (3, 0), (1, 2), (3, 5), (2, 1), (0, 5), (4, 2), (0, 3)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)]
+      ]
+    ],
+    ![
+      ![
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(4, 0), (5, 4), (3, 2), (1, 2), (4, 5), (5, 0), (1, 3), (2, 3)],
+        ![(5, 4), (4, 0), (5, 0), (4, 5), (2, 1), (3, 1), (1, 3), (2, 3)],
+        ![(4, 5), (3, 2), (5, 0), (1, 2), (4, 0), (2, 1), (5, 4), (3, 1)],
+        ![(1, 3), (2, 3), (4, 5), (2, 1), (1, 2), (3, 1), (3, 2), (0, 4)],
+        ![(3, 1), (2, 1), (4, 0), (2, 3), (3, 2), (1, 3), (1, 2), (0, 5)]
+      ],
+      ![
+        ![(4, 5), (2, 3), (2, 1), (0, 5), (3, 2), (5, 4), (0, 4), (3, 1)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 0), (5, 4), (4, 0), (1, 2), (2, 3), (0, 4), (4, 5), (0, 5)],
+        ![(0, 4), (5, 4), (3, 2), (5, 0), (0, 5), (2, 1), (4, 5), (1, 3)],
+        ![(4, 0), (3, 2), (0, 5), (3, 1), (5, 0), (2, 1), (4, 5), (2, 3)],
+        ![(5, 4), (3, 1), (2, 1), (5, 0), (2, 3), (4, 0), (0, 4), (3, 2)]
+      ],
+      ![
+        ![(1, 3), (4, 5), (5, 4), (3, 1), (0, 5), (1, 2), (3, 2), (0, 4)],
+        ![(4, 5), (0, 5), (3, 2), (0, 4), (4, 0), (1, 3), (5, 0), (2, 1)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(5, 4), (0, 4), (3, 1), (0, 5), (5, 0), (1, 2), (4, 0), (2, 3)],
+        ![(4, 5), (3, 1), (1, 2), (5, 0), (3, 2), (0, 5), (4, 0), (1, 3)],
+        ![(3, 2), (5, 4), (4, 0), (1, 3), (5, 0), (1, 2), (3, 1), (0, 4)]
+      ],
+      ![
+        ![(5, 4), (1, 3), (2, 1), (0, 5), (1, 2), (0, 4), (4, 5), (2, 3)],
+        ![(4, 5), (4, 0), (0, 5), (1, 2), (2, 3), (5, 0), (0, 4), (3, 1)],
+        ![(4, 0), (4, 5), (5, 0), (1, 3), (0, 5), (3, 2), (5, 4), (0, 4)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(4, 5), (1, 3), (2, 3), (4, 0), (2, 1), (5, 0), (0, 5), (1, 2)],
+        ![(0, 4), (2, 3), (5, 4), (1, 2), (5, 0), (2, 1), (4, 0), (1, 3)]
+      ],
+      ![
+        ![(3, 2), (3, 1), (4, 0), (1, 2), (0, 5), (2, 1), (1, 3), (2, 3)],
+        ![(5, 4), (2, 3), (1, 3), (5, 0), (1, 2), (0, 5), (0, 4), (3, 2)],
+        ![(1, 3), (5, 4), (0, 5), (2, 1), (5, 0), (2, 3), (3, 1), (0, 4)],
+        ![(0, 5), (5, 4), (0, 4), (5, 0), (3, 2), (1, 2), (2, 1), (3, 1)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)],
+        ![(3, 1), (3, 2), (2, 1), (0, 4), (1, 2), (4, 5), (2, 3), (1, 3)]
+      ],
+      ![
+        ![(1, 2), (5, 0), (3, 2), (1, 3), (0, 4), (2, 3), (3, 1), (2, 1)],
+        ![(0, 4), (4, 5), (0, 5), (4, 0), (1, 2), (3, 2), (2, 3), (1, 3)],
+        ![(4, 5), (0, 4), (3, 1), (2, 1), (4, 0), (0, 5), (2, 3), (1, 3)],
+        ![(3, 2), (4, 0), (2, 1), (4, 5), (1, 2), (0, 5), (3, 1), (0, 4)],
+        ![(2, 3), (1, 3), (1, 2), (5, 4), (2, 1), (0, 5), (3, 1), (3, 2)],
+        ![(0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0), (0, 0)]
+      ]
+    ]
+  ]
+end MacMahon
diff --git a/LeanPool/projects/macmahon-min-universal-sets.yaml b/LeanPool/projects/macmahon-min-universal-sets.yaml
new file mode 100644
index 0000000000..f3b3fbc500
--- /dev/null
+++ b/LeanPool/projects/macmahon-min-universal-sets.yaml
@@ -0,0 +1,62 @@
+slug: macmahon-min-universal-sets
+title: The ten minimum universal collections of MacMahon cubes
+summary: >-
+  Classifies all minimum universal inventories of six-coloured MacMahon cubes.
+  A universal inventory can build a two-by-two-by-two model of every cube variety,
+  with matching exterior faces and eight distinct physical copies. The minimum
+  inventory size is twelve, exactly ten labelled inventories attain it, and they
+  are precisely the two-triangle collections in Conway's tableau. Natural-number
+  multiplicities are allowed; every minimum inventory has no repeated variety.
+  The tableau has zero diagonal; its thirty off-diagonal entries are the varieties.
+  The development also verifies all proper signed-axis rotations, the thirty
+  varieties, all six-colour face assignments, and the equivalence of corner
+  matching with physical face matching. This resolves Johnson and Roldán's
+  Conjectures 4 and 8 (arXiv:2407.13208v1), with a stronger multiset conclusion.
+branch: combinatorics
+entry_module: LeanPool.MacMahon
+authors:
+- Jason Davies
+source:
+  url: https://github.com/jasondavies/macmahon-min-universal-sets/tree/d8856c97e43e6fa66383c81b8ac4f5bd1c285bc8
+  github_repo: jasondavies/macmahon-min-universal-sets
+  commit: d8856c97e43e6fa66383c81b8ac4f5bd1c285bc8
+license: Apache-2.0
+status: verified
+provenance: AI
+main_declarations:
+- MacMahon.minimum_size
+- MacMahon.physical_exactly_ten
+main_results:
+- declaration: MacMahon.minimum_size
+  informal: Twelve is the attained minimum size of a universal physical inventory.
+- declaration: MacMahon.physical_minimum
+  informal: Every universal physical inventory has at least twelve cubes.
+- declaration: MacMahon.physical_exactly_ten
+  informal: Exactly ten labelled universal physical inventories have size twelve.
+- declaration: MacMahon.physical_iff_two_triangles
+  informal: >-
+    An inventory of twelve cubes is physically universal exactly when its Conway
+    tableau is the two disjoint triangles of a partition of the six labels into
+    two triples, with one copy of each directed edge.
+- declaration: MacMahon.physical_minimum_has_no_repeats
+  informal: Every variety has multiplicity at most one in a minimum universal inventory.
+- declaration: MacMahon.proper_rotation_iff
+  informal: The rotation table contains precisely all proper signed-axis rotations.
+- declaration: MacMahon.exposed_face_rule
+  informal: The outward faces at each of the eight positions obey the coordinate sign rule.
+- declaration: MacMahon.face_colours_valid
+  informal: Every off-diagonal tableau entry assigns the six distinct nonzero colours.
+- declaration: MacMahon.face_assignment_coverage
+  informal: Every assignment of six distinct nonzero colours is a rotated tableau variety.
+- declaration: MacMahon.face_assignment_unique
+  informal: The variety and proper rotation representing a face assignment are unique.
+tags:
+- combinatorics
+- coloured-cubes
+- classification
+- finite-geometry
+msc:
+- 05A15
+- 05C70
+- 68V15
+- 00A08