Classification of minimum universal inventories

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.

def MacMahon.relabel (e : Equiv.Perm Label) (a : Inventory) : Inventory

Pull an inventory back along a permutation of the tableau labels.

Equations

• MacMahon.relabel e a p = a (e p.1, e p.2)

theorem MacMahon.row_relabel (e : Equiv.Perm Label) (a : Inventory) (i : Label) : row (relabel e a) i = row a (e i)

theorem MacMahon.partition_sum_relabel (e : Equiv.Perm Label) (a : Inventory) (s : Finset Label) : ∑ p : Pair, twoTriangles s p * relabel e a p = ∑ p : Pair, twoTriangles (Finset.map (Equiv.toEmbedding e) s) p * a p

theorem MacMahon.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

theorem MacMahon.no_normalized_doubled_edge (a : Inventory) (hz : DiagonalZero a) (hr : ∀ (i : Label), row a i = 2) (hs : ∀ (i j : Label), a (i, j) = a (j, i)) (hp : ∀ (b : Fin 10), 0 < ∑ p : Pair, winner b p * a p) : a (0, 1) ≠ 2

Partition cover excludes a doubled edge at the normalized position 01.

theorem MacMahon.normalized_triangle_closes (a : Inventory) (hz : DiagonalZero a) (hr : ∀ (i : Label), row a i = 2) (hs : ∀ (i j : Label), 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

Two unit edges from 0 must close to the triangle on labels 0, 1 and 2.

theorem MacMahon.classify_degree_two (a : Inventory) (hz : DiagonalZero a) (hr : ∀ (i : Label), row a i = 2) (hs : ∀ (i j : Label), a (i, j) = a (j, i)) (hp : ∀ (b : Fin 10), 0 < ∑ p : Pair, winner b p * a p) : ∃ (b : Fin 10), a = winner b

Complete classification using two local configurations, up to relabelling.