IR046 — Nonzero quadratic products

A finite product of nonzero quadratic elements is nonzero, by norm multiplicativity and integer no-zero-divisors.

Method: native-induction. Induction: factor count. Risk: routine.

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

Planned prerequisites and notation

• IR030 — Quadratic equality is decidable
• IR031 — Norm identity and multiplicativity
• IR005 — Finite rational folds
• IRD13 — QuadNorm

Checked supporting leaves, not parent closure

• QF001 — Nonvanishing finite quadratic product traces
• QN001 — Nonzero quadratic-integer products
• SI001 — Nonzero signed-integer products

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