The signed double-sum identity

Combining the bialternant, the diagonal coefficient, the staircase expansion, and the Jacobi–Trudi Leibniz expansion: the signed double sum of guarded coefficients of complete homogeneous products equals 1. This is the polynomial form of the orthonormality ⟨χ_μ, χ_μ⟩ = 1.

noncomputable def RS.diagExp {k : ℕ} (v : Fin k → ℕ) : Fin k →₀ ℕ

The diagonal staircase exponent of a shape.

Equations

• RS.diagExp v = ∑ i : Fin k, Finsupp.single i (v i + (k - 1 - ↑i))

theorem RS.t_identity {k : ℕ} (v : Fin k → ℕ) (hinj : Function.Injective fun (i : Fin k) => v i + (k - 1 - ↑i)) : (∑ τ : Equiv.Perm (Fin k), ↑↑(Equiv.Perm.sign τ) * if stairShift τ ≤ diagExp v then ∑ σ : Equiv.Perm (Fin k), ↑↑(Equiv.Perm.sign σ) * if ∀ (i : Fin k), 0 ≤ ↑(v i) + ↑↑(σ i) - ↑↑i then (∏ i : Fin k, hSub Finset.univ (↑(v i) + ↑↑(σ i) - ↑↑i).toNat).coeff (diagExp v - stairShift τ) else 0 else 0) = 1

The signed double-sum identity.