The minimum inventory size and tight degree bounds

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

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

theorem MacMahon.total_rows (a : Inventory) : total a = ∑ i : Label, row a i

theorem MacMahon.total_cols (a : Inventory) : total a = ∑ j : Label, col a j

theorem MacMahon.universal_row_bound (a : Inventory) (hz : DiagonalZero a) (h : Universal a) (i : Label) : 3 * row a i + 40 ≤ 4 * total a

theorem MacMahon.universal_col_bound (a : Inventory) (hz : DiagonalZero a) (h : Universal a) (j : Label) : 3 * col a j + 40 ≤ 4 * total a

theorem MacMahon.universal_minimum (a : Inventory) (hz : DiagonalZero a) (h : Universal a) : 12 ≤ total a

theorem MacMahon.eq_two_of_le_of_sum (f : Label → ℕ) (hb : ∀ (i : Label), f i ≤ 2) (hs : ∑ i : Label, f i = 12) (i : Label) : f i = 2

If a finite sum attains the sum of pointwise upper bounds, all bounds are tight.

theorem MacMahon.rows_two (a : Inventory) (hz : DiagonalZero a) (h : Universal a) (ht : total a = 12) (i : Label) : row a i = 2

theorem MacMahon.cols_two (a : Inventory) (hz : DiagonalZero a) (h : Universal a) (ht : total a = 12) (i : Label) : col a i = 2

theorem MacMahon.reverse_bound (a : Inventory) (hz : DiagonalZero a) (h : Universal a) (ht : total a = 12) (i j : Label) : a (j, i) ≤ 2 * a (i, j)