The sign resolution

The Jacobi–Trudi character degree is a ratio of positive naturals, so in the ±-dichotomy of jtChar_pm_simple only the positive sign survives: the Jacobi–Trudi character IS a native character.

theorem RS.eStair_strictAnti (μ : YoungDiagram) {i j : Fin μ.rowLens.length} (hij : i < j) : eStair μ j < eStair μ i

The staircase exponents strictly decrease.

theorem RS.jtChar_one_pos_identity (μ : YoungDiagram) : ∃ (N : ℕ) (D : ℕ), 0 < N ∧ 0 < D ∧ ↑D * jtChar μ 1 = ↑N

Positivity of the degree: a positive natural multiple of jtChar μ 1 is a positive natural.

theorem RS.jtChar_eq_nChar (μ : YoungDiagram) : ∃ (S₀ : Submodule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card)))), IsSimpleModule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) ↥S₀ ∧ ∀ (π : Equiv.Perm (Fin μ.card)), jtChar μ π = nChar S₀ π

The Jacobi–Trudi character is a native character.