IR045 — Moment polynomial identity

Writing P_t=sum(k<N,p_tk*X^k), prove sum(k<N,p_tk*A_(0,k))=beta_t*product(u!=t,lambda_t-lambda_u) by finite sum interchange and polynomial evaluation.

Method: native-induction. Induction: finite double sums. Risk: high.

This is a human-readable planning contract, not a parsed kernel formula or accepted proof.

Planned prerequisites and notation

• IR044 — Annihilating polynomial construction
• IR005 — Finite rational folds
• IR029 — Quadratic ring operations
• IRD15 — Frequency
• IRD16 — AuxJet