The Cayley-Dickson Construction in ACL2

TL;DR

This paper explores the Cayley-Dickson Construction within ACL2(r), examining how to generate higher-dimensional number systems like quaternions and octonions while preserving key algebraic properties.

Contribution

It formalizes the Cayley-Dickson Construction in ACL2(r), analyzing conditions under which constructed vector spaces maintain Euclidean length properties.

Findings

Formalization of Cayley-Dickson Construction in ACL2(r)

Conditions for preserving Euclidean length in constructed vector spaces

Insights into algebraic properties of quaternions and octonions

Abstract

The Cayley-Dickson Construction is a generalization of the familiar construction of the complex numbers from pairs of real numbers. The complex numbers can be viewed as two-dimensional vectors equipped with a multiplication. The construction can be used to construct, not only the two-dimensional Complex Numbers, but also the four-dimensional Quaternions and the eight-dimensional Octonions. Each of these vector spaces has a vector multiplication, v_1*v_2, that satisfies: 1. Each nonzero vector has a multiplicative inverse. 2. For the Euclidean length of a vector |v|, |v_1 * v_2| = |v_1| |v2|. Real numbers can also be viewed as (one-dimensional) vectors with the above two properties. ACL2(r) is used to explore this question: Given a vector space, equipped with a multiplication, satisfying the Euclidean length condition 2, given above. Make pairs of vectors into "new" vectors with a multiplication. When do the newly constructed vectors also satisfy condition 2?

Equations

$$\Vert {\mathbf{v}}_{\_}1\bullet {\mathbf{v}}_{\_}2\Vert =\Vert {\mathbf{v}}_{\_}1\Vert \cdot \Vert {\mathbf{v}}_{\_}2\Vert .$$

$$\displaystyle(x_{\_}{1},\ldots,x_{\_}{n})\,\mbox{\boldmath$\odot$}\,(y_{\_}{1},\ldots,y_{\_}{n})$$

$$\begin{array}[]{ccc}|\mathbf{v}|&=&\sqrt{\mathbf{v}\odot\mathbf{v}}\\ \|\mathbf{v}\|&=&\mathbf{v}\odot\mathbf{v}.\end{array}$$

$$\Vert \mathbf{v}\bullet \mathbf{w}\Vert =\Vert \mathbf{v}\Vert \cdot \Vert \mathbf{w}\Vert ,$$

$$\Vert ({\mathbf{v}}_{\_}1;{\mathbf{v}}_{\_}2)\bullet ({\mathbf{w}}_{\_}1;{\mathbf{w}}_{\_}2)\Vert =\Vert ({\mathbf{v}}_{\_}1;{\mathbf{v}}_{\_}2)\Vert \cdot \Vert ({\mathbf{w}}_{\_}1;{\mathbf{w}}_{\_}2)\Vert .$$

$$(a_{\_}1;a_{\_}2)\cdot (b_{\_}1;b_{\_}2)=([a_{\_}1b_{\_}1-a_{\_}2b_{\_}2];[a_{\_}1b_{\_}2+a_{\_}2b_{\_}1])$$

$$\Vert (a_{\_}1;a_{\_}2)\cdot (b_{\_}1;b_{\_}2)\Vert =\Vert (a_{\_}1;a_{\_}2)\Vert \cdot \Vert (b_{\_}1;b_{\_}2)\Vert .$$

$$(c;d)$$

$$(c_{\_}1;c_{\_}2)\cdot (d_{\_}1;d_{\_}2)$$

$$\Vert (c_{\_}1;c_{\_}2)\cdot (d_{\_}1;d_{\_}2)\Vert =\Vert (c_{\_}1;c_{\_}2)\Vert \cdot \Vert (d_{\_}1;d_{\_}2)\Vert .$$

$$\begin{array}[]{c|rrr}&i&j&k\\ \hline\cr i&-1&k&-j\\ j&-k&-1&i\\ k&j&-i&-1\end{array}$$

$$(q;r)$$

