Turns out that what the (aVa) ψ = a(V(a ψ)) moufang identity of the #octonions is really about is the translation between division-algebraic vector-reflection and clifford-algebraic vector-reflection (generated by chains of left-multiplication).

Similarly (aψ)(χa) = a(ψχ)a makes sure the decomposition of a vector into two spinors is compatible with their respective transformation behaviour (two transformed spinors on one side, the corresponding transformed vector on the other).

Project idea: formalize error correcting codes in Mizar.

Error-correcting codes are a beautiful subject, mostly because they're linear algebra over finite fields (and linear algebra is beautiful).

But there are exceptional connections in the subject: the Golay code and the Leech lattice especially connect with disparate subjects.

To give one sense of connection, I gave Robert A Wilson's construction of the Leech lattice using the octonions as a "milestone".

#Mizar #ProofAssistant #ErrorCorrectingCodes #LeechLattice #LinearAlgebra #Octonions #GolayCode

https://thmprover.wordpress.com/2025/01/09/from-error-correcting-codes-to-the-leech-lattice/

Daniel and Jorge talk about super complex numbers and how they might hold the secrets of the Universe..

What are octonions?

#Algebra #complexNumbers #DanielAndJorgeExplainTheUniverse #Geometry #Math #Mathematics #octonions #Physics #podcast #podcasts #Quantum #QuantumMechanics #QuantumPhysics #science #SpecialRelativity

TIL about an apparently notorious #OpenQuestion in #topology: is there a complex structure on the 6-sphere?

The Chern character rules out complex structures on 𝑆ⁿ for n>6. Apparently 𝑆⁴ doesn't even have an almost complex structure, although 𝑆⁶ does (coming as the unit sphere in the pure imaginary #octonions IIUC).

See https://doi.org/10.4153/CMB-1966-003-9 for some overview and refs. Learned from https://twitter.com/CihanPostsThms/status/1632549791036059648

Octonions.jl v0.2.2 extends all complex analytic functions in the standard library to the #octonions!

Octonions are a type of hypercomplex number whose product is neither associative nor commutative. Besides their normal uses, they are also useful for testing numerical algorithms that are intended to generically work for even weird numbers.

Here we use them to check that the fallback QR and unpivoted LU decompositions in #JuliaLang do the right thing.

https://github.com/JuliaGeometry/Octonions.jl

In this talk I show how to multiply quaternions AND ALSO OCTONIONS using the dot product and cross product of vectors in 3 dimensions:

https://www.youtube.com/watch?v=JI5xPGN_sWo

For quaternions this is well-known, but for octonions it's less so.

I sketched the proof that both these algebras have a norm obeying

|ab| = |a| |b|

To see the details, go to the proof of Theorem 2 here:

https://golem.ph.utexas.edu/category/2020/07/octonions_and_the_standard_mod_1.html

I do the proof for octonions, but the same argument also works for quaternions!

#quaternions #octonions