Octonionic formula for the ternary eight-dimensional cross product A cross product is a multilinear map $X(v_1,\cdots,v_r)$ on a $d$-dimensional oriented inner product space $V$ for which (i) $\langle X(v_1,\cdots,v_r),w\rangle$ is alternating in $v_1,\cdots,v_r,w$ and (ii) the magnitude $\|X(v_1,\cdots,v_r)\|$ equals the $r$-dimensional volume of the parallelotope spanned by $v_1,\cdots,v_r$.
Condition (i) is equivalent to saying $X(v_1,\cdots,v_r)$ is perpendicular to each one of $v_1,\cdots,v_r$, and condition (ii) is algebraically given in terms of the grammian determinant:
$$\|X(v_1,\cdots,v_r)\|^2=\det\begin{bmatrix}\langle v_1,v_1\rangle & \cdots & \langle v_1,v_r\rangle \\ \vdots & \ddots & \vdots \\ \langle v_r,v_1\rangle & \cdots & \langle v_r,v_r\rangle\end{bmatrix} $$
An orthogonal transformation $g\in\mathrm{O}(V)$ may be applied to $X$ via the formula
$$ (g\cdot X)(v_1,\cdots,v_r):=gX(g^{-1}v_1,\cdots,g^{-1}v_r).$$
In this way, $\mathrm{O}(V)$ acts on the moduli space of cross products on $V$ of a given type.
It's a relatively simple matter to classify cross products of type $(r,d)$ when $r\ge d-1$ or $r\le 1$, and for any type $(r,d)$ defined on $V$ one may define a type $(r-1,d-1)$ on the oriented orthogonal complement of a unit $v\in V$ by fixing $v_r=v$ in $X(v_1,\cdots,v_r)$. The binary cross products ($r=2$) correspond to composotion algebras $A$: for pure imaginary $u,v\in A$ we have the multiplication rule $uv=-\langle u,v\rangle+u\times v$ (and one can use this to construct $A$ from $\times$).
So the octonions $\mathbb{O}$ give rise to a cross product of type $(2,7)$. It's symmetry group is $G_2=\mathrm{Aut}(\mathbb{O})$, which is a rather awkward kind of symmetry (and small compared to $\mathrm{SO}(8)$). But it's the shadow of a type $(3,8)$ one with much nicer symmetry group $\mathrm{Spin}(7)\hookrightarrow\mathrm{SO}(8)$ (see L690).
To understand this latter symmetry group: the clifford algebra $\mathrm{Cliff}(V)$ is the tensor algebra $T(V)$ modulo the relations $v^2=-1$ for all unit $v\in V$, and the spin group $\mathrm{Spin}(V)$ is the group comprised of products of evenly many unit vectors of $V$. In $\mathbb{O}$, pure imaginary unit elements are square roots of $-1$, so there is the following action of $\mathrm{Spin}(\mathrm{Im}(\mathbb{O}))$ on $\mathbb{O}$:
$$(u_1\cdot u_2\cdots u_{2k-1}\cdot u_{2k})\,v=u_1(u_2(\cdots u_{2k-1}(u_{2k}v)\cdots)). $$
A formula for the ternary cross product on $\mathbb{O}$ is $X(a,b,c)=\frac{1}{2}[a(\overline{b}c)-c(\overline{b}a)]$. The only place I've been able to find this (or any) octonionic formula for it is here. Where does it come from?
Before I found that formula, I tried to create my own. I reasoned that if $X(a,b,c)$ restricts to the binary one on $\mathrm{Im}(\mathbb{O})$ then we at least know $X(1,b,c)=\mathrm{Im}(\mathrm{Im}(b)\mathrm{Im}(c))$. Then I figured to evaluate $X(a,b,c)$, we can rotate the "frame" $\{a,b,c\}$ to $\{|a|,\circ,\circ\}$ via some rotation, then apply $X$, then rotate back. There is a canonical rotation sending $a$ to $1$, namely left multiplication by $\overline{a}/|a|$, so I wrote out the formula
$$X(a,b,c)=a\,\mathrm{Im}\left(\mathrm{Im}\left(\frac{\overline{a}}{|a|}b\right)\mathrm{Im}\left(\frac{\overline{a}}{|a|}c\right)\right).$$
I've verified that my $X(a,b,c)$ has the correct magnitude, is perpendicular to $a,b,c$, and is alternating and linear in $b$ and $c$, but I wouldn't know how to show it's linear in $a$ (or alternating in $a,b$, say, or cyclically symmetric in $a,b,c$). Through some laborious calculations I was able to determine the difference between my $X$ and their $X$ is the associator $[\overline{a},b,\overline{a}c]$, so they're not quite the same. One nice thing about my formula is (besides having a heuristic backstory), it looks like it might be amenable to showing $\mathrm{Spin}(7)$ symmetry.
Is there anything salvagable in my formula or its "derivation"? If not, what then is the backstory behind the given formula at the link? Ultimately, at the end of the day, I'd like: the octonionic formula for ternary cross product, a plausible story about how I could have discovered the formula on a stranded island from scratch, and a direction to go in to start seeing the $\mathrm{Spin}(7)$ symmetry. That story is already written some by the information I've provided.
 A: First of all, let's say we make the middle argument of $X(\cdot,\cdot,\cdot)$ the "special one," I suppose for symmetry's sake. We know that $X(a,1,c)$ should be the usual binary cross product on $\mathrm{Im}(\mathbb{O})$, which has the formula $a\times c=\frac{1}{2}[ac-ca]$ when $a,c$ are imaginary. Since that formula depends only on the imaginary parts of $a,c$ and the same should go for $X(a,1,c)$, we can extend that formula so that it holds for all $a,c$.