$$(q_{\_}1;q_{\_}2)\cdot (r_{\_}1;r_{\_}2)$$

$$\Vert (q_{\_}1;q_{\_}2)\cdot (r_{\_}1;r_{\_}2)\Vert =\Vert (q_{\_}1;q_{\_}2)\Vert \cdot \Vert (r_{\_}1;r_{\_}2)\Vert .$$

$$\begin{array}[]{c|rrrrrrr}&i&j&k&\ell&I&J&K\\ \hline\cr i&-1&k&-j&I&-\ell&-K&J\\ j&-k&-1&i&J&K&-\ell&-I\\ k&j&-i&-1&K&-J&I&-\ell\\ \ell&-I&-J&-K&-1&i&j&k\\ I&\ell&-K&J&-i&-1&-k&j\\ J&K&\ell&-I&-j&k&-1&-i\\ K&-J&I&\ell&-k&-j&i&-1\end{array}$$

$$({\mathbf{v}}_{\_}1;{\mathbf{v}}_{\_}2)\bullet ({\mathbf{w}}_{\_}1;{\mathbf{w}}_{\_}2)$$

$$\Vert ({\mathbf{v}}_{\_}1;{\mathbf{v}}_{\_}2)\bullet ({\mathbf{w}}_{\_}1;{\mathbf{w}}_{\_}2)\Vert =\Vert ({\mathbf{v}}_{\_}1;{\mathbf{v}}_{\_}2)\Vert \cdot \Vert ({\mathbf{w}}_{\_}1;{\mathbf{w}}_{\_}2)\Vert ,$$

$$\Vert {\mathbf{v}}_{\_}1\bullet {\mathbf{v}}_{\_}2\Vert =\Vert {\mathbf{v}}_{\_}1\Vert \cdot \Vert {\mathbf{v}}_{\_}2\Vert .$$

$${\mathbf{v}}^{-1}=\frac{1}{\Vert \mathbf{v}\Vert }\circ \bar{\mathbf{v}}$$

$$\Vert {\mathbf{v}}_{\_}1\bullet {\mathbf{v}}_{\_}2\Vert =\Vert {\mathbf{v}}_{\_}1\Vert \cdot \Vert {\mathbf{v}}_{\_}2\Vert .$$

$$[\text{mbox}Vp(x)\wedge \text{mbox}Vp(y)\wedge \text{mbox}Vp(z)]\to (x+y)+z=x+(y+z)$$

$$[\text{mbox}Vp(x)\wedge \text{mbox}Vp(y)]\to x+y=y+x$$

$$\text{mbox}Vp(x)\to \vec{0}+x=x$$

$$\text{mbox}Vp(x)\to x+(-x)=\vec{0}$$

$$[\text{mbox}Realp(a)\wedge \text{mbox}Realp(b)\wedge \text{mbox}Vp(x)]\to a\circ (b\circ x)=(a\cdot b)\circ x$$

$$\text{mbox}Vp(x)\to 1\circ x=x$$

$$[\text{mbox}Realp(a)\wedge \text{mbox}Realp(b)\wedge \text{mbox}Vp(x)]\to (a+b)\circ x=(a\circ x)+(b\circ x)$$

$$[\text{mbox}Realp(a)\wedge \text{mbox}Vp(x)\wedge \text{mbox}Vp(y)]\to a\circ (x+y)=(a\circ x)+(a\circ y)$$

Full text

The construction can be used to construct, not only the two-dimensional Complex Numbers, but also the four-dimensional Quaternions and the eight-dimensional Octonions. Each of these vector spaces has a vector multiplication, $\mathbf{v}_{\_}{1}\bullet\mathbf{v}_{\_}{2}$, that satisfies:

Each nonzero vector, $\mathbf{v}$, has a multiplicative inverse $\mathbf{v}^{-1}$. 2. 2.

For the Euclidean length of a vector $|\mathbf{v}|$, $|\mathbf{v}_{\_}{1}\bullet\mathbf{v}_{\_}{2}|=|\mathbf{v}_{\_}{1}|\cdot|\mathbf{v}_{\_}{2}|$

