Decode quadratic triples; z represents ((A*C+2*B*E)+(A*E+B*C)*sqrt2)/(D*F). Equality is of coefficients after cross multiplication.
Proposed arity: 3. Parameters: x y z. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.