Two separate component equations
These local conservative aliases abbreviate the real and radical coordinate balances in Z[√2]. They do not assert multiplication totality or norm multiplicativity. Each is a primitive equation, with no definition prerequisite and no global registry mutation. Six existing rational aliases and ND0157 are unchanged.
The separate relations preserve the exact two implication premises of the checked theorem; they are not silently replaced by a single conjunction premise.
ND0388 — IQuadProductReal
The signed pair rp,rn represents the real component AC+2BD of (A+B sqrt(2))(C+D sqrt(2)).
Parameters: ap, an, bp, bn, cp, cn, dp, dn, rp, rn.
rp + (ap · cn + an · cp + 2 · (bp · dn + bn · dp)) = ap · cp + an · cn + 2 · (bp · dp + bn · dn) + rnChecked theorems using this exact expansion: SN003 · RN002 · QN001.
ND0389 — IQuadProductRadical
The signed pair sp,sn represents the radical component AD+BC of (A+B sqrt(2))(C+D sqrt(2)).
Parameters: ap, an, bp, bn, cp, cn, dp, dn, sp, sn.
sp + (ap · dn + an · dp + (bp · cn + bn · cp)) = ap · dp + an · dn + (bp · cp + bn · cn) + snChecked theorems using this exact expansion: SN003 · RN002 · QN001.
Full local definition network · Checked arithmetic DAG · Exact definitions and typed uses.