IR021 — Finite binomial convolution

The degree<=N coefficients of ExpPartial(x+z,N) equal the corresponding convolution coefficients of ExpPartial(x,N)*ExpPartial(z,N); bound the discarded terms explicitly.

Method: native-induction. Induction: N. Risk: high.

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

Planned prerequisites and notation

• IR009 — Power difference factorization
• IR019 — Exponential partial-sum totality
• IR020 — Exponential explicit tail
• IRD08 — ExpPartial