IR047 — Bounded nonzero jet at zero

For nonzero beta and distinct frequencies, some k<N satisfies sum beta_j*lambda_j^k !=0. Use IR045 at a nonzero coefficient and bounded decidable search; no determinant or infinite-series argument.

Method: native-search. Induction: none. Risk: high.

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

Planned prerequisites and notation

• IR034 — Distinct frequencies with quantitative gap
• IR045 — Moment polynomial identity
• IR046 — Nonzero quadratic products
• IR043 — Auxiliary low jets vanish algebraically
• IR008 — Bounded decidable minimum
• IRD16 — AuxJet