Expositions · C01.1 · Registrar
C01.1 · Definitions/conventions
Section of C01.1 — Split-octonions as the programme’s carrier. Section object E-C01.1.definitions-conventions · kind PROSE · cites no record · attestation inherited from the article (R69).
← Claims used · Derivation →
Write a carrier element as
\[ X=\begin{pmatrix}a&u\\v&b\end{pmatrix}, \qquad a,b\in\mathbb R,\quad u,v\in\mathbb R^3. \]
The row/column position is notation. Define the product by
\[ \begin{pmatrix}a&u\\v&b\end{pmatrix} \begin{pmatrix}c&U\\V&d\end{pmatrix} = \begin{pmatrix} ac+u\cdot V & aU+du+v\times V\\ cv+bV-u\times U & v\cdot U+bd \end{pmatrix}. \]
The opposite cross-product signs are part of the explicit convention, not something inferred from a remembered table. The included `mul` implements precisely this expression. The independent routine `cd` uses the suite’s displayed product
\[ (p,q)(r,s)=(pr+\bar s q,\;sp+q\bar r) \]
with quaternion multiplication coded separately. The equality between the two implementations is checked coefficientwise, not assumed.
Let \(\epsilon_i\) be the standard coordinate vectors. Choose
\[ 1=\begin{pmatrix}1&0\\0&1\end{pmatrix},\qquad e_i=\begin{pmatrix}0&\epsilon_i\\-\epsilon_i&0\end{pmatrix},\qquad f_i=\begin{pmatrix}0&\epsilon_i\\\epsilon_i&0\end{pmatrix},\qquad l=\begin{pmatrix}1&0\\0&-1\end{pmatrix}. \]
The basis order is \((1,e_1,e_2,e_3,f_1,f_2,f_3,l)\). For coefficients \(x=(s,E_1,E_2,E_3,F_1,F_2,F_3,t)\), the coordinate conversion is
\[ a=s+t,\quad b=s-t,\quad u=E+F,\quad v=F-E. \]
Its inverse is explicitly implemented by `unzorn`. The quaternion comparison uses \(p=(s,E)\), \(q=(t,-F)\), so in this convention \(f_i=-e_i l\). Naming the basis without this conversion would leave precisely the ambiguity that defeated the old production record.
Define
\[ \bar X=\begin{pmatrix}b&-u\\-v&a\end{pmatrix},\qquad N(X)=ab-u\cdot v. \]
The code derives the coefficient form of this norm from the Zorn coordinates. It also checks symbolically that conjugation reverses products and that \(X\bar X=\bar X X=N(X)1\), and that \(N(XY)=N(X)N(Y)\).
← Claims used · Derivation →
Receipt, script and stdout: on the article page. Registrar master sha256 01d1a5873ede42f5b2c5f4fdcee3a4a74c09a14b99a0deea86a60ebd9c821033 · BUILD_STAMP S371a · 2026-09-26 22:53Z · master 01d1a5873ede42f5 · cut 9dcc6ce9a8ee3e02