Guard and margin bridges for the double-sum identity

The staircase guard of the double-sum identity matches the signed nonnegativity guard of the Jacobi–Trudi character, the shifted margins match the shifted compositions, and sorted shapes have injective staircase exponents.

theorem RS.diagExp_apply {k : ℕ} (v : Fin k → ℕ) (j : Fin k) : (diagExp v) j = v j + (k - 1 - ↑j)

The staircase-shifted exponent at a row.

theorem RS.stair_guard_iff {k : ℕ} (v : Fin k → ℕ) (τ : Equiv.Perm (Fin k)) : stairShift τ ≤ diagExp v ↔ ∀ (i : Fin k), 0 ≤ ↑(v i) + ↑↑(τ i) - ↑↑i

The staircase guard is the signed nonnegativity guard.

theorem RS.stair_margin_eq {k : ℕ} (v : Fin k → ℕ) (τ : Equiv.Perm (Fin k)) (h : stairShift τ ≤ diagExp v) (j : Fin k) : (diagExp v - stairShift τ) j = (↑(v j) + ↑↑(τ j) - ↑↑j).toNat

The shifted margin is the shifted composition.

theorem RS.staircase_injective {k : ℕ} (v : Fin k → ℕ) (hsort : ∀ (i j : Fin k), i ≤ j → v j ≤ v i) : Function.Injective fun (i : Fin k) => v i + (k - 1 - ↑i)

Sorted shapes have injective staircase exponents.