The octonion norm is multiplicative (eight-square identity)

Theorem OctonionD8.norm_mul. For all real vectors $p, q \in \mathbb{R}^8$ (coordinates indexed by $\{0,1,\dots,7\}$, written $p_0,\dots,p_7$ and $q_0,\dots,q_7$), with no further hypotheses, the statement asserts

i.e. the squared Euclidean norm of the product $p \ast q$ equals the product of the squared Euclidean norms of $p$ and $q$. The product $\ast$ is the bilinear map defined in the imported file (not a Mathlib notion), unfolded below.

The product. For $p, q \in \mathbb{R}^8$ and each $k \in \{0,\dots,7\}$,

where $T(i,j,k) \in \{-1, 0, 1\}$ is an integer structure-constant table (cast to $\mathbb{R}$), read as "the coefficient of $e_k$ in $e_i e_j$" for the standard basis $e_0,\dots,e_7$. $T$ is defined by the following cases, checked in this order:

1. If $i = 0$: $T(0,j,k) = 1$ if $j = k$, else $0$ (so $e_0$ is a left identity).

2. Else if $j = 0$: $T(i,0,k) = 1$ if $i = k$, else $0$ (so $e_0$ is a right identity).

3. Else if $i = j$ (both nonzero): $T(i,i,k) = -1$ if $k = 0$, else $0$ (so $e_i^2 = -e_0$ for $i = 1,\dots,7$).

4. Else if $k = 0$ (with $i \ne j$, both nonzero): $T(i,j,0) = 0$.

5. Otherwise ($i, j, k$ all nonzero, $i \ne j$): the value is determined by a Fano-plane rule. Each nonzero index $m \in \{1,\dots,7\}$ is mapped to the point $\varphi(m) = (m + 6) \bmod 7 = m - 1 \in \mathbb{Z}/7$. The seven "lines" are the 3-element subsets $L_l = \{l,\ l+1,\ l+3\} \subseteq \mathbb{Z}/7$ for $l \in \mathbb{Z}/7$ (arithmetic mod $7$). Then

   • $T(i,j,k) = +1$ if there is an $l \in \mathbb{Z}/7$ with $L_l = \{\varphi(i), \varphi(j), \varphi(k)\}$ (equality of sets) and the ordered pair $(\varphi(i), \varphi(j))$ is one of $(l, l+1)$, $(l+1, l+3)$, $(l+3, l)$;
   • otherwise $T(i,j,k) = -1$ if there is an $l$ with $L_l = \{\varphi(i), \varphi(j), \varphi(k)\}$;
   • otherwise $T(i,j,k) = 0$.

   Since each $L_l$ has exactly three distinct elements, the set equality forces $i, j, k$ to be pairwise distinct; in particular $T(i,j,i) = T(i,j,j) = 0$ in this case. Translating back to indices $1,\dots,7$ (point $l$ corresponds to index $l+1$), the seven lines are the index triples

and for each listed triple $(a,b,c)$ the table encodes $e_a e_b = e_c$, $e_b e_c = e_a$, $e_c e_a = e_b$ (value $+1$), while the reversed orders give $e_b e_a = -e_c$, etc. (value $-1$). Pairs of distinct nonzero indices always lie in exactly one such triple, but the statement does not rely on or assert this; it is simply what the table evaluates to.

Scope and edge cases. The identity is claimed for every $p, q$, including $p = 0$ or $q = 0$ (both sides then $0$) and basis vectors. There are no hypotheses, so the statement is not vacuous. The imported files also define auxiliary objects (matrices of left/right multiplication by fixed vectors, a "flow" matrix built from them, the Fano plane packaged as a Steiner triple system on 7 points, and a "role colouring" predicate); none of these appear in this statement. The only imported notions used are the product $\ast$, its table $T$, the index-to-point map $\varphi$, and the lines $L_l$ described above.