The recurrence of IR079 uniquely determines coefficients and agrees with (1+z)/(1-z)=1+2*sum(j>=1,z^j). Prove by induction on the coefficient index, with positive integer division justified.
Method: native-induction. Induction: coefficient index. Risk: high.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.