SN002 — Witnessed integer norm separation

Named statement

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

For a nonzero signed coefficient pair, the two natural norm contributions differ by a witnessed positive integer. The complete SN001 and NG001 proofs are included. This is the integer gap, not yet the rational-denominator or real-algebraic lower bound required by IR032.

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) -> ~(ap=an /\ bp=bn) -> exists k. (s+S k=(S(S 0))*t \/ (S(S 0))*t+S k=s)

Fresh HA and independently compiled Lean checks

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

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

Target AST SHA-256: 7a0c83cccc0c50cb487d5dda5fc177677b4aeb7758ac7179e2f46023dcccd4c5
Certificate SHA-256: 3b4257b6bd12ed44eb2de6342652a69480045fc09fe63dd62b9d94d0eabb2dc6

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

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