Quaternion Non-Commutativity

The quaternions are non-commutative: qi * qj is not equivalent to qj * qi. Explicit witness: the k-component differs in sign. This is the first non-commutative algebra earned within tau.

Quaternion Non-Commutativity

Summary

The quaternions are non-commutative: qi * qj is not equivalent to qj * qi. Explicit witness: the k-component differs in sign. This is the first non-commutative algebra earned within tau.

Statement

%
\label{thm:quaternion-division}
$\mathbb{H}_\tau$ is a \textbf{division algebra}:
every nonzero $q \in \mathbb{H}_\tau$ has a multiplicative inverse
\[
    \boxed{q^{-1} = \frac{\bar{q}}{|q|^2},
    \qquad q q^{-1} = q^{-1} q = 1.}
\]

Proof / Justification

For $q \neq 0$, $|q|^2 = a^2 + b^2 + c^2 + d^2 > 0$.
Then $q \cdot (\bar{q}/|q|^2) = q\bar{q}/|q|^2 = |q|^2/|q|^2 = 1$
by Proposition~\ref{prop:norm-conjugation}, and similarly for $q^{-1}q$.

Source Context

• Registry source: book-01.jsonl line 194
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part17/ch78-elliptic-quaternions.tex lines 159-168

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Boundary.Quaternions
• Name: Tau.Boundary.quaternion_non_commutativity

Dependencies

• Canonical: I.D87

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.