Schur specialisations at super power sums are multiplicities

The additive splitting identity decomposes superPS p q as superPS p 0 + superPS 0 q; both one-sided values are intertwiner dimensions, and the induction multiplicities are natural numbers, so every Schur specialisation at a super power sum is a natural number — the full nonnegativity input for the hook arguments of Deligne 1.10/1.12.

theorem RS.exists_nat_sum {ι : Type u_1} (s : Finset ι) (f : ι → ℂ) (h : ∀ i ∈ s, ∃ (m : ℕ), f i = ↑m) : ∃ (M : ℕ), ∑ i ∈ s, f i = ↑M

A finite sum of natural values is a natural value.

theorem RS.diagramSchur_superPS_exists_nat (p q : ℕ) (lam : YoungDiagram) : ∃ (m : ℕ), diagramSchur lam (superPS p q) = ↑m

Schur specialisations at super power sums are natural numbers: the two-sided value splits into one-sided multiplicities through the additive identity.