Named statement
forall ap an bp bn d cp cn dp dn e a b c t.
IRatEq(ap,an,d,cp,cn,e) ->
IRatEq(bp,bn,d,dp,dn,e) ->
SignedDifferenceSquare(ap,an,a) ->
SignedDifferenceSquare(bp,bn,b) ->
SignedDifferenceSquare(cp,cn,c) ->
SignedDifferenceSquare(dp,dn,t) ->
IRatEq(a,2*b,d*d,c,2*t,e*e)Equivalent rational quadratic coordinate pairs give equivalent rational norms, including negative norms and overlapping signed representatives. The two IRatEq premises explicitly include nonzero denominators; their squares are proved nonzero. Actual signed-square scaling, transport and uniqueness proofs supply the result. No new definition, rational quotient object or real-number interpretation is assumed.
Exact original expanded HA target
forall ap an bp bn d cp cn dp dn e a b c t. (~(d=0) /\ (~(e=0) /\ (ap*e+cn*d=an*e+cp*d))) -> (~(d=0) /\ (~(e=0) /\ (bp*e+dn*d=bn*e+dp*d))) -> 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=t+(dp*dn+dn*dp) -> (~(d*d=0) /\ (~(e*e=0) /\ (a*(e*e)+(2*t)*(d*d)=(2*b)*(e*e)+c*(d*d))))Fresh HA and independently compiled Lean checks
Download the exact canonical proof bundle (gzip) · Original run record.
29 local nodes; 2,630 ordinary proof-body nodes. No receipt is substituted for a proof body.
Target AST SHA-256: db34efff2aecd8c2f5afdb13cad631533c9dd9cbe2de2a878318cd31ac2290da
Certificate SHA-256: 795cd64495f9ab37dc7b12add368225567bbb63bcca6e1f698ffbd08db431667
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.