For each t<N construct P_t(X)=product(u<N,u!=t,X-lambda_u), its coefficient list of degree<N, and prove evaluation at every frequency. No determinant library is required.
Method: native-induction. Induction: finite factor-list length. Risk: high.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.