5th-root-of-unity.egi

--
-- This file has been auto-generated by egison-translator.
--

def z : MathValue := rtu 5

def a11 : MathValue := z ^ 1 + z ^ 4

def a12 : MathValue := z ^ 2 + z ^ 3

def b10 : MathValue := a11 + a12

def b11 : MathValue := a11 - a12

def b12 : MathValue := a12 - a11

assertEqual "b10" b10 (-1)

def b10' : MathValue := b10

def b11' : MathValue := sqrt (b11 ^ 2)

def a11' : MathValue := (b10' + b11') / 2

def a12' : MathValue := (b10' - b11') / 2

def a21 : MathValue := z ^ 1 - z ^ 4

def a22 : MathValue := z ^ 2 - z ^ 3

def b20 : MathValue := a21 + a22

def b21 : MathValue := a21 - a22

def b22 : MathValue := a22 - a21

def b20' : MathValue := sqrt ((-3) + 4 * a12')

def b21' : MathValue := sqrt ((-3) + 4 * a11')

def a21' : MathValue := (b20' + b21') / 2

def a22' : MathValue := (b20' - b21') / 2

def z1' : MathValue := (a11' + a21') / 2

assertEqual
  "5th-root-of-unity"
   z1'
  ((-1 + sqrt 5 + sqrt (-5 - 2 * sqrt 5) + sqrt (-5 + 2 * sqrt 5)) / 4)

-- The check that motivated the radical work: z1'^5 = 1.  After the
-- principal-branch normalization every sqrt atom has a positive
-- radicand, the real part collapses arithmetically, and the imaginary
-- residue vanishes modulo the pair-product relations of the radical
-- atoms, applied once at this comparison point via idealNF.
def radicalRels : [MathValue] :=
  [ '((sqrt (5 + 2 * sqrt 5))^2 - 5 - 2 * sqrt 5)
  , '((sqrt (5 - 2 * sqrt 5))^2 - 5 + 2 * sqrt 5)
  , '((sqrt (5 + 2 * sqrt 5)) * (sqrt (5 - 2 * sqrt 5)) - sqrt 5)
  , '((sqrt 5)^2 - 5)
  , '(i^2 + 1) ]

assertEqual "z1'^5 = 1" (idealNF radicalRels (z1'^5 - 1)) 0