TR001 — Integer polynomial evaluation stability

For P over Z, x,y in [1,2], |P(x)-P(y)|<=M_P*|x-y|, where M_P=1+sum(j>=1,j*abs(a_j)*2^(j-1)); zero/trailing-zero encodings handled.

Method: native-induction. Induction: degree. Risk: routine.

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

Planned prerequisites and notation

• IR009 — Power difference factorization
• IR005 — Finite rational folds
• IR026 — Canonical approximation accuracy
• IRD25 — IntegerPolynomial
• IRD26 — TransCert