The octonion squared norm is multiplicative

Proved

Octonion.normSq_mul

by jawneeboy · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebracayley-integersoctonion-arithmeticoctonions

Use the Cayley–Dickson model $\mathbb O_R=\mathbb H_R\times\mathbb H_R$ , with $(a,b)(c,d)=(ac-\bar d b,da+b\bar c)$ and $\overline{(a,b)}=(\bar a,-b)$ . Write $N(x)=\sum_{i=0}^7 x_i^2$ for the squared norm in the coordinate order $(a_0,a_1,a_2,a_3,b_0,b_1,b_2,b_3)$ . Let $R$ be any commutative ring and $x,y\in\mathbb O_R$ .

N(xy)=N(x)N(y).

This is the composition identity for the octonion quadratic form; positivity or division is not assumed.

Preamble

import Definitions.Def_Octonion_normSq
import Definitions.Def_Octonion_octonions
import Mathlib.Algebra.Quaternion
import Mathlib.Tactic.Abel
import Mathlib.Tactic.Ring

open Quaternion Octonion BigOperators
variable {R : Type*} [CommRing R]

Formal statement

theorem Octonion.normSq_mul (x y : octonions R) : normSq (x * y) = normSq x * normSq y := by sorry

Source

Standard reference: John H. Conway and Derek A. Smith, On Quaternions and Octonions: Their Geometry, Arithmetic, and Symmetry, A K Peters, 2003. https://www.routledge.com/On-Quaternions-and-Octonions/Conway-Smith/p/book/9781568811345. Relevant topics appear in Chapter 6 (composition algebras), Chapter 9 (octavian integers), and Section 10.1 (the 240 octavian units), as confirmed by the publisher's table of contents. Supporting exposition: John Baez, Integral Octonions (Part 6), September 17, 2013, https://math.ucr.edu/home/baez/octonions/integers/integers_6.html. These references concern the classical mathematics. This contribution supplies Lean definitions and machine-checked proofs in the stated coordinate convention; it does not claim new mathematical results or reproduce a particular proof from the book. The topic references do not assert that the exact Lean statement occurs there. Verification of the book references is limited to its table of contents, not a statement-by-statement comparison with the book; no page-specific or numbered theorem attribution is claimed. Local formalization: Basic/Thm_Octonion_normSq_mul.lean, line 10; SHA-256 c9500cc8b7ea046a07c9e41fe6a8f5c1359af1c8b627bdb0892883fe2563899f. No public source repository is claimed.

View graph