IR031 — Norm identity and multiplicativity

N(x)=x*conj(x)=(A²-2B²)/D² and N(x*y)=N(x)*N(y).

Method: native-ring. Induction: none. 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
• IRD13 — QuadNorm

Checked supporting leaves, not parent closure

• RN001 — Rational norm representative independence
• RN002 — Rational quadratic norm multiplication
• SN003 — Signed quadratic norm multiplicativity

The planning contract above remains open. Checked arithmetic DAG · Complete execution evidence.