For L given by IR017, specialize IR079-81 at z=1/3 to obtain exp(L)=2. Do not assume this identity in Log2Partial or appeal to an imported real logarithm.
Method: native-induction. Induction: finite coefficient identities and explicit precision. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.
Planned prerequisites and notation
- IR017 — Logarithm series remainder
- IR020 — Exponential explicit tail
- IR021 — Finite binomial convolution
- IR022 — Exponential addition and integer powers
- IR079 — Formal atanh/exponential coefficient recurrence
- IR080 — Formal recurrence identifies rational series
- IR081 — Composition-tail bound at one third
- IRD07 — Log2Partial
- IRD08 — ExpPartial