Universal arithmetic lemma · Local exact evidence

RN002 — Rational quadratic norm multiplication

Named statement

forall ap an bp bn cp cn dp dn rp rn sp sn a b c d r t u v.
  ~(u=0) ->
  ~(v=0) ->
  SignedDifferenceSquare(ap,an,a) ->
  SignedDifferenceSquare(bp,bn,b) ->
  SignedDifferenceSquare(cp,cn,c) ->
  SignedDifferenceSquare(dp,dn,d) ->
  SignedDifferenceSquare(rp,rn,r) ->
  SignedDifferenceSquare(sp,sn,t) ->
  IQuadProductReal(ap,an,bp,bn,cp,cn,dp,dn,rp,rn) ->
  IQuadProductRadical(ap,an,bp,bn,cp,cn,dp,dn,sp,sn) ->
  IRatMul(a,2*b,u*u,c,2*d,v*v,r,2*t,(u*v)*(u*v))

The exact signed integer norm identity now yields the existing rational multiplication relation. Both input denominators are explicitly nonzero; the output denominator is (uv)², not uv. Arbitrary signed output coordinate representatives are allowed. This does not identify the represented element with a real number or prove the full IR031 norm/conjugate statement.

Exact original expanded HA target
∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. ∀ j. ∀ u. ∀ v. ∀ w. ∀ x0. ∀ x1. ∀ x2. ∀ x3. ∀ x4. ∀ x5. ∀ x6. ∀ x7. ∀ x8. ¬x7 = 0 → ¬x8 = 0 → x · x + y · y = x1 + (x · y + y · x) → z · z + n · n = x2 + (z · n + n · z) → m · m + k · k = x3 + (m · k + k · m) → i · i + j · j = x4 + (i · j + j · i) → u · u + v · v = x5 + (u · v + v · u) → w · w + x0 · x0 = x6 + (w · x0 + x0 · w) → 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 → ¬x7 · x7 = 0 ∧ (¬x8 · x8 = 0 ∧ (¬x7 · x8 · (x7 · x8) = 0 ∧ (¬x7 · x7 · (x8 · x8) = 0 ∧ x5 · (x7 · x7 · (x8 · x8)) + (x1 · (2 · x4) + 2 · x2 · x3) · (x7 · x8 · (x7 · x8)) = 2 · x6 · (x7 · x7 · (x8 · x8)) + (x1 · x3 + 2 · x2 · (2 · x4)) · (x7 · x8 · (x7 · x8)))))

Fresh HA and independently compiled Lean checks

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

46 local nodes; 42,483 ordinary proof-body nodes. No receipt is substituted for a proof body.

Target AST SHA-256: ab88f7b597011f85f10d543e582abb37db52852d940b4b7a8c4c2cf7ae22c335
Certificate SHA-256: 70c033412b498cb8e180a800c45773610adb27aedad70716b6cc0e332edd9c68

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.