Real numbers can also be viewed as (one-dimensional) vectors with the above two properties.

ACL2(r) is used to explore this question: Given a vector space, equipped with a multiplication, satisfying the Euclidean length condition 2, given above. Make pairs of vectors into “new” vectors with a multiplication. When do the newly constructed vectors also satisfy condition 2?

1 Cayley-Dickson Construction

Given a vector space, with vector addition, $\mathbf{v}_{\_}{1}+\mathbf{v}_{\_}{2}$; vector minus $-\mathbf{v}$; a zero vector $\vec{0}$; scalar multiplication by real number $a$, $a\circ\mathbf{v}$; a unit vector $\vec{1}$; and vector multiplication $\mathbf{v}_{\_}{1}\bullet\mathbf{v}_{\_}{2}$; satisfying the Euclidean length condition $|\mathbf{v}_{\_}{1}\bullet\mathbf{v}_{\_}{2}|=|\mathbf{v}_{\_}{1}|\cdot|\mathbf{v}_{\_}{2}|$ (2).

Define the norm of vector $\mathbf{v}$ by $\|\mathbf{v}\|=|\mathbf{v}|^{2}$. Since $|\mathbf{v}_{\_}{1}\bullet\mathbf{v}_{\_}{2}|=|\mathbf{v}_{\_}{1}|\cdot|\mathbf{v}_{\_}{2}|$ is equivalent to $|\mathbf{v}_{\_}{1}\bullet\mathbf{v}_{\_}{2}|^{2}=|\mathbf{v}_{\_}{1}|^{2}\cdot|\mathbf{v}_{\_}{2}|^{2}$, the Euclidean length condition is equivalent to

[TABLE]

Recall the dot (or inner) product, of $n$-dimensional vectors, is defined by

[TABLE]

Then Euclidean length and norm of vector $\mathbf{v}$ are given by

[TABLE]

Except for vector multiplication, it is easy to treat ordered pairs of vectors, $(\mathbf{v}_{\_}{1};\mathbf{v}_{\_}{2})$, as vectors:

$(\mathbf{v}_{\_}{1};\mathbf{v}_{\_}{2})+(\mathbf{w}_{\_}{1};\mathbf{w}_{\_}{2})=(\mathbf{v}_{\_}{1}+\mathbf{w}_{\_}{1};\mathbf{v}_{\_}{2}+\mathbf{w}_{\_}{2})$ 2. 2.

$-(\mathbf{v}_{\_}{1};\mathbf{v}_{\_}{2})=(-\mathbf{v}_{\_}{1};-\mathbf{v}_{\_}{2})$ 3. 3.

zero vector: $(\vec{0};\vec{0})$ 4. 4.

\mbox{ a}\circ(\mathbf{v}_{\_}{1};\mathbf{v}_{\_}{2})=(\!\!\mbox{ a}\circ\mathbf{v}_{\_}{1};\!\mbox{ a}\circ\mathbf{v}_{\_}{2}) 5. 5.

unit vector: $(\vec{1};\vec{0})$ 6. 6.

$(\mathbf{v}_{\_}{1};\mathbf{v}_{\_}{2})\odot(\mathbf{w}_{\_}{1};\mathbf{w}_{\_}{2})=\{\mathbf{v}_{\_}{1}\odot\mathbf{w}_{\_}{1}\}+\{\mathbf{v}_{\_}{2}\odot\mathbf{w}_{\_}{2}\}$ 7. 7.

$\|(\mathbf{v}_{\_}{1};\mathbf{v}_{\_}{2})\|=\|\mathbf{v}_{\_}{1}\|+\|\mathbf{v}_{\_}{2}\|$

Given that

[TABLE]

the problem is to define multiplication of vector pairs so that

[TABLE]

1.1 Examples

Complex multiplication.

