groebner.egi

--
-- Groebner bases: the value-level engine of
-- lib/math/algebra/groebner.egi (design/cas-simplification.md G2).
-- The declare ideal declaration is tested separately in ideal.egi:
-- its rules are batch-scoped, so they would rewrite the radical
-- symbols in this file's value-level tests too.
--

declare symbol s2, s3, s6
declare symbol x, y, z
declare symbol θ, φ, α

-- completion: multiplication table of {1, √2, √3, √6}
def gb := groebnerBasis [s2^2 - 2, s3^2 - 3, s6 - s2 * s3]
assertEqual "multiplication table"
  (show gb)
  "[s2^2 - 2, s2 s3 - s6, s2 s6 - 2 * s3, s3^2 - 3, s3 s6 - 3 * s2, s6^2 - 6]"
assertEqual "completed rule sqrt2*sqrt6" (polyNF gb (s2 * s6)) (2 * s3)

-- normal form, membership, invariance
assertEqual "binomial square" (polyNF gb ((s2 + s3)^2)) (2 * s6 + 5)
assertEqual "ideal membership" (polyNF gb (s2 * s3 - s6)) 0
assertEqual "NF invariant under ideal shifts"
  (polyNF gb ((s2 + s3)^2 + (s2^2 - 2) * (s6 + 7)))
  (polyNF gb ((s2 + s3)^2))

-- textbook example: cyclic-3
def cyc := groebnerBasis [x + y + z, x*y + y*z + z*x, x*y*z - 1]
assertEqual "cyclic-3 reduced basis" (show cyc) "[z + y + x, y^2 + x^2 + x y, x^3 - 1]"
assertEqual "x^5 y mod cyclic-3" (polyNF cyc (x^5 * y)) (x^2 * y)

-- keep-prefix semantics of the explicit priority list
assertEqual "keep y" (polyNFWith [y] [x + y] (x^3)) (- y^3)
assertEqual "keep x" (polyNFWith [x] [x + y] (y^3)) (- x^3)

-- trigonometric atoms via the lib helper (rule-suppression quote inside)
assertEqual "trig generator survives construction"
  (show (trigIdeal θ)) "[('sin θ)^2 + ('cos θ)^2 - 1]"
assertEqual "sin^4 - cos^4, keep sin"
  (polyNFWith [('sin θ)] (trigIdeal θ) ((sin θ)^4 - (cos θ)^4))
  (2 * (sin θ)^2 - 1)

-- guards: fail-open on Laurent / fractions, trivial ideals
assertEqual "empty ideal" (groebnerBasis []) []
assertEqual "unit ideal" (groebnerBasis [5]) [1]
assertEqual "laurent fail-open" (groebnerBasis [x / y]) [x / y]
assertEqual "univariate power" (polyNF [x^2 - 2] (x^6)) 8

--
-- Observability and the safe one-call forms.
--

assertEqual "polyNFStatus ok" (polyNFStatus [x^2 - 2] (x^4)) ("ok", 4)
assertEqual "polyNFStatus fail-open"
  (fst (polyNFStatus [x^2 - 2] (x / y))) "fail-open"
assertEqual "idealNF completes its generators"
  (idealNF [s2^2 - 2, s3^2 - 3, s6 - s2 * s3] (s2 * s6)) (2 * s3)
assertEqual "idealEquals via one difference test"
  (idealEquals [s2^2 - 2, s3^2 - 3, s6 - s2 * s3] ((s2 + s3)^2) (2 * s6 + 5))
  True

--
-- The coefficient-field engine: GF(4) = F_2[α]/(α^2 + α + 1).
--

def red2 (c: MathValue) : MathValue := i.modulo c 2
def fdiv2 (a: MathValue) (b: MathValue) : MathValue := i.modulo (a * i.modulo b 2) 2

def gb4 := groebnerBasisField red2 fdiv2 [] [α^2 + α + 1]
assertEqual "GF(4) basis" (show gb4) "[α^2 + α + 1]"
assertEqual "GF(4): (α+1)^2 = α" (polyNFField red2 fdiv2 [] gb4 ((α + 1)^2)) α
assertEqual "GF(4): α (α+1) = 1" (polyNFField red2 fdiv2 [] gb4 (α * (α + 1))) 1
assertEqual "GF(4): α^3 = 1" (polyNFField red2 fdiv2 [] gb4 (α^3)) 1

--
-- The four-term fifth root of unity: the real part of z4^5 collapses
-- to 1 by arithmetic (principal-branch atoms), and the imaginary
-- residue vanishes modulo the pair-product relations of the
-- (all-positive-radicand) atoms.
--

def z4 := (-1 + (sqrt 5) + sqrt(-5 - 2*(sqrt 5)) + sqrt(-5 + 2*(sqrt 5))) / 4
def radicalRels :=
  [ '((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 "z4^5 = 1" (idealNF radicalRels (z4^5 - 1)) 0