IR081 — Composition-tail bound at one third

For z=1/3, construct finite truncation degrees making the difference between exp(A(z)), the finite formal composition and the rational-series truncation smaller than any dyadic error. Bound the outer exponential tail, inner atanh tail and positive omitted coefficient mass separately.

Method: native-induction. Induction: explicit tail schedules. Risk: critical.

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

Planned prerequisites and notation

• IR080 — Formal recurrence identifies rational series
• IR017 — Logarithm series remainder
• IR020 — Exponential explicit tail
• IR010 — Geometric tail arithmetic
• IR023 — Exponential order and Lipschitz
• IR012 — Approximation operations without real sorts
• IRD07 — Log2Partial
• IRD08 — ExpPartial