Think of the real numbers as one-dimensional vectors. Interpret ordered pairs of real numbers as complex numbers: For real $a$ and $b$, $(a;b)=(\mbox{{complex}}\ a\ \ b)=a+b\cdot i$. For reals $a_{\_}{1},a_{\_}{2}$ and $b_{\_}{1},b_{\_}{2}$, complex multiplication is defined by

[TABLE]

and satisfies

[TABLE]

Quaternion multiplication.

Think of the complex numbers as two-dimensional vectors. Interpret ordered pairs of complex numbers as William Hamilton’s quaternions [2, 4, 3]: For complex $c=a_{\_}{1}+a_{\_}{2}\cdot i$ and $d=b_{\_}{1}+b_{\_}{2}\cdot i$,

[TABLE]

where $i\cdot j=k$.

For complex $c=a_{\_}{1}+a_{\_}{2}\cdot i$, $\bar{c}=a_{\_}{1}-a_{\_}{2}\cdot i$ is the conjugate of $c$.

For complex numbers $c_{\_}{1}=a_{\_}{1}+a_{\_}{2}\cdot i$, $c_{\_}{2}=a_{\_}{3}+a_{\_}{4}\cdot i$, $d_{\_}{1}=b_{\_}{1}+b_{\_}{2}\cdot i$, and $d_{\_}{2}=b_{\_}{3}+b_{\_}{4}\cdot i$, quaternion multiplication is defined by

[TABLE]

and satisfies

[TABLE]

Quaternion multiplication is completely determined by this table for the multiplication of $i$, $j$, and $k$:

[TABLE]

Quaternion multiplication is not commutative, since $i\cdot j=k$ and $j\cdot i=-k$. Quaternion multiplication is associative: $(q_{\_}{1}\cdot q_{\_}{2})\cdot q_{\_}{3}=q_{\_}{1}\cdot(q_{\_}{2}\cdot q_{\_}{3})$.

Octonion multiplication.

Think of the quaternions as four-dimensional vectors. Interpret ordered pairs of quaternions as John Graves’s and Arthur Cayley’s octonions [2, 4, 3]: For quaternions $q=a_{\_}{1}+a_{\_}{2}\cdot i+a_{\_}{3}\cdot j+a_{\_}{4}\cdot k$ and $r=b_{\_}{1}+b_{\_}{2}\cdot i+b_{\_}{3}\cdot j+b_{\_}{4}\cdot k$,

[TABLE]

where $i\cdot\ell=I$, $j\cdot\ell=J$, and $k\cdot\ell=K$

For quaternion $q=a_{\_}{1}+a_{\_}{2}\cdot i+a_{\_}{3}\cdot j+a_{\_}{4}\cdot k$, $\bar{q}=a_{\_}{1}-a_{\_}{2}\cdot i-a_{\_}{3}\cdot j-a_{\_}{4}\cdot k$ is the conjugate of $q$.

For quaternions $q_{\_}{1}$, $q_{\_}{2}$, $r_{\_}{1}$, and $r_{\_}{2}$, octonion multiplication is defined by

[TABLE]

and satisfies

[TABLE]

Octonion multiplication is completely determined by this table for the multiplication of $i$, $j$, $k$, $\ell$, $I$, $J$, and $K$:

[TABLE]

Since the octonions contain the quaternions, octonion multiplication is also not commutative. Octonian multiplication is not associative, since $\ell\cdot(I\cdot J)=K$ and $(\ell\cdot I)\cdot J=-K$.

Complex (1), quaternion (2), and octonion (3) multiplication suggest these possible definitions for vector multiplication:

[TABLE]

When the $\mathbf{v}_{\_}{i}$ and $\mathbf{w}_{\_}{i}$ are real numbers, all three definitions are equivalent, since real multiplication is commutative and the conjugate of real $a$, $\bar{a}$, is just $a$.

