IR022 — Exponential addition and integer powers

For fixed rational-sequence arguments with supplied enclosures, exp(x+z)=exp(x)*exp(z), exp(0)=1, and exp(j*x)=exp(x)^j, witnessed to every finite accuracy.

Method: native-induction. Induction: j and precision. Risk: high.

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

Planned prerequisites and notation

• IR012 — Approximation operations without real sorts
• IR020 — Exponential explicit tail
• IR021 — Finite binomial convolution
• IRD08 — ExpPartial