Let $G\subseteq\mathrm{O}(V)$ be the symmetry group of $X$. Ideally, we want it to act transitively on the unit sphere $S^7\subseteq\mathrm{Im}(\mathbb{O})$, in which case for all unit octonions $b$ there should be a $g\in G$ with the property $g^{-1}b=1$, in which case $X(a,b,c)=gX(g^{-1}a,1,g^{-1}c)$ can be evaluated using the formula. We don't know what $G$ is, but there is a canonical element of $\mathrm{O}(V)$ that rotates $1$ to $b$, namely (say left) multiplication by $b$. Checking $bX(b^{-1}a,1,b^{-1}c)$ gives
$$ \frac{1}{2}b\left[(\overline{b}a)(\overline{b}c)-(\overline{b}c)(\overline{b}a)\right]. $$
Unfortunately, the desired simplification $b[(\overline{b}a)(\overline{b}c)]\to a(\overline{b}c)$, while seemingly begging to be true, is not valid. The Moufang identities do not help since $b\ne\overline{b}$.
The idea can be augmented though. We already know the value of $X(a,b,c)$ when $b$ is real, so we need to know its value when $b$ is imaginary. Now when we apply the above idea (in which case left multiplication by $b$ corresponds to an element of $\mathrm{Pin}(\mathrm{Im}(\mathbb{O}))$ acting) we have $\overline{b}=-b$ in which case we can simplify $b((ba)(bc))$ by writing $x=bab^{-1}$ and $y=bc$ so it becomes
$$ b((ba)(bc))=b((xb)y)=(bxb)y=-a(bc). $$
Therefore, we get
$$ X(a,b,c)=-\frac{1}{2}\left[a(bc)-c(ba)\right]$$
when $b$ is purely imaginary. In general, when we split $b$ inside $X(a,b,c)$ into real and imaginary parts, we wind up with
$$ X(a,b,c)=\frac{1}{2}\left[a(\overline{b}c)-c(\overline{b}a)\right].$$
The nice thing about this is that $\mathrm{Pin}(7)$-symmetry is built right into the motivation behind the formula. It's easy to check that $\mathrm{Pin}(7)$ stabilizes this, but I don't know how to prove it's the full symmetry group. In any case, checking this is a cross product at this point should be comparatively straightforward.