When the $\mathbf{v}_{\_}{i}$ and $\mathbf{w}_{\_}{i}$ are complex numbers, the last two definitions are equivalent, since complex multiplication is commutative. However, when $\mathbf{v}_{\_}{1}=1+0\cdot i=\mathbf{w}_{\_}{1}$, $\mathbf{v}_{\_}{2}=0+1\cdot i$, and $\mathbf{w}_{\_}{2}=0+(-1\cdot i)$, the product given by equation (4) is the zero vector $([0+0\cdot i];[0+0\cdot i])$. So a vector product defined by (4) need not satisfy

[TABLE]

for complex inputs.

Since the quaternions contain the complex numbers, a vector product defined by (4) also will not be satisfactory for quaternion inputs. When $\mathbf{v}_{\_}{1}=0+(-1\cdot i)+0\cdot j+0\cdot k$, $\mathbf{v}_{\_}{2}=0+0\cdot i+1\cdot j+0\cdot k=\mathbf{w}_{\_}{2}$, and $\mathbf{w}_{\_}{1}=0+1\cdot i+0\cdot j+0\cdot k$, the product given by equation (5) is the zero vector $([0+0\cdot i+0\cdot j+0\cdot k];[0+0\cdot i+0\cdot j+0\cdot k])$. So a vector product defined by either (4) or (5) need not satisfy

[TABLE]

for quaternion inputs.

This leaves (6) as a possible way to define vector multiplication of ordered pairs of vectors. So a vector conjugate, $\bar{\mathbf{v}}$, is also required. Continuing the enumeration of vector pair operations given on page 2:

$\overline{(\mathbf{v}_{\_}{1};\mathbf{v}_{\_}{2})}=(\bar{\mathbf{v}}_{\_}{1};-\mathbf{v}_{\_}{2})$ 2. 9.

$(\mathbf{v}_{\_}{1};\mathbf{v}_{\_}{2})\bullet(\mathbf{w}_{\_}{1};\mathbf{w}_{\_}{2})=([\mathbf{v}_{\_}{1}\mathbf{w}_{\_}{1}-\bar{\mathbf{w}}_{\_}{2}\mathbf{v}_{\_}{2}];[\mathbf{w}_{\_}{2}\mathbf{v}_{\_}{1}+\mathbf{v}_{\_}{2}\bar{\mathbf{w}}_{\_}{1}])$

The enumerated list of items, $1,2,\cdots,9$, defining various operations on ordered pairs of vectors, is called the Cayley-Dickson Construction [5, 3].

1.2 Summary

• •

Start with the real numbers.

Apply the Cayley-Dickson Construction to pairs of real numbers.

Obtain a vector algebra isomorphic to the complex numbers.

• •

Apply the Cayley-Dickson Construction to pairs of complex numbers.

Obtain a vector algebra isomorphic to the quaternions.

• •

Apply the Cayley-Dickson Construction to pairs of quaternions.

Obtain a vector algebra isomorphic to the octonians.

Each of these vector spaces: real numbers, complex numbers, quaternions, and octonians, satisfy

[TABLE]

Futhermore, every vector $\mathbf{v}\neq\vec{0}$ has a multiplicative inverse:

[TABLE]

2 Composition Algebras

A composition algebra [2, 4] is a real vector space, with vector multiplication, a real-valued norm, and a real-valued dot product, satisfying this composition law

[TABLE]

Use encapsulate to axiomatize, in ACL2(r), composition algebras.

ACL2(r) function symbols are needed for

• •

Vector Predicate. $\mbox{{Vp}}(x)$ for “$x$ is a vector.”

• •

Zero Vector. $\vec{0}$

• •

Vector Addition. $\mathbf{v}_{\_}{1}+\mathbf{v}_{\_}{2}$

• •

Vector Minus. $-\mathbf{v}$

• •

Scalar Multiplication. For real number $a$, $a\circ\mathbf{v}$

• •

Vector Multipication. $\mathbf{v}_{\_}{1}\bullet\mathbf{v}_{\_}{2}$

• •

Unit Vector. $\vec{1}$

• •

Vector Norm. $\|\mathbf{v}\|$

• •

