The octonion nucleus lies in ℝ · 1

The nucleus of a not-necessarily-associative algebra is the set of elements that associate with everything. For the octonions it is as small as it can be: ℝ · 1. The statement below is the "third slot" form -- c associates in the last position, (x y) c = x (y c), for all x, y -- and concludes that c has no imaginary part. Equivalently: 𝕆 is as far from associative as an alternative algebra gets, since by the alternative laws any two elements already generate an associative subalgebra.

The proof is the finite Cayley-table check the memo describes. For each of the seven Fano triples (i, j, k) the associator [e_i, e_j, c] is expanded in coordinates; each c.coords m outside the quaternion subalgebra span{e_0, e_i, e_j, e_k} picks up a relation c.coords m = -c.coords m. Three triples cover all seven imaginary indices: (1,2,4) kills 3,5,6,7, (2,3,5) kills 1,4, and (3,4,6) kills 2.

decide handles the Fin 8 guards. Nothing here or anywhere in this development is discharged by kernel-external evaluation, so nothing below rests on the compiler.

theorem Octonion.coord_eq {a b : Octonion} (hab : a = b) (k : Fin 8) : a.coords k = b.coords k

theorem Octonion.tbl_1_2 : (basisVec 1).mul (basisVec 2) = basisVec 4

theorem Octonion.tbl_2_3 : (basisVec 2).mul (basisVec 3) = basisVec 5

theorem Octonion.tbl_3_4 : (basisVec 3).mul (basisVec 4) = basisVec 6

theorem Octonion.nucleus_real (c : Octonion) (h : ∀ (x y : Octonion), (x.mul y).mul c = x.mul (y.mul c)) : c.coords 1 = 0 ∧ c.coords 2 = 0 ∧ c.coords 3 = 0 ∧ c.coords 4 = 0 ∧ c.coords 5 = 0 ∧ c.coords 6 = 0 ∧ c.coords 7 = 0

The substantive inclusion: an element in the third-slot nucleus has no imaginary part.