If all true exponential jets below r vanish at every node, then |F^(r)(x_ell0)| <= r!*12^r/(7r)! * N*B*(3q)^(7r)*2^(15q). Nodes lie in [0,3], so exp(9q)<3^(9q)<2^(15q). Derive via IR056/58, not Rolle or compactness.
Method: native-order. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.
Planned prerequisites and notation
- IR054 — Finite exponential divided-difference estimate
- IR056 — Finite confluent interpolation identity
- IR057 — Explicit interpolation coefficient bound
- IR058 — Polynomial-to-exponential tail transfer
- IR022 — Exponential addition and integer powers
- IR023 — Exponential order and Lipschitz
- IRD16 — AuxJet
- IRD21 — ConfluentFunctional