Named statement
forall ap an bp bn cp cn dp dn rp rn sp sn.
IQuadProductReal(ap,an,bp,bn,cp,cn,dp,dn,rp,rn) ->
IQuadProductRadical(ap,an,bp,bn,cp,cn,dp,dn,sp,sn) ->
~(ap=an /\ bp=bn) ->
~(cp=cn /\ dp=dn) ->
~(rp=rn /\ sp=sn)The product of two nonzero elements of Z[√2] is nonzero, with all four signed input pairs and both output pairs arbitrary. Both component equations are explicit premises. Complete SN001, SN003 and SI001 proof bodies are shared and rechecked; metadata is never a theorem premise. This is a binary algebraic statement, not yet finite trace existence or real-number interpretation.
Exact original expanded HA target
∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. ∀ j. ∀ u. ∀ v. ∀ w. ∀ x0. u + (x · k + y · m + 2 · (z · j + n · i)) = x · m + y · k + 2 · (z · i + n · j) + v → w + (x · j + y · i + (z · k + n · m)) = x · i + y · j + (z · m + n · k) + x0 → ¬(x = y ∧ z = n) → ¬(m = k ∧ i = j) → ¬(u = v ∧ w = x0)Fresh HA and independently compiled Lean checks
Download the exact canonical proof bundle (gzip) · Original run record.
221 local nodes; 81,273 ordinary proof-body nodes. No receipt is substituted for a proof body.
Target AST SHA-256: f4d0bc4f03497b4b9d2b601380b0958486e631f8a2c5f4d0b647b43662f18ca9
Certificate SHA-256: faeb2544f48735855f80ba183dc596190cc4d788f804ed57af793bd6a7b89aa3
Checked arithmetic DAG · Definition network · Larger IR046 planning cone · All current evidence.
IR072 remains open. This local exact certificate is not an Alpha/Stable admission or a completed irrationality proof.