IR054 — Finite exponential divided-difference estimate

Apply IR051-53 to ExpPartial(lambda*t,J): for nodes in [0,M] and lambda>=0, its order-N functional is bounded by lambda^N/N!*ExpPartial(lambda*M,max(J-N,0)), with J<N handled separately.

Method: native-induction. Induction: finite polynomial degree. Risk: critical.

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

Planned prerequisites and notation

• IR019 — Exponential partial-sum totality
• IR051 — Monomial divided differences
• IR052 — Homogeneous-sum enclosure
• IR053 — Factorial-binomial cancellation
• IRD08 — ExpPartial
• IRD21 — ConfluentFunctional