The exact dimension determinant

Row-normalizing the Jacobi–Trudi determinant at the delta sequence by the staircase factorials turns its entries into descending Pochhammer evaluations; reversing both indices removes all signs and evaluates the determinant as a manifestly positive Vandermonde product of staircase differences.

noncomputable def RS.eStair (μ : YoungDiagram) (i : Fin μ.rowLens.length) : ℕ

The staircase exponents of a diagram over its own row count.

Equations

• RS.eStair μ i = μ.rowLens.get i + (μ.rowLens.length - 1 - ↑i)

theorem RS.diagramSchur_delta_mul (μ : YoungDiagram) : diagramSchur μ deltaSeq * ∏ i : Fin μ.rowLens.length, ↑(eStair μ i).factorial = ∏ i : Fin μ.rowLens.length, ∏ j > i, (↑(eStair μ (Fin.revPerm j)) - ↑(eStair μ (Fin.revPerm i)))

The row-normalized dimension determinant: the Jacobi–Trudi determinant at the delta sequence times the staircase factorials is the Vandermonde product of the staircase differences.