A,B are witnessed signed integers and D>0; denotes (A+B*sqrt2)/D. sqrt2 is semantic shorthand only, not a kernel term.
Proposed arity: 3. Parameters: A B D. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.