IR062 — Growth on the interpolation interval

For 0<=t<=3, frequencies<=3q and |beta|<=B, bound the derivative-order-7r series by N*B*(3q)^(7r)*2^(15q), using e<3 and 3^9<2^15.

Method: native-order. Induction: none. Risk: routine.

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

Planned prerequisites and notation

• IR023 — Exponential order and Lipschitz
• IR033 — Quadratic powers and coefficient height
• IR043 — Auxiliary low jets vanish algebraically
• IR058 — Polynomial-to-exponential tail transfer
• IRD16 — AuxJet
• IRD08 — ExpPartial