Recurrence from Schur-determinant vanishing

Given a power-sum sequence t whose determinant Schur specialisation vanishes on sufficiently wide single-row extensions, the complete-homogeneous sequence newtonHZ t satisfies a nontrivial linear recurrence. This is the algebraic core of the argument that hook confinement forces a nilpotent trace.

The proof proceeds in three stages:

1. Determinant vanishing — the vanishing hypothesis hvan yields det = 0 for every matrix of the form (fun i j : Fin (a+1) => newtonHZ t (ρ i + 1 + j)) whenever the row-shifts ρ take integer values ≥ b − a. Negative degrees evaluate to zero.

2. Finite rank — the span of the vectors v ρ := (fun k => newtonHZ t (ρ + 1 + k)) for ρ ≥ b − a has finrank ≤ a (a proper subspace of Fin (a+1) → ℂ).

3. Annihilator extraction — a nonzero linear functional vanishing on that span is converted to the coefficient vector c of the recurrence.

Stage 1: determinant vanishing from Schur vanishing

Stage 2: linear dependence and finite-rank bound

Stage 3: extracting the recurrence

theorem RS.exists_recurrence_of_schurDet_vanishing {t : ℕ → ℂ} {a b : ℕ} (hvan : ∀ (w : List ℕ), w.SortedGE → (∀ x ∈ w, 0 < x) → w.length = a + 1 → b + 1 ≤ w.getD a 0 → schurDet t w = 0) : ∃ (c : Fin (a + 1) → ℂ), c ≠ 0 ∧ ∀ (ρ : ℤ), ↑b - ↑a ≤ ρ → ∑ k : Fin (a + 1), c k * newtonHZ t (ρ + 1 + ↑↑k) = 0

Schur-determinant vanishing on wide single-row extensions forces the complete-homogeneous sequence to satisfy a nontrivial linear recurrence.