The natural dimension identity and square staircases

The dimension identity nDim S₀ · ∏ eᵢ! = n! · ∏∏ diffs at the natural-number level, the staircase evaluation for square diagrams, and the elementary factorial bounds feeding the square growth estimate.

theorem RS.dim_mul_eq (μ : YoungDiagram) (S₀ : Submodule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card)))) (hchar : ∀ (π : Equiv.Perm (Fin μ.card)), jtChar μ π = nChar S₀ π) : nDim S₀ * ∏ i : Fin μ.rowLens.length, (eStair μ i).factorial = μ.card.factorial * ∏ i : Fin μ.rowLens.length, ∏ j > i, (eStair μ (Fin.revPerm j) - eStair μ (Fin.revPerm i))

The natural dimension identity.

theorem RS.square_rowLens_length (s : ℕ) : (squareDiagram s).rowLens.length = s

The square diagram has s rows.

theorem RS.eStair_square (s : ℕ) (i : Fin (squareDiagram s).rowLens.length) : eStair (squareDiagram s) i = s + (s - 1 - ↑i)

The square staircase evaluates to 2s − 1 − i.

theorem RS.Ioi_prod_sub {L : ℕ} (i : Fin L) : ∏ j > i, (↑j - ↑i) = (L - 1 - ↑i).factorial

Interval products are factorials.

theorem RS.factorial_add_le (d r : ℕ) : (d + r).factorial ≤ (d + r) ^ r * d.factorial

Adding r to the argument multiplies the factorial by at most (d+r)^r.

theorem RS.shifted_factorial_le (s d : ℕ) (hd : d < s) : (s + d).factorial ≤ (2 * s) ^ s * d.factorial

The shifted factorial bound: (s+d)! ≤ (2s)^s · d! for d < s.