SN001 — Signed quadratic-norm zero criterion

Named statement

forall ap an bp bn s t. SignedDifferenceSquare(ap,an,s) -> SignedDifferenceSquare(bp,bn,t) -> s=(S(S 0))*t -> (ap=an /\ bp=bn)

The square witnesses s,t are natural numbers. The coefficient pairs ap,an and bp,bn may be arbitrary, including negative and nonnormalized integer representatives. No real-number sort or new axiom is introduced.

forall ap an bp bn s t. ap*ap+an*an=s+(ap*an+an*ap) -> bp*bp+bn*bn=t+(bp*bn+bn*bp) -> s=(S(S 0))*t -> (ap=an /\ bp=bn)

Fresh HA and independently compiled Lean checks

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

206 local nodes; 40,402 ordinary proof-body nodes. No receipt is substituted for a proof body.

Target AST SHA-256: c948aa0e7350e5c51c464721215573a489b0921c9d1a3263c9c5181f20164941
Certificate SHA-256: 5685db9bdbe1ceb79e29a25dff767c519ccf424705a1e395dad5fcb3b01911de

Checked reuse and remaining scope

The certificate includes the natural twice-square proof, together with the actual absolute-difference existence, absolute-square balance and signed-square functionality proof bodies. Their complete ancestor cones are checked again; historical receipts are not imported as axioms.

This proves the signed zero-norm criterion only. The rational/real quantitative lower bound, rational-denominator interpretation and the full irrationality argument remain open.

Definition network · Larger IR032 planning cone · All current evidence.