SN003 — Signed quadratic norm multiplicativity

Named statement

forall ap an bp bn cp cn dp dn rp rn sp sn a b c d r t.
  SignedDifferenceSquare(ap,an,a) ->
  SignedDifferenceSquare(bp,bn,b) ->
  SignedDifferenceSquare(cp,cn,c) ->
  SignedDifferenceSquare(dp,dn,d) ->
  SignedDifferenceSquare(rp,rn,r) ->
  SignedDifferenceSquare(sp,sn,t) ->
  IQuadProductReal(ap,an,bp,bn,cp,cn,dp,dn,rp,rn) ->
  IQuadProductRadical(ap,an,bp,bn,cp,cn,dp,dn,sp,sn) ->
  r+2*(a*d+b*c)=(a*c+(2*2)*(b*d))+2*t

This proves N(xy)=N(x)N(y) in Z[√2], including transport to arbitrary signed output representatives. It rechecks actual signed-square product, scaling, sum, and cross-interchange proof bodies. Three small deterministic ring helpers replace normalization of the entire eighteen-variable formula. No rational denominator or real-number interpretation is claimed.

forall ap an bp bn cp cn dp dn rp rn sp sn a b c d r t. ap*ap+an*an=a+(ap*an+an*ap) -> bp*bp+bn*bn=b+(bp*bn+bn*bp) -> cp*cp+cn*cn=c+(cp*cn+cn*cp) -> dp*dp+dn*dn=d+(dp*dn+dn*dp) -> rp*rp+rn*rn=r+(rp*rn+rn*rp) -> sp*sp+sn*sn=t+(sp*sn+sn*sp) -> rp+((ap*cn+an*cp)+2*(bp*dn+bn*dp))=((ap*cp+an*cn)+2*(bp*dp+bn*dn))+rn -> sp+((ap*dn+an*dp)+(bp*cn+bn*cp))=((ap*dp+an*dn)+(bp*cp+bn*cn))+sn -> r+2*(a*d+b*c)=(a*c+(2*2)*(b*d))+2*t

Fresh HA and independently compiled Lean checks

Download the exact canonical proof bundle (gzip) · Original run record.

37 local nodes; 41,346 ordinary proof-body nodes. No receipt is substituted for a proof body.

Target AST SHA-256: e123c3a589c565bfb3da565b09d0d7fd4e0ca431f884f790f02899bc10711bfa
Certificate SHA-256: 93465c3527692a4b2614c0b54d30457b7f70682203477afd9afe9775d3977ebf

Checked arithmetic DAG · Definition network · Larger IR031 planning cone · All current evidence.

IR072 remains open. This local exact certificate is not an Alpha/Stable admission or a completed irrationality proof.