IR033 — Quadratic powers and coefficient height

For integer pair (A,B), powers have integer-pair traces; weighted height h(A,B)=|A|+2|B| is submultiplicative and h(i,j)<=3q for i,j<q.

Method: native-induction. Induction: power exponent. Risk: routine.

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

Planned prerequisites and notation

• IR029 — Quadratic ring operations
• IR005 — Finite rational folds
• IR004 — Absolute value and interval arithmetic
• IRD12 — QuadMul
• IRD15 — Frequency