# Bioctonion

# 1 Properties

This small Haskell program finds a counter-example to the property

(x x^*) y = x (x^* y)

and checks some other properties too.

See Fediverse thread: https://mathstodon.xyz/@johncarlosbaez/115367621334052139

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import qualified Prelude
import Prelude (IO, Bool, Integer, Eq((==)), Show)
import Test.QuickCheck (Arbitrary, quickCheck)

-- *-algebra

class StarAlgebra a where
  negate :: a -> a
  conjugate :: a -> a
  (+) :: a -> a -> a
  (-) :: a -> a -> a
  a - b = a + negate b
  (*) :: a -> a -> a

infixl 7 *
infixl 6 +, -

-- base case

type Z = Integer

instance StarAlgebra Z where
  negate a = Prelude.negate a
  conjugate a = a
  a + b = a Prelude.+ b
  a * b = a Prelude.* b
  a - b = a Prelude.- b

-- Cayley-Dickson construction

newtype CayleyDickson a = CayleyDickson (a, a)
  deriving (Eq, Show, Arbitrary)

instance StarAlgebra a => StarAlgebra (CayleyDickson a) where
  negate (CayleyDickson (a, b)) = CayleyDickson (negate a, negate b)
  conjugate (CayleyDickson (a, b)) = CayleyDickson (conjugate a, negate b)
  CayleyDickson (a, b) + CayleyDickson (c, d) = CayleyDickson (a + c, b + d)
  CayleyDickson (a, b) * CayleyDickson (c, d) = CayleyDickson
    (a * c - conjugate d * b, d * a + b * conjugate c)

-- complex numbers
type C = CayleyDickson Z

-- quaternions
type H = CayleyDickson C

-- octonions
type O = CayleyDickson H

-- complexification

newtype Bi a = Bi (a, a)
  deriving (Show, Eq, Arbitrary)

instance StarAlgebra a => StarAlgebra (Bi a) where
  negate (Bi (a, b)) = Bi (negate a, negate b)
  conjugate (Bi (a, b)) = Bi (conjugate a, negate (conjugate b))
  Bi (a, b) + Bi (c, d) = Bi (a + c, b + d)
  Bi (a, b) * Bi (c, d) = Bi (a * c - b * d, a * d + b * c)

-- a property of bioctonions that doesn't hold
prop_Baez :: Bi O -> Bi O -> Bool
prop_Baez x y =
  (x * conjugate x) * y ==
  x * (conjugate x * y)

-- a property of octonions that seems to hold
prop_claude :: O -> O -> O -> Bool
prop_claude a b c =
  (b * a) * c - b * (a * c) ==
  (a * conjugate b) * c - a * (conjugate b * c)

-- a property of bioctonions that seems to hold
prop_Gerenuk :: Bi O -> Bi O -> Bool
prop_Gerenuk x y =
  (x * conjugate x) * y - x * (conjugate x * y) ==
  (y * x) * conjugate x - y * (x * conjugate x)

-- check the properties
main :: IO ()
main = do
  quickCheck prop_Baez
  quickCheck prop_claude
  quickCheck prop_Gerenuk

Download: bioctonion.hs