help links subscribe changes refresh edit

	The Algebra of Complex Numbers Is Frobenius In Many Ways
	↑

CaleyDickson

Edit detail for CaleyDickson revision 9 of 18

	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
Editor: Bill Page Time: 2011/04/18 19:51:41 GMT-7
Note: split-octonions and properties

removed:
-        --print(x::OutputForm * y::OutputForm)

added:
    norm(x:%):C == retract(conjugate(x)*x)


changed:
-)set output tex on
-)set output algebra off
-\end{axiom}
R := Expression Integer
\end{axiom}

changed:
-C := CaleyDickson(FRAC INT,'i,1)
C := CaleyDickson(R,'i,1)

removed:
-c:C := scalar [2,3]

changed:
-Cg:ILIST(Complex FRAC INT,0) := construct map(x+-> complex(x.1,x.2),
Cg:ILIST(Complex R,0) := construct map(x+-> complex(x.1,x.2),

changed:
-\end{axiom}
-- normed?
c1:C := scalar [subscript('c1,[i]) for i in 1..2]
c2:C := scalar [subscript('c2,[i]) for i in 1..2]
c3:C := scalar [subscript('c3,[i]) for i in 1..8]
-- Normed?
test(norm(c1*c2)=norm(c1)*norm(c2))
-- Commutative?
test( c1 * c2 = c2 * c1 )
-- Associative?
test((c1 * c2) * c3 = c1 * (c2 * c3))
\end{axiom}

removed:
-q:Q := scalar [2,3,4,5]

changed:
-Qg:ILIST(Quaternion FRAC INT,0) := construct map(x+-> quatern(x.1,x.2,x.3,x.4),
Qg:ILIST(Quaternion R,0) := construct map(x+-> quatern(x.1,x.2,x.3,x.4),

changed:
--- non-commutative
-test( Qe.1 * Qe.2 = - Qe.2 * Qe.1 )
-\end{axiom}
q1:Q := scalar [subscript('q1,[i]) for i in 1..4]
q2:Q := scalar [subscript('q2,[i]) for i in 1..4]
q3:Q := scalar [subscript('q3,[i]) for i in 1..8]
-- Normed?
test( norm(q1*q2) = norm(q1)*norm(q2))
-- Commutative?
test( q1 * q2 = q2 * q1 )
-- Associative?
test((q1 * q2) * q3 = q1 * (q2 * q3))
\end{axiom}

removed:
-o:O := scalar [2,3,4,5,6,7,8,9]

changed:
-Og:ILIST(Octonion FRAC INT,0):=map(x+-> octon(x.1,x.2,x.3,x.4,x.5,x.6,x.7,x.8),
Og:ILIST(Octonion R,0):=map(x+-> octon(x.1,x.2,x.3,x.4,x.5,x.6,x.7,x.8),

changed:
--- Non-commutative
-test( Oe.2 * Oe.4 = - Oe.4 * Oe.2 )
--- Non-associative
-test((Oe.2 * Oe.4) * Oe.7 = - Oe.2 * (Oe.4 * Oe.7))
-\end{axiom}
o1:O := scalar [subscript('o1,[i]) for i in 1..8]
o2:O := scalar [subscript('o2,[i]) for i in 1..8]
o3:O := scalar [subscript('o3,[i]) for i in 1..8]
-- normed?
test(norm(o1*o2)=norm(o1)*norm(o2))
-- Commutative?
test( o1 * o2 = o2 * o1 )
-- Associative?
test((o1 * o2) * o3 = o1 * (o2 * o3))
-- Alternative?
test((o1 * o2) * o1 = o1 * (o2 * o1))
\end{axiom}

Split-Octonions

Ref: http://en.wikipedia.org/wiki/Split-octonion

Note: Our table below is not identical the one shown in the reference where a different convention is used to define multiplication.

\begin{axiom}
sO:=CaleyDickson(Q,'ℓ,-1)
rank()$sO
sOe:ILIST(sO,0) := construct entries basis()$sO
matrix [[sOe.i * sOe.j for j in 0..#sOe-1] for i in 0..#sOe-1]
so1:sO := scalar [subscript('so1,[i]) for i in 1..8]
so2:sO := scalar [subscript('so2,[i]) for i in 1..8]
so3:sO := scalar [subscript('so3,[i]) for i in 1..8]
-- Normed?
test(norm(so1*so2)=norm(so1)*norm(so2))
-- Commutative?
test( so1 * so2 = so2 * so1 )
-- Associative?
test((so1 * so2) * so3 = so1 * (so2 * so3))
-- Alternative?
test((so1 * so2) * so1 = - so1 * (so2 * so1))
\end{axiom}

removed:
-s:S := scalar [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17]

changed:
--- Non-commutative
-test( Se.3 * Se.10 = - Se.10 * Se.3 )
--- Non-associative
-test( (Se.3 * Se.6) * Se.11 =  -Se.3 * (Se.6 * Se.11) )
s1:S := scalar [subscript('s1,[i]) for i in 1..16]
s2:S := scalar [subscript('s2,[i]) for i in 1..16]
s3:S := scalar [subscript('s3,[i]) for i in 1..16]
-- normed?
test(norm(s1*s2)=norm(s1)*norm(s2))
-- Commutative
test( s1 * s2 = s2 * s1 )
-- Associative?
test( (s1 * s2) * s3 =  s1 * (s2 * s3) )
-- Alternative?
test((s1 * s2) * s1 = - s1 * (s2 * s1))
-- Power Associateive?
test((s1 * s1) * s1 = s1 * (s1 * s1))

Ref:

http://en.wikipedia.org/wiki/Cayley%E2%80%93Dickson_construction

"The Cayley–Dickson construction, named after Arthur Cayley and Leonard Eugene Dickson, produces a sequence of algebras over the field of real numbers, each with twice the dimension of the previous one. The algebras produced by this process are known as Cayley–Dickson algebras; since they extend the complex numbers, ... "

complex numbers, quaternions, octonions, sedenions, ...

http://en.wikipedia.org/wiki/Hypercomplex_number

spad

)abbrev domain CALEY CaleyDickson
CaleyDickson(C:CommutativeRing,gen:Symbol,gamma:C):ComplexCategory(C) with
    scalar:List % -> %
  == add
    Rep == DirectProduct(2,C)
    rep(x:%):Rep == x pretend Rep
    per(x:Rep):% == x pretend %

    pair(x:C,y:C):Rep == directProduct vector [x,y]
    complex(x:C,y:C):% == per pair(x,y)
    real(x:%):C == rep(x).1
    imag(x:%):C == rep(x).2

    0:% == complex(0,0)
    zero?(x:%):Boolean == zero? rep(x)
    1:% == per pair(1,0)
    one?(x:%):Boolean  == one? real x and zero? imag x

    if C has conjugate:C->C then
      -- In general we need conjugate
      (x:% * y:%):% ==
        complex(real x * real y - gamma*conjugate imag y * imag x,
                imag y * real x + imag x * conjugate real y)
      conjugate(x:%):% == complex(conjugate(real x), -imag x)
    else
      -- If not complex then conjugate is identity
      (x:% * y:%):% ==
        complex(real x * real y - gamma*imag y * imag x,
                imag y * real x + imag x * real y)
      conjugate(x:%):% == complex(real x, -imag x)

    norm(x:%):C == retract(conjugate(x)*x)

    if C has Field then
      inv(x:%):% == per(inv(real(conjugate x * x))$C * rep conjugate x)
      (x:% / y:%):% == x * inv(y)

    if C has rank:()->PositiveInteger then
      rank():PositiveInteger == 2*rank()$C
    else
      rank():PositiveInteger == 2

    if C has basis:()->Vector C then
      basis():Vector % ==
        concat([complex(i,0) for i in entries basis()$C],
               [complex(0,i) for i in entries basis()$C])
    else
      basis():Vector % == [1,imaginary()]

    if C has scalar:List C -> C then
      scalar(x:List %):% ==
        h:Integer := divide(#x,2).quotient
        complex(scalar([retract(x.i)@C for i in 1..h]),scalar([retract(x.i)@C for i in h+1..#x]))
    else
      scalar(x:List %):% == complex(retract x.1,retract x.2)

    coerce(x:%):OutputForm ==
      outr:=real(x)::OutputForm
      imag x = 0 => return outr
      outi := hconcat(imag(x)::OutputForm, gen::OutputForm)
      if imag x = 1 then
        outi := gen::OutputForm
      if imag x = -1 then
        outi := -(gen::OutputForm)
      if C has imaginary:()->C then
        if imag x = -imaginary()$C then
          outi := -hconcat(imaginary()$C::OutputForm,gen::OutputForm)
      real x = 0 => return outi
      return outr + outi 
    --
    -- Many other funtctions are inherited from ComplexCategory
    --
    -- To Do:
    -- 1) Check which other functions are still correct for higher-order algebras!
    --
    -- re-defined these only to save function calls
    (x:% + y:%):% == per(rep x + rep y)
    (x:% = y:%):Boolean == rep x = rep y

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/442641077606971384-25px001.spad using 
      old system compiler.
   CALEY abbreviates domain CaleyDickson 
------------------------------------------------------------------------
   initializing NRLIB CALEY for CaleyDickson 
   compiling into NRLIB CALEY 
****** Domain: C already in scope
   compiling local rep : $ -> DirectProduct(2,C)
      CALEY;rep is replaced by x 
Time: 0.36 SEC.

   compiling local per : DirectProduct(2,C) -> $
      CALEY;per is replaced by x 
Time: 0 SEC.

   compiling local pair : (C,C) -> DirectProduct(2,C)
Time: 0.02 SEC.

   compiling exported complex : (C,C) -> $
Time: 0 SEC.

   compiling exported real : $ -> C
Time: 0 SEC.

   compiling exported imag : $ -> C
Time: 0.01 SEC.

   compiling exported Zero : () -> $
Time: 0 SEC.

   compiling exported zero? : $ -> Boolean
Time: 0 SEC.

   compiling exported One : () -> $
Time: 0 SEC.

   compiling exported one? : $ -> Boolean
Time: 0.01 SEC.

augmenting C: (SIGNATURE C conjugate (C C))
   compiling exported * : ($,$) -> $
Time: 0.01 SEC.

   compiling exported conjugate : $ -> $
Time: 0 SEC.

   compiling exported * : ($,$) -> $
Time: 0.01 SEC.

   compiling exported conjugate : $ -> $
Time: 0 SEC.

   compiling exported norm : $ -> C
Time: 0.03 SEC.

****** Domain: C already in scope
augmenting C: (Field)
   compiling exported inv : $ -> $
Time: 0 SEC.

   compiling exported / : ($,$) -> $
Time: 0 SEC.

augmenting C: (SIGNATURE C rank ((PositiveInteger)))
   compiling exported rank : () -> PositiveInteger
Time: 0 SEC.

   compiling exported rank : () -> PositiveInteger
      CALEY;rank;Pi;19 is replaced by 2 
Time: 0 SEC.

augmenting C: (SIGNATURE C basis ((Vector C)))
   compiling exported basis : () -> Vector $
Time: 0.04 SEC.

   compiling exported basis : () -> Vector $
Time: 0 SEC.

augmenting C: (SIGNATURE C scalar (C (List C)))
   compiling exported scalar : List $ -> $
Time: 0.05 SEC.

   compiling exported scalar : List $ -> $
Time: 0.01 SEC.

   compiling exported coerce : $ -> OutputForm
augmenting C: (SIGNATURE C imaginary (C))
Time: 0.02 SEC.

   compiling exported + : ($,$) -> $
Time: 0 SEC.

   compiling exported = : ($,$) -> Boolean
Time: 0 SEC.

****** Domain: C already in scope
augmenting C: (EuclideanDomain)
****** Domain: C already in scope
augmenting C: (PolynomialFactorizationExplicit)
****** Domain: C already in scope
augmenting C: (RadicalCategory)
****** Domain: C already in scope
augmenting C: (TranscendentalFunctionCategory)
****** Domain: C already in scope
augmenting C: (RealNumberSystem)
****** Domain: C already in scope
augmenting C: (TranscendentalFunctionCategory)
****** Domain: C already in scope
augmenting C: (Comparable)
****** Domain: C already in scope
augmenting C: (ConvertibleTo (InputForm))
****** Domain: C already in scope
augmenting C: (ConvertibleTo (Pattern (Float)))
****** Domain: C already in scope
augmenting C: (ConvertibleTo (Pattern (Integer)))
****** Domain: C already in scope
augmenting C: (DifferentialRing)
****** Domain: C already in scope
augmenting C: (Eltable C C)
****** Domain: C already in scope
augmenting C: (EuclideanDomain)
****** Domain: C already in scope
augmenting C: (Evalable C)
****** Domain: C already in scope
augmenting C: (Field)
****** Domain: C already in scope
augmenting C: (Finite)
****** Domain: C already in scope
augmenting C: (FiniteFieldCategory)
****** Domain: C already in scope
augmenting C: (InnerEvalable (Symbol) C)
****** Domain: C already in scope
augmenting C: (IntegerNumberSystem)
****** Domain: C already in scope
augmenting C: (IntegralDomain)
****** Domain: C already in scope
augmenting C: (LinearlyExplicitRingOver (Integer))
****** Domain: C already in scope
augmenting C: (PartialDifferentialRing (Symbol))
****** Domain: C already in scope
augmenting C: (PatternMatchable (Float))
****** Domain: C already in scope
augmenting C: (PatternMatchable (Integer))
****** Domain: C already in scope
augmenting C: (RealConstant)
****** Domain: C already in scope
augmenting C: (RealNumberSystem)
****** Domain: C already in scope
augmenting C: (RetractableTo (Fraction (Integer)))
****** Domain: C already in scope
augmenting C: (RetractableTo (Integer))
****** Domain: C already in scope
augmenting C: (TranscendentalFunctionCategory)
(time taken in buildFunctor:  2290)

;;;     ***       |CaleyDickson| REDEFINED

;;;     ***       |CaleyDickson| REDEFINED
Time: 2.46 SEC.

   Cumulative Statistics for Constructor CaleyDickson
      Time: 3.03 seconds

   finalizing NRLIB CALEY 
   Processing CaleyDickson for Browser database:
--->-->CaleyDickson((scalar (% (List %)))): Not documented!!!!
--->-->CaleyDickson(constructor): Not documented!!!!
--->-->CaleyDickson(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/CALEY.NRLIB/CALEY.lsp" (written 18 APR 2011 07:51:08 PM):

; /var/zope2/var/LatexWiki/CALEY.NRLIB/CALEY.fasl written
; compilation finished in 0:00:00.736
------------------------------------------------------------------------
   CaleyDickson is now explicitly exposed in frame initial 
   CaleyDickson will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/CALEY.NRLIB/CALEY

   >> System error:
   The bounding indices 163 and 162 are bad for a sequence of length 162.
See also:
  The ANSI Standard, Glossary entry for "bounding index designator"
  The ANSI Standard, writeup for Issue SUBSEQ-OUT-OF-BOUNDS:IS-AN-ERROR

Test

axiom

R := Expression Integer

$\label{eq1}\hbox{\axiomType{Expression}\ } (\hbox{\axiomType{Integer}\ })$

(1)

Type: Type

Complex Numbers

axiom

C := CaleyDickson(R,'i,1)

$\label{eq2}\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{Expression}\ } (\hbox{\axiomType{Integer}\ }) , i , 1)$

(2)

Type: Type

axiom

rank()$C

$\label{eq3}2$

(3)

Type: PositiveInteger?

axiom

Ce:ILIST(C,0) := construct entries basis()$C

$\label{eq4}\left[ 1, \: i \right]$

(4)

Type: IndexedList?(CaleyDickson?(Expression(Integer),i,1),0)

axiom

matrix [[Ce.i * Ce.j for j in 0..#Ce-1] for i in 0..#Ce-1]

$\label{eq5}\left[ \begin{array}{cc} 1 & i \ i & - 1$

(5)

Type: Matrix(CaleyDickson?(Expression(Integer),i,1))

axiom

--
-- compare
--
Cg:ILIST(Complex R,0) := construct map(x+-> complex(x.1,x.2),
           1$SquareMatrix(2,FRAC INT)::List List FRAC INT)

$\label{eq6}\left[ 1, \: i \right]$

(6)

Type: IndexedList?(Complex(Expression(Integer)),0)

axiom

matrix [[Cg.i * Cg.j for j in 0..#Cg-1] for i in 0..#Cg-1]

$\label{eq7}\left[ \begin{array}{cc} 1 & i \ i & - 1$

(7)

Type: Matrix(Complex(Expression(Integer)))

axiom

-- normed?
c1:C := scalar [subscript('c1,[i]) for i in 1..2]

$\label{eq8}{c 1_{1}}+{{c 1_{2}}i}$

(8)

Type: CaleyDickson?(Expression(Integer),i,1)

axiom

c2:C := scalar [subscript('c2,[i]) for i in 1..2]

$\label{eq9}{c 2_{1}}+{{c 2_{2}}i}$

(9)

Type: CaleyDickson?(Expression(Integer),i,1)

axiom

c3:C := scalar [subscript('c3,[i]) for i in 1..8]

$\label{eq10}{c 3_{1}}+{{c 3_{2}}i}$

(10)

Type: CaleyDickson?(Expression(Integer),i,1)

axiom

-- Normed?
test(norm(c1*c2)=norm(c1)*norm(c2))

$\label{eq11} \mbox{\rm true}$

(11)

Type: Boolean

axiom

-- Commutative?
test( c1 * c2 = c2 * c1 )

$\label{eq12} \mbox{\rm true}$

(12)

Type: Boolean

axiom

-- Associative?
test((c1 * c2) * c3 = c1 * (c2 * c3))

$\label{eq13} \mbox{\rm true}$

(13)

Type: Boolean

Quaternions

axiom

Q := CaleyDickson(C,'j,1)

$\label{eq14}\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{Expression}\ } (\hbox{\axiomType{Integer}\ }) , i , 1) , j , 1)$

(14)

Type: Type

axiom

rank()$Q

$\label{eq15}4$

(15)

Type: PositiveInteger?

axiom

Qe:ILIST(Q,0) := construct entries basis()$Q

$\label{eq16}\left[ 1, \: i , \: j , \:{ij}\right]$

(16)

Type: IndexedList?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),0)

axiom

matrix [[Qe.i * Qe.j for j in 0..#Qe-1] for i in 0..#Qe-1]

$\label{eq17}\left[ \begin{array}{cccc} 1 & i & j &{ij} \ i & - 1 &{ij}& - j \ j & -{ij}& - 1 & i \ {ij}& j & - i & - 1$

(17)

Type: Matrix(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1))

axiom

--
-- compare
--
Qg:ILIST(Quaternion R,0) := construct map(x+-> quatern(x.1,x.2,x.3,x.4),
           1$SquareMatrix(4,FRAC INT)::List List FRAC INT)

$\label{eq18}\left[ 1, \: i , \: j , \: k \right]$

(18)

Type: IndexedList?(Quaternion(Expression(Integer)),0)

axiom

matrix [[Qg.i * Qg.j for j in 0..#Qg-1] for i in 0..#Qg-1]

$\label{eq19}\left[ \begin{array}{cccc} 1 & i & j & k \ i & - 1 & k & - j \ j & - k & - 1 & i \ k & j & - i & - 1$

(19)

Type: Matrix(Quaternion(Expression(Integer)))

axiom

q1:Q := scalar [subscript('q1,[i]) for i in 1..4]

$\label{eq20}{q 1_{1}}+{{q 1_{2}}i}+{{{q 1_{3}}+{{q 1_{4}}i}}j}$

(20)

Type: CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1)

axiom

q2:Q := scalar [subscript('q2,[i]) for i in 1..4]

$\label{eq21}{q 2_{1}}+{{q 2_{2}}i}+{{{q 2_{3}}+{{q 2_{4}}i}}j}$

(21)

Type: CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1)

axiom

q3:Q := scalar [subscript('q3,[i]) for i in 1..8]

$\label{eq22}{q 3_{1}}+{{q 3_{2}}i}+{{{q 3_{5}}+{{q 3_{6}}i}}j}$

(22)

Type: CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1)

axiom

-- Normed?
test( norm(q1*q2) = norm(q1)*norm(q2))

$\label{eq23} \mbox{\rm true}$

(23)

Type: Boolean

axiom

-- Commutative?
test( q1 * q2 = q2 * q1 )

$\label{eq24} \mbox{\rm false}$

(24)

Type: Boolean

axiom

-- Associative?
test((q1 * q2) * q3 = q1 * (q2 * q3))

$\label{eq25} \mbox{\rm true}$

(25)

Type: Boolean

Octonions

Ref: http://en.wikipedia.org/wiki/Octonion

axiom

O:=CaleyDickson(Q,'k,1)

$\label{eq26}\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{Expression}\ } (\hbox{\axiomType{Integer}\ }) , i , 1) , j , 1) , k , 1)$

(26)

Type: Type

axiom

rank()$O

$\label{eq27}8$

(27)

Type: PositiveInteger?

axiom

Oe:ILIST(O,0) := construct entries basis()$O

$\label{eq28}\left[ 1, \: i , \: j , \:{ij}, \: k , \:{ik}, \:{jk}, \:{{ij}k}\right]$

(28)

Type: IndexedList?(CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1),0)

axiom

matrix [[Oe.i * Oe.j for j in 0..#Oe-1] for i in 0..#Oe-1]

$\label{eq29}\left[ \begin{array}{cccccccc} 1 & i & j &{ij}& k &{ik}&{jk}&{{ij}k} \ i & - 1 &{ij}& - j &{ik}& - k &{-{ij}k}&{jk} \ j & -{ij}& - 1 & i &{jk}&{{ij}k}& - k &{- ik} \ {ij}& j & - i & - 1 &{{ij}k}& -{jk}&{ik}& - k \ k &{- ik}& -{jk}&{-{ij}k}& - 1 & i & j &{ij} \ {ik}& k &{-{ij}k}&{jk}& - i & - 1 & -{ij}& j \ {jk}&{{ij}k}& k &{- ik}& - j &{ij}& - 1 & - i \ {{ij}k}& -{jk}&{ik}& k & -{ij}& - j & i & - 1$

(29)

Type: Matrix(CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1))

axiom

--
-- compare
--
Og:ILIST(Octonion R,0):=map(x+-> octon(x.1,x.2,x.3,x.4,x.5,x.6,x.7,x.8),
           1$SquareMatrix(8,FRAC INT)::List List FRAC INT)

$\label{eq30}\left[ 1, \: i , \: j , \: k , \: E , \: I , \: J , \: K \right]$

(30)

Type: IndexedList?(Octonion(Expression(Integer)),0)

axiom

matrix [[Og.i * Og.j for j in 0..#Og-1] for i in 0..#Og-1]

$\label{eq31}\left[ \begin{array}{cccccccc} 1 & i & j & k & E & I & J & K \ i & - 1 & k & - j & I & - E & - K & J \ j & - k & - 1 & i & J & K & - E & - I \ k & j & - i & - 1 & K & - J & I & - E \ E & - I & - J & - K & - 1 & i & j & k \ I & E & - K & J & - i & - 1 & - k & j \ J & K & E & - I & - j & k & - 1 & - i \ K & - J & I & E & - k & - j & i & - 1$

(31)

Type: Matrix(Octonion(Expression(Integer)))

axiom

o1:O := scalar [subscript('o1,[i]) for i in 1..8]

$\label{eq32}{o 1_{1}}+{{o 1_{2}}i}+{{{o 1_{3}}+{{o 1_{4}}i}}j}+{{{o 1_{5}}+{{o 1_{6}}i}+{{{o 1_{7}}+{{o 1_{8}}i}}j}}k}$

(32)

Type: CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1)

axiom

o2:O := scalar [subscript('o2,[i]) for i in 1..8]

$\label{eq33}{o 2_{1}}+{{o 2_{2}}i}+{{{o 2_{3}}+{{o 2_{4}}i}}j}+{{{o 2_{5}}+{{o 2_{6}}i}+{{{o 2_{7}}+{{o 2_{8}}i}}j}}k}$

(33)

Type: CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1)

axiom

o3:O := scalar [subscript('o3,[i]) for i in 1..8]

$\label{eq34}{o 3_{1}}+{{o 3_{2}}i}+{{{o 3_{3}}+{{o 3_{4}}i}}j}+{{{o 3_{5}}+{{o 3_{6}}i}+{{{o 3_{7}}+{{o 3_{8}}i}}j}}k}$

(34)

Type: CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1)

axiom

-- normed?
test(norm(o1*o2)=norm(o1)*norm(o2))

$\label{eq35} \mbox{\rm true}$

(35)

Type: Boolean

axiom

-- Commutative?
test( o1 * o2 = o2 * o1 )

$\label{eq36} \mbox{\rm false}$

(36)

Type: Boolean

axiom

-- Associative?
test((o1 * o2) * o3 = o1 * (o2 * o3))

$\label{eq37} \mbox{\rm false}$

(37)

Type: Boolean

axiom

-- Alternative?
test((o1 * o2) * o1 = o1 * (o2 * o1))

$\label{eq38} \mbox{\rm true}$

(38)

Type: Boolean

Split-Octonions

Ref: http://en.wikipedia.org/wiki/Split-octonion

Note: Our table below is not identical the one shown in the reference where a different convention is used to define multiplication.

axiom

sO:=CaleyDickson(Q,'ℓ,-1)

$\label{eq39}\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{Expression}\ } (\hbox{\axiomType{Integer}\ }) , i , 1) , j , 1) , � � , - 1)$

(39)

Type: Type

axiom

rank()$sO

$\label{eq40}8$

(40)

Type: PositiveInteger?

axiom

sOe:ILIST(sO,0) := construct entries basis()$sO

$\label{eq41}\left[ 1, \: i , \: j , \:{ij}, \: � � , \:{i � �}, \:{j � �}, \:{{ij}� �}\right]$

(41)

Type: IndexedList?(CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),ℓ,-1),0)

axiom

matrix [[sOe.i * sOe.j for j in 0..#sOe-1] for i in 0..#sOe-1]

$\label{eq42}\left[ \begin{array}{cccccccc} 1 & i & j &{ij}& � � &{i � �}&{j � �}&{{ij}� �} \ i & - 1 &{ij}& - j &{i � �}& - � � &{-{ij}� �}&{j � �} \ j & -{ij}& - 1 & i &{j � �}&{{ij}� �}& - � � &{- i � �} \ {ij}& j & - i & - 1 &{{ij}� �}& -{j � �}&{i � �}& - � � \ � � &{- i � �}& -{j � �}&{-{ij}� �}& 1 & - i & - j & -{ij} \ {i � �}& � � &{-{ij}� �}&{j � �}& i & 1 &{ij}& - j \ {j � �}&{{ij}� �}& � � &{- i � �}& j & -{ij}& 1 & i \ {{ij}� �}& -{j � �}&{i � �}& � � &{ij}& j & - i & 1$

(42)

Type: Matrix(CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),ℓ,-1))

axiom

so1:sO := scalar [subscript('so1,[i]) for i in 1..8]

$\label{eq43}{so 1_{1}}+{{so 1_{2}}i}+{{{so 1_{3}}+{{so 1_{4}}i}}j}+{{{so 1_{5}}+{{so 1_{6}}i}+{{{so 1_{7}}+{{so 1_{8}}i}}j}}� �}$

(43)

Type: CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),ℓ,-1)

axiom

so2:sO := scalar [subscript('so2,[i]) for i in 1..8]

$\label{eq44}{so 2_{1}}+{{so 2_{2}}i}+{{{so 2_{3}}+{{so 2_{4}}i}}j}+{{{so 2_{5}}+{{so 2_{6}}i}+{{{so 2_{7}}+{{so 2_{8}}i}}j}}� �}$

(44)

Type: CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),ℓ,-1)

axiom

so3:sO := scalar [subscript('so3,[i]) for i in 1..8]

$\label{eq45}{so 3_{1}}+{{so 3_{2}}i}+{{{so 3_{3}}+{{so 3_{4}}i}}j}+{{{so 3_{5}}+{{so 3_{6}}i}+{{{so 3_{7}}+{{so 3_{8}}i}}j}}� �}$

(45)

Type: CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),ℓ,-1)

axiom

-- Normed?
test(norm(so1*so2)=norm(so1)*norm(so2))

$\label{eq46} \mbox{\rm true}$

(46)

Type: Boolean

axiom

-- Commutative?
test( so1 * so2 = so2 * so1 )

$\label{eq47} \mbox{\rm false}$

(47)

Type: Boolean

axiom

-- Associative?
test((so1 * so2) * so3 = so1 * (so2 * so3))

$\label{eq48} \mbox{\rm false}$

(48)

Type: Boolean

axiom

-- Alternative?
test((so1 * so2) * so1 = - so1 * (so2 * so1))

$\label{eq49} \mbox{\rm false}$

(49)

Type: Boolean

Sedenions

Ref: http://en.wikipedia.org/wiki/Sedenion

axiom

S:=CaleyDickson(O,'l,1)

$\label{eq50}\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{CaleyDickson}\ } (\hbox{\axiomType{Expression}\ } (\hbox{\axiomType{Integer}\ }) , i , 1) , j , 1) , k , 1) , l , 1)$

(50)

Type: Type

axiom

rank()$S

$\label{eq51}16$

(51)

Type: PositiveInteger?

axiom

Se:ILIST(S,0) := construct entries basis()$S

$\label{eq52}\left[ 1, \: i , \: j , \:{ij}, \: k , \:{ik}, \:{jk}, \:{{ij}k}, \: l , \:{il}, \:{jl}, \:{{ij}l}, \:{kl}, \:{{ik}l}, \:{{jk}l}, \:{{{ij}k}l}\right]$

(52)

Type: IndexedList?(CaleyDickson?(CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1),l,1),0)

axiom

matrix [[Se.i * Se.j for j in 0..#Se-1] for i in 0..#Se-1]

$\label{eq53}\left[ \begin{array}{cccccccccccccccc} 1 & i & j &{ij}& k &{ik}&{jk}&{{ij}k}& l &{il}&{jl}&{{ij}l}&{kl}&{{ik}l}&{{jk}l}&{{{ij}k}l} \ i & - 1 &{ij}& - j &{ik}& - k &{-{ij}k}&{jk}&{il}& - l &{-{ij}l}&{jl}&{{- ik}l}&{kl}&{{{ij}k}l}&{-{jk}l} \ j & -{ij}& - 1 & i &{jk}&{{ij}k}& - k &{- ik}&{jl}&{{ij}l}& - l &{- il}&{-{jk}l}&{{-{ij}k}l}&{kl}&{{ik}l} \ {ij}& j & - i & - 1 &{{ij}k}& -{jk}&{ik}& - k &{{ij}l}&{- jl}&{il}& - l &{{-{ij}k}l}&{{jk}l}&{{- ik}l}&{kl} \ k &{- ik}& -{jk}&{-{ij}k}& - 1 & i & j &{ij}&{kl}&{{ik}l}&{{jk}l}&{{{ij}k}l}& - l &{- il}&{- jl}&{-{ij}l} \ {ik}& k &{-{ij}k}&{jk}& - i & - 1 & -{ij}& j &{{ik}l}& -{kl}&{{{ij}k}l}&{-{jk}l}&{il}& - l &{{ij}l}&{- jl} \ {jk}&{{ij}k}& k &{- ik}& - j &{ij}& - 1 & - i &{{jk}l}&{{-{ij}k}l}& -{kl}&{{ik}l}&{jl}&{-{ij}l}& - l &{il} \ {{ij}k}& -{jk}&{ik}& k & -{ij}& - j & i & - 1 &{{{ij}k}l}&{{jk}l}&{{- ik}l}& -{kl}&{{ij}l}&{jl}&{- il}& - l \ l &{- il}&{- jl}&{-{ij}l}& -{kl}&{{- ik}l}&{-{jk}l}&{{-{ij}k}l}& - 1 & i & j &{ij}& k &{ik}&{jk}&{{ij}k} \ {il}& l &{-{ij}l}&{jl}&{{- ik}l}&{kl}&{{{ij}k}l}&{-{jk}l}& - i & - 1 & -{ij}& j &{- ik}& k &{{ij}k}& -{jk} \ {jl}&{{ij}l}& l &{- il}&{-{jk}l}&{{-{ij}k}l}&{kl}&{{ik}l}& - j &{ij}& - 1 & - i & -{jk}&{-{ij}k}& k &{ik} \ {{ij}l}&{- jl}&{il}& l &{{-{ij}k}l}&{{jk}l}&{{- ik}l}&{kl}& -{ij}& - j & i & - 1 &{-{ij}k}&{jk}&{- ik}& k \ {kl}&{{ik}l}&{{jk}l}&{{{ij}k}l}& l &{- il}&{- jl}&{-{ij}l}& - k &{ik}&{jk}&{{ij}k}& - 1 & - i & - j & -{ij} \ {{ik}l}& -{kl}&{{{ij}k}l}&{-{jk}l}&{il}& l &{{ij}l}&{- jl}&{- ik}& - k &{{ij}k}& -{jk}& i & - 1 &{ij}& - j \ {{jk}l}&{{-{ij}k}l}& -{kl}&{{ik}l}&{jl}&{-{ij}l}& l &{il}& -{jk}&{-{ij}k}& - k &{ik}& j & -{ij}& - 1 & i \ {{{ij}k}l}&{{jk}l}&{{- ik}l}& -{kl}&{{ij}l}&{jl}&{- il}& l &{-{ij}k}&{jk}&{- ik}& - k &{ij}& j & - i & - 1$

(53)

Type: Matrix(CaleyDickson?(CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1),l,1))

axiom

s1:S := scalar [subscript('s1,[i]) for i in 1..16]

$\label{eq54}\begin{array}{@{}l} \displaystyle {s 1_{1}}+{{s 1_{2}}i}+{{{s 1_{3}}+{{s 1_{4}}i}}j}+{{{s 1_{5}}+{{s 1_{6}}i}+{{{s 1_{7}}+{{s 1_{8}}i}}j}}k}+ \ \ \displaystyle {{{s 1_{9}}+{{s 1_{10}}i}+{{{s 1_{11}}+{{s 1_{12}}i}}j}+{{{s 1_{13}}+{{s 1_{14}}i}+{{{s 1_{15}}+{{s 1_{16}}i}}j}}k}}l}$

(54)

Type: CaleyDickson?(CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1),l,1)

axiom

s2:S := scalar [subscript('s2,[i]) for i in 1..16]

$\label{eq55}\begin{array}{@{}l} \displaystyle {s 2_{1}}+{{s 2_{2}}i}+{{{s 2_{3}}+{{s 2_{4}}i}}j}+{{{s 2_{5}}+{{s 2_{6}}i}+{{{s 2_{7}}+{{s 2_{8}}i}}j}}k}+ \ \ \displaystyle {{{s 2_{9}}+{{s 2_{10}}i}+{{{s 2_{11}}+{{s 2_{12}}i}}j}+{{{s 2_{13}}+{{s 2_{14}}i}+{{{s 2_{15}}+{{s 2_{16}}i}}j}}k}}l}$

(55)

Type: CaleyDickson?(CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1),l,1)

axiom

s3:S := scalar [subscript('s3,[i]) for i in 1..16]

$\label{eq56}\begin{array}{@{}l} \displaystyle {s 3_{1}}+{{s 3_{2}}i}+{{{s 3_{3}}+{{s 3_{4}}i}}j}+{{{s 3_{5}}+{{s 3_{6}}i}+{{{s 3_{7}}+{{s 3_{8}}i}}j}}k}+ \ \ \displaystyle {{{s 3_{9}}+{{s 3_{10}}i}+{{{s 3_{11}}+{{s 3_{12}}i}}j}+{{{s 3_{13}}+{{s 3_{14}}i}+{{{s 3_{15}}+{{s 3_{16}}i}}j}}k}}l}$

(56)

Type: CaleyDickson?(CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1),l,1)

axiom

-- normed?
test(norm(s1*s2)=norm(s1)*norm(s2))

$\label{eq57} \mbox{\rm false}$

(57)

Type: Boolean

axiom

-- Commutative
test( s1 * s2 = s2 * s1 )

$\label{eq58} \mbox{\rm false}$

(58)

Type: Boolean

axiom

-- Associative?
test( (s1 * s2) * s3 =  s1 * (s2 * s3) )

$\label{eq59} \mbox{\rm false}$

(59)

Type: Boolean

axiom

-- Alternative?
test((s1 * s2) * s1 = - s1 * (s2 * s1))

$\label{eq60} \mbox{\rm false}$

(60)

Type: Boolean

axiom

-- Power Associateive?
test((s1 * s1) * s1 = s1 * (s1 * s1))

$\label{eq61} \mbox{\rm true}$

(61)

Type: Boolean

axiom

-- zero divisor
(Se.3 + Se.10) * (Se.6 - Se.15)

$\label{eq62}0$

(62)

Type: CaleyDickson?(CaleyDickson?(CaleyDickson?(CaleyDickson?(Expression(Integer),i,1),j,1),k,1),l,1)