Vector Dot Product. $\mathbf{v}_{\_}{1}\odot\mathbf{v}_{\_}{2}$

• •

Predicate with Quantifier. $\forall u[\mbox{{Vp}}(u)\rightarrow u\odot x=0]$

• •

Skolem Function. Witness function for Predicate with Quantifier

In addition to the usual closure axioms, the encapsulate adds these axioms to ACL2(r):

• •

Real Vector Space Axioms.

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

• •

Real Vector Algebra Axioms.

[TABLE]

[TABLE]

[TABLE]

[TABLE]

• •

Vector Norm and Dot Product Axioms.

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

The ACL2(r) theory of composition algebras includes the following theorems and definitions:

• •

Scaling Laws.

[TABLE]

[TABLE]

• •

Exchange Law.

[TABLE]

• •

Conjugate Definition.

[TABLE]

• •

Conjugate Laws.

[TABLE]

[TABLE]

[TABLE]

[TABLE]

• •

Inverse Definition.

[TABLE]

• •

Inverse Law.

[TABLE]

• •

Alternative Laws. Special versions of associativity.

[TABLE]

[TABLE]

[TABLE]

• •

Other Theorems.

[TABLE]

[TABLE]

[TABLE]

3 Composition Algebra Doubling.

Use encapsulate to axiomatize, in ACL2(r), two composition algebras, with vector predicates $V_{\_}{1}p$ and $V_{\_}{2}p$. The vectors satisfying $V_{\_}{2}p$ are ordered pairs of elements satisfying $V_{\_}{1}p$. Both algebras, individually, satisfy all the axioms (and also all theorems) of the previous section. These additional axioms connect the various vector operations of the two spaces:

• •

Additional Axioms.

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

Since both $V_{\_}{1}p$ and $V_{\_}{2}p$ are composition algebras,

[TABLE]

Among the consequences of these encapsulated axioms, ACL2(r) verifies:

• •

Dot Product Doubling.

[TABLE]

• •

Conjugation Doubling.

[TABLE]

• •

Product Doubling.

[TABLE]

• •

Norm Doubling.

[TABLE]

• •

Associativity of $\bullet_{\_}{1}$.

[TABLE]

The above doubling theorems match the definitions used in the Cayley-Dickson Construction for making ordered pairs of $V_{\_}{1}p$ vectors into $V_{\_}{2}p$ vectors. Furthermore, if both the $V_{\_}{2}p$ ordered pairs and the the component $V_{\_}{1}p$ vectors form composition algebras, then the component $V_{\_}{1}p$ algebra has an associative multiplication.

In addition, ACL2(r) verifies that if the component $V_{\_}{1}p$ vectors form a composition algebra with an associative multiplication, then the Cayley-Dickson Construction makes the $V_{\_}{2}p$ ordered pairs into a composition algebra.

3.1 Summary

ACL2(r) verifies:

• •

Start with a composition algebra $V_{\_}{1}p$.

• •

Let $V_{\_}{2}p$ be the set of ordered pairs of elements from $V_{\_}{1}p$.

• •

Then

2. (a)

If $V_{\_}{2}p$ is also a composition algebra, then $V_{\_}{1}p$-multiplication is associative. 2. (b)

If $V_{\_}{1}p$-multiplication is associative, then $V_{\_}{2}p$ can be made into a composition algebra. 2. 2.

1. (a)

If $V_{\_}{2}p$ is a composition algebra with associative multiplication, then $V_{\_}{1}p$-multiplication is associative and commutative. 2. (b)

If $V_{\_}{1}p$-multiplication is associative and commutative, then $V_{\_}{2}p$ can be made into a composition algebra with associative multiplication. 3. 3.

1. (a)

If $V_{\_}{2}p$ is a composition algebra with associative and commutative multiplication, then $V_{\_}{1}p$-multiplication is also associative and commutative, and $V_{\_}{1}p$-conjugation is trivial. 2. (b)

If $V_{\_}{1}p$-multiplication is associative and commutative, and

