The Octonion Algebra

The octonions O are the unique 8-dimensional normed division algebra (Hurwitz 1898). They are non-associative and non-commutative.

Role in the program

The Jordan-von Neumann-Wigner classification (1934) says all simple formally real Jordan algebras are built from the four normed division algebras R, C, H, O plus spin factors. The exceptional Jordan algebra h_3(O) is the unique Jordan algebra that:

• Cannot embed in any C*-algebra (non-special)
• Cannot participate in any composite system (Barnum-Graydon-Wilce 2020)
• Has automorphism group F_4, which contains the SM gauge group

Main definitions

• Octonion -- the octonion type as an 8-dim real algebra
• Octonion.mul -- the non-associative multiplication
• Octonion.conj -- the octonionic conjugation
• Octonion.normSq -- the norm-squared (composition algebra property)
• Octonion.imagUnit -- the 7 imaginary unit octonions (Fano plane)

Main results

• non_associative -- octonion multiplication is not associative
• norm_multiplicative -- |ab| = |a||b|
• CompositionAlgebra.left_alternative, CompositionAlgebra.right_alternative -- the generic composition-algebra laws specialize to octonions via their instance

Hurwitz's classification, Aut(𝕆) = G₂, and S⁶ = G₂/SU(3) are not stated here: they were carried as custom axiom declarations in the source tree and were dropped on the way in, since this tree admits no custom axioms and nothing consumed them. ★ Of those three, Hurwitz's classification is since 2026-08-23 a theorem of this tree (Composition/Classification.lean, hurwitz_classification, axioms []) rather than a dropped axiom. The other two remain unstated.

References

• Baez, "The Octonions," Bull. AMS 39 (2002), arXiv:math/0105155
• Hurwitz, "Uber die Composition der quadratischen Formen von beliebig vielen Variablen," 1898

structure Octonion : Type

The octonion algebra, represented as R^8. Basis: e_0 = 1 (real unit), e_1 through e_7 (imaginary units).

• coords : Fin 8 → ℝ

  The 8 real components.

@[instance_reducible]

instance Octonion.instZero : Zero Octonion

Equations

• Octonion.instZero = { zero := { coords := fun (x : Fin 8) => 0 } }

@[instance_reducible]

instance Octonion.instAdd : Add Octonion

Equations

• Octonion.instAdd = { add := fun (a b : Octonion) => { coords := fun (i : Fin 8) => a.coords i + b.coords i } }

@[instance_reducible]

instance Octonion.instNeg : Neg Octonion

Equations

• Octonion.instNeg = { neg := fun (a : Octonion) => { coords := fun (i : Fin 8) => -a.coords i } }

@[instance_reducible]

instance Octonion.instSMulReal : SMul ℝ Octonion

Equations

• Octonion.instSMulReal = { smul := fun (r : ℝ) (a : Octonion) => { coords := fun (i : Fin 8) => r * a.coords i } }

theorem Octonion.ext {a b : Octonion} (h : ∀ (i : Fin 8), a.coords i = b.coords i) : a = b

theorem Octonion.ext_iff {a b : Octonion} : a = b ↔ ∀ (i : Fin 8), a.coords i = b.coords i

@[simp]

theorem Octonion.zero_coords (i : Fin 8) : coords 0 i = 0

@[simp]

theorem Octonion.add_coords (a b : Octonion) (i : Fin 8) : (a + b).coords i = a.coords i + b.coords i

@[simp]

theorem Octonion.smul_coords (r : ℝ) (a : Octonion) (i : Fin 8) : (r • a).coords i = r * a.coords i

@[simp]

theorem Octonion.neg_coords (a : Octonion) (i : Fin 8) : (-a).coords i = -a.coords i

def Octonion.one : Octonion

The real unit octonion e_0 = (1, 0, 0, 0, 0, 0, 0, 0).

Equations

• Octonion.one = { coords := fun (i : Fin 8) => if i = 0 then 1 else 0 }

def Octonion.basisVec (i : Fin 8) : Octonion

The i-th basis octonion e_i.

Equations

• Octonion.basisVec i = { coords := fun (j : Fin 8) => if j = i then 1 else 0 }

def Octonion.mul (a b : Octonion) : Octonion

Octonionic multiplication. Non-associative, non-commutative. Defined via the Fano plane multiplication table (Baez convention). Triples: (1,2,4), (2,3,5), (3,4,6), (4,5,7), (5,6,1), (6,7,2), (7,1,3). For each triple (i,j,k): e_i * e_j = e_k (cyclic positive), e_j * e_i = -e_k. e_0 is the two-sided identity; e_i^2 = -e_0 for i > 0. Extended bilinearly: (sum a_i e_i) * (sum b_j e_j) = sum a_i b_j (e_i * e_j).

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Octonion.instMul : Mul Octonion

Equations

• Octonion.instMul = { mul := Octonion.mul }

def Octonion.conj (a : Octonion) : Octonion

Octonionic conjugation: a* = 2 Re(a) - a. Equivalently: conjugate flips the sign of all imaginary components.

Equations

• a.conj = { coords := fun (i : Fin 8) => if i = 0 then a.coords 0 else -a.coords i }

def Octonion.re (a : Octonion) : ℝ

The real part of an octonion.

Equations

• a.re = a.coords 0

def Octonion.normSq (a : Octonion) : ℝ

The norm-squared: N(a) = a * a* = sum of squares of components.

Equations

• a.normSq = ∑ i : Fin 8, a.coords i ^ 2

def Octonion.imagUnit (i : Fin 7) : Octonion

The 7 imaginary unit octonions e_1, ..., e_7.

Equations

• Octonion.imagUnit i = Octonion.basisVec ⟨↑i + 1, ⋯⟩

theorem Octonion.mul_one' (a : Octonion) : a.mul one = a

Octonionic multiplication has a two-sided identity.

theorem Octonion.one_mul' (a : Octonion) : one.mul a = a

theorem Octonion.non_associative : ∃ (a : Octonion) (b : Octonion) (c : Octonion), (a.mul b).mul c ≠ a.mul (b.mul c)

Octonions are NOT associative. There exist a, b, c with (ab)c != a(bc).

theorem Octonion.norm_multiplicative (a b : Octonion) : (a.mul b).normSq = a.normSq * b.normSq

The norm is multiplicative: N(ab) = N(a) N(b). This supplies the concrete octonion example used in Hurwitz's classification.

theorem Octonion.mul_eq_zero_iff (a b : Octonion) : a.mul b = 0 ↔ a = 0 ∨ b = 0

Octonions form a division algebra: ab = 0 implies a = 0 or b = 0.

theorem Octonion.conj_mul (a b : Octonion) : (a.mul b).conj = b.conj.mul a.conj

Conjugation is an anti-involution: (ab)* = b* a*.

theorem Octonion.conj_conj (a : Octonion) : a.conj.conj = a

Conjugation is involutive: a** = a.

theorem Octonion.mul_conj (a : Octonion) : a.mul a.conj = a.normSq • one

a * a* = N(a) * 1.

theorem Octonion.mul_add' (a b c : Octonion) : a.mul (b + c) = a.mul b + a.mul c

theorem Octonion.add_mul' (a b c : Octonion) : (a + b).mul c = a.mul c + b.mul c

theorem Octonion.smul_mul (r : ℝ) (a b : Octonion) : (r • a).mul b = r • a.mul b

theorem Octonion.mul_smul' (r : ℝ) (a b : Octonion) : a.mul (r • b) = r • a.mul b