Symmetry of degree-two inventories

theorem MacMahon.entry_le_row (a : Inventory) (i j : Label) : a (i, j) ≤ row a i

theorem MacMahon.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 : Label) : a (i, l) = if l = j ∨ l = k then 1 else 0

Two unit entries exhaust a row of total multiplicity two.

theorem MacMahon.symmetric_of_degree_two (a : Inventory) (hr : ∀ (i : Label), row a i = 2) (hc : ∀ (i : Label), col a i = 2) (hb : ∀ (i j : Label), a (j, i) ≤ 2 * a (i, j)) (i j : Label) : a (i, j) = a (j, i)

Degree two and reciprocal support force reciprocal multiplicities.