For natural A,B, A²=2*B² implies A=B=0; signed versions follow by absolute values. Replay in HA, not merely the separate Lean demo.
Method: native-induction. Induction: strong induction on A+B. Risk: reuse-audit.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.