SI001 — Nonzero signed-integer products

Named statement

forall p n q m r s.
  r+(p*m+n*q)=(p*q+n*m)+s ->
  ~(p=n) ->
  ~(q=m) ->
  ~(r=s)

Two nonzero signed integers have a nonzero product, even with overlapping, noncanonical input and output pairs. The output balance is explicit. Actual square-existence, square-product, square-zero and natural no-zero-divisor proof bodies supply the constructive argument. This is a binary integer lemma, not quadratic-field or finite-product closure.

forall p n q m r s. r+(p*m+n*q)=(p*q+n*m)+s -> ~(p=n) -> ~(q=m) -> ~(r=s)

Fresh HA and independently compiled Lean checks

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

34 local nodes; 2,400 ordinary proof-body nodes. No receipt is substituted for a proof body.

Target AST SHA-256: ee1a6a3a9dfc5f7d45c67d4a040a8ff0ccf2d4422f2ddc42e1fad69334c2d581
Certificate SHA-256: e0fd91506b33ed8a390173ed0599e8980e2c99ade59b24c37be92cf05bcfbc38

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.