Positivity of the restriction pairing #
The pairing restrPairing lam mu is nonzero whenever lam ≤ mu,
bridging the combinatorial Pieri chain to the representation-theoretic
branching sandwich.
theorem
RS.restrPairing_ne_zero
(Hpad :
∀ (μ : YoungDiagram) {k : ℕ},
μ.rowLens.length ≤ k →
∀ (π : Equiv.Perm (Fin μ.card)),
jtChar μ π = ∑ σ : Equiv.Perm (Fin k),
↑↑(Equiv.Perm.sign σ) * if ∀ (i : Fin k), 0 ≤ ↑(μ.rowLen ↑i) + ↑↑(σ i) - ↑↑i then
↑(colourChar (fun (i : Fin k) => (↑(μ.rowLen ↑i) + ↑↑(σ i) - ↑↑i).toNat) π)
else 0)
(lam mu : YoungDiagram)
(hle : lam ≤ mu)
(h : lam.card ≤ mu.card)
:
The restriction pairing is nonzero whenever one diagram contains the other, by the Pieri chain's positivity.