(A+B*sqrt2)/D=0 iff A=B=0; equality of two triples is equivalent to two signed integer equalities after clearing denominators.
Method: native-order. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.