For M=7r, C_jk=L0^(-(M-k))*c_jk with rational denominator dividing720^M. Therefore M!*(720*L0)^M times the IR056 identity is polynomial; include the Taylor degree factorial to clear Taylor coefficients. Record every nonzero denominator and its lower bound.
Method: native-induction. Induction: truncated inverse-product coefficients. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.