Super power sums from hook vanishing

The full symmetric-function lemma (Lemma A.9 of the accompanying paper): a sequence whose determinant Schur specialization vanishes on every Young diagram outside the (a, b) hook is a difference of power sums of two disjoint multisets of nonzero complex numbers, of sizes at most a and b.

This is the composition of exists_recurrence_of_schurDet_vanishing (RecurrenceFromVanishing.lean) with superPowerSums_of_recurrence (RationalityFromRecurrence.lean), through the list↔diagram bridge of Common/YoungDiagrams.lean.

theorem RS.superPowerSums_of_hook_vanishing {t : ℕ → ℂ} {a b : ℕ} (hvan : ∀ (μ : YoungDiagram), ¬IsInHook a b μ → diagramSchur μ t = 0) : ∃ (α : Multiset ℂ) (β : Multiset ℂ), α.card ≤ a ∧ β.card ≤ b ∧ (∀ x ∈ α, x ≠ 0) ∧ (∀ x ∈ β, x ≠ 0) ∧ (∀ x ∈ α, x ∉ β) ∧ ∀ (m : ℕ), 1 ≤ m → t m = (Multiset.map (fun (x : ℂ) => x ^ m) α).sum - (Multiset.map (fun (x : ℂ) => x ^ m) β).sum

Lemma A.9: if the Schur specialization of t vanishes on every diagram outside the (a, b) hook, then t is a super power sum: a difference of power sums of disjoint multisets of nonzero complex numbers of sizes at most a and b.

theorem RS.powerSums_zero_of_hook_and_eventually_zero {t : ℕ → ℂ} {a b : ℕ} (hvan : ∀ (μ : YoungDiagram), ¬IsInHook a b μ → diagramSchur μ t = 0) (hev : ∃ (N₀ : ℕ), ∀ (m : ℕ), N₀ ≤ m → t m = 0) (m : ℕ) : 1 ≤ m → t m = 0

The nilpotent-trace engine: a sequence whose Schur specialization vanishes outside a hook and which is eventually zero vanishes identically from degree 1 onward. (Lemmas A.9 and A.10 composed; the categorical nilpotent-trace theorem instantiates t m with the traces of the powers of a nilpotent endomorphism.)