IR079 — Formal atanh/exponential coefficient recurrence

Let A(z)=2*sum(j>=0,z^(2j+1)/(2j+1)) as finite coefficient tables. Formal exp(A) has F(0)=1 and (1-z²)F'=2F coefficientwise to each finite degree; composition only uses finitely many positive-degree terms.

Method: native-induction. Induction: coefficient degree. Risk: critical.

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

Planned prerequisites and notation

• IR005 — Finite rational folds
• IR019 — Exponential partial-sum totality
• IR021 — Finite binomial convolution
• IR077 — Finite Taylor derivative identity
• IRD07 — Log2Partial
• IRD08 — ExpPartial

Checked supporting leaves, not parent closure

• CV001 — Universal natural convolution vanishing

The planning contract above remains open. Checked arithmetic DAG · Complete execution evidence.