# 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.

## Key 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?