IR035 — Cleared rational quadratic lower bound

If D>0 and D*g=A+B*sqrt2!=0, then |g|>=1/(D*(|A|+2|B|)); do not conflate the denominator D with a square or omit it.

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

• IR032 — Integral quadratic norm separation
• IR004 — Absolute value and interval arithmetic
• IRD11 — QuadRep
• IRD13 — QuadNorm