Exact named statement
∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. ∀ j. ∀ u. ∀ v. ∀ w. ∀ x0. ∀ x1. ∀ x2. ∀ x3. ∀ x4. ∀ x5. ∀ x6. 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 → x5 + 2 · (x1 · x4 + x2 · x3) = x1 · x3 + 2 · 2 · (x2 · x4) + 2 · x6No displayed named abbreviation.
Complete certificate and independent checks
37 actual local proof nodes. Each node carries its complete ordinary HA proof body.
Full canonical proof bundle · Original HA receipt · Independent Lean receipt
Target SHA-256: e123c3a589c565bfb3da565b09d0d7fd4e0ca431f884f790f02899bc10711bfa
Bundle SHA-256: 93465c3527692a4b2614c0b54d30457b7f70682203477afd9afe9775d3977ebf
Checked statement containment
These exact targets occur inside this certificate. These links summarize containment, not direct dependency arrows; the downloadable bundle records every private lemma and ordered edge.
Scope
signed norm multiplicativity not rational IR031
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.