C01.2 · Definitions/conventions

Write \[ \mathbb O_\epsilon=\mathbb H\oplus\mathbb H\ell,\qquad (p,q)(r,s)=(pr+\epsilon\,\bar s q,\;sp+q\bar r), \quad \overline{(p,q)}=(\bar p,-q). \] Here \(\epsilon=+1\) is the split product, while \(\epsilon=-1\) is the compact comparison product. The norm is \(n(p,q)=|p|^2-\epsilon|q|^2\). These are the exact definitions executed by `omul` and `onorm`; the two computed norm inertias appear under `split.norm_inertia` and `compact.norm_inertia`.

Use the prior pilot's ordered basis \[ (1,e_1,e_2,e_3,f_1,f_2,f_3,\ell),\qquad f_i=-e_i\ell. \] Thus an article-coordinate vector \((s,E,F,t)\) corresponds to quaternion halves \(p=(s,E)\), \(q=(t,-F)\). In native Zorn coordinates it is \[ (a,u,v,b)=(s+t,\ E+F,\ F-E,\ s-t). \] This sign convention is part of the object under test, not a table inferred from the desired answer.

A derivation is a real linear map \(D\) satisfying \[ D(xy)=(Dx)y+x(Dy) \] for every pair of algebra elements. If \(c^k_{ij}\) are the multiplication coefficients, its exact defining system is \[ \sum_m D_{km}c^m_{ij} -\sum_m D_{mi}c^k_{mj} -\sum_m D_{mj}c^k_{im}=0. \] The script forms this system from the product, with one equation for each output coordinate and ordered basis pair. It does not import a presumed list of exceptional generators.