$V_{\_}{1}p$-conjugation is trivial, then $V_{\_}{2}p$ can be made into a composition algebra with associative and commutative multiplication.

3.1.1 A last example

Apply the Cayley-Dickson Construction to pairs of octonions. Think of the octonions as eight-dimensional vectors. Interpret ordered pairs of octonions as sixteen-dimensional vectors called Sedenions [6]: For octonians

[TABLE]

[TABLE]

For octonion

[TABLE]

is the conjugate of $o$.

For octonions $o_{\_}{1}$, $o_{\_}{2}$, $p_{\_}{1}$, and $p_{\_}{2}$, sedenion multiplication is defined by

[TABLE]

Recall the octonians have a non-trivial conjugate and octonian multiplication is not commutative and also not associative. The octonions form a composition algebra, so that for octonions $o$ and $p$, $\|o\cdot p\|=\|o\|\cdot\|p\|$.

By item 1(a) listed above about composition algebras, since octonian multiplication is not associative, the sedenions is not a composition algebra. In fact, the sedenion product of nonzero vectors could be the zero vector. For example, let $o_{\_}{1}$, $o_{\_}{2}$, $p_{\_}{1}$, and $p_{\_}{2}$ be these otonions:

[TABLE]

Then

[TABLE]

So

[TABLE]

but

[TABLE]

and

[TABLE]

All nonzero sedenions have multiplicative inverses. For example,

[TABLE]

Appendix A ACL2(r) Books

A.1 cayley1.lisp

The Reals form a (1-dimensional) composition algebra.

A.2 cayley1a.lisp

Cons pairs of Reals form a (2-dimensional) composition algebra.

This algebra is (isomorphic to) the Complex Numbers.

A.3 cayley1b.lisp

Cons pairs of Complex Numbers form a (4-dimensional) composition algebra.

This algebra is (isomorphic to) the Quaternions.

3-Dimensional Vector Cross Product and 3-Dimensional Dot Product are related to 4-Dimensional Quaternion Multiplication.

A.4 cayley1c.lisp

Cons pairs of Quaternions form a (8-dimensional) composition algebra.

This algebra is (isomorphic to) the Octonions.

7-Dimensional Vector Cross Product and 7-Dimensional Dot Product are related to 8-Dimensional Octonion Multiplication.

A.5 cayley1d.lisp

Cons pairs of Octonions form a (16-dimensional) algebra.

This algebra is (isomorphic to) the Sedenions.

This algebra is not a composition algebra, but all nonzero Sedenions have multiplicative inverses.

A.6 cayley2.lisp

Axioms and theory of composition algebras.

A.7 cayley2.lisp

In composition algebras, $\|v\|=v\odot v$.

A.8 cayley3.lisp

Start with a composition algebra V1. Let V2 be the set of ordered pairs of elements from V1.

If V2 is also a composition algebra, then V1-multiplication is associative.

A.9 cayley3a.lisp

Start with a composition algebra V. Let V2 be the set of ordered pairs of elements from V.

If V-multiplication is associative, then V2 can be made into a composition algebra.

A.10 cayley4.lisp

Start with a composition algebra V1. Let V2 be the set of ordered pairs of elements from V1.

If V2 is a composition algebra with associative multiplication, then V1-multiplication is associative and commutative.

A.11 cayley4a.lisp

Start with a composition algebra V. Let V2 be the set of ordered pairs of elements from V.

If V-multiplication is associative and commutative, then V2 can be made into a composition algebra with associative multiplication.

A.12 cayley5.lisp

Start with a composition algebra V1. Let V2 be the set of ordered pairs of elements from V1.

If V2 is a composition algebra with associative and commutative multiplication, then V1-multiplication is associative and commutative, and V1-conjugation is trivial.

A.13 cayley5a.lisp

Start with a composition algebra V. Let V2 be the set of ordered pairs of elements from V.

If V-multiplication is associative and commutative, and V-conjugation is trivial, then V2 can be made into a composition algebra with associative and commutative multiplication.