IR032 — Integral quadratic norm separation

If A,B are integers not both zero, abs(A²-2B²)>=1; hence |A+B*sqrt2|>=1/(|A|+2*|B|). Denominator is positive.

Method: native-order. Induction: none. Risk: routine.

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

Planned prerequisites and notation

• IR016 — Even-square descent
• IR030 — Quadratic equality is decidable
• IR031 — Norm identity and multiplicativity
• IR015 — Sqrt2 algebra and strict bounds
• IR004 — Absolute value and interval arithmetic
• IRD13 — QuadNorm

Checked supporting leaves, not parent closure

• SN001 — Signed quadratic-norm zero criterion
• SN002 — Witnessed integer norm separation

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