IR020 — Exponential explicit tail

For x>=0 and N+2>=2*x, bound each finite tail beyond N by 2*x^(N+1)/(N+1)!; give an explicit N(x,t) making this <2^-t. Handle x=0 separately.

Method: native-induction. Induction: tail length and precision schedule. 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
• IR010 — Geometric tail arithmetic
• IR011 — Factorial lower bounds
• IR006 — Dyadic domination
• IRD08 — ExpPartial