def Hex.PolyQuot.Roots.monic {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) : DensePoly (PolyQuot p x)

Monic normalization over a checked fixed field.

Equations

• Hex.PolyQuot.Roots.monic f = if f.isZero = true then 0 else Hex.DensePoly.scale f.leadingCoeff⁻¹ f

def Hex.PolyQuot.Roots.derivative {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) : DensePoly (PolyQuot p x)

Formal derivative using the existing rational scalar action, avoiding any law-bearing cast instance on the computational fixed-field carrier.

Equations

• Hex.PolyQuot.Roots.derivative f = Hex.DensePoly.ofCoeffs (List.map (fun (i : Nat) => ↑(i + 1) • f.coeff (i + 1)) (List.range (f.size - 1))).toArray

def Hex.PolyQuot.Roots.yunAux {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (w repeated : DensePoly (PolyQuot p x)) (multiplicity fuel : Nat) (out : Array (DensePoly (PolyQuot p x) × Nat)) : Array (DensePoly (PolyQuot p x) × Nat)

Fuel-bounded characteristic-zero Yun loop. Each returned pair is a monic square-free component and its positive multiplicity index.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PolyQuot.Roots.yunAux w repeated multiplicity 0 out = out

def Hex.PolyQuot.Roots.yun {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) : Array (DensePoly (PolyQuot p x) × Nat)

Yun square-free decomposition over a checked fixed field. The zero and constant polynomials have no finite components; the public root driver handles their distinct root-set conventions.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.Roots.commonDen {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) : Nat

Common positive denominator of every rational coordinate occurring among the coefficients of f.

Equations

• Hex.PolyQuot.Roots.commonDen f = Array.foldl (fun (den : Nat) (a : Hex.PolyQuot p x) => Array.foldl (fun (den : Nat) (q : Rat) => den.lcm q.den) den a.coeffs.toArray) 1 f.toArray

def Hex.PolyQuot.Roots.clearRat (den : Nat) (q : Rat) : Int

Clear a rational coefficient against a common denominator.

Equations

• Hex.PolyQuot.Roots.clearRat den q = q.num * Int.ofNat (den / q.den)

def Hex.PolyQuot.Roots.clearedOuter {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) : DensePoly ZPoly

Regard a fixed-field polynomial as a polynomial in the generator y, with coefficients in Int[t], after clearing all rational denominators at once.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.Roots.normEliminant {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) : ZPoly

Integer norm eliminant Res_y(p(y), F(y,t)) of a fixed-field polynomial.

Equations

• Hex.PolyQuot.Roots.normEliminant f = p.liftOuter.resultant (Hex.PolyQuot.Roots.clearedOuter f)

def Hex.PolyQuot.Roots.candidateLift (e : ZPoly) : DensePoly (DensePoly ZPoly)

Constant trivariate lift of a candidate eliminant: regard e(z) as a polynomial in the candidate variable z whose coefficients are constant in both the generator variable y and the evaluation variable S.

Equations

• Hex.PolyQuot.Roots.candidateLift e = Hex.DensePoly.ofCoeffs (Array.map (fun (c : Int) => Hex.DensePoly.C (Hex.DensePoly.C c)) (Hex.DensePoly.toArray e))

def Hex.PolyQuot.Roots.evalShifted {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) : DensePoly (DensePoly ZPoly)

The trivariate polynomial S - G(y, z) with G = clearedOuter f, regarded as a polynomial in the candidate variable z whose coefficients are polynomials in the generator y over Int[S]. The evaluation variable S enters only the constant coordinate of the constant z-coefficient.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.Roots.evalEliminant {p : ZPoly} {x : SimpleRoot p} (f : DensePoly (PolyQuot p x)) (e : ZPoly) : ZPoly

Integer evaluation eliminant for one component and candidate eliminant: the double resultant Res_y(p(y), Res_z(e(z), S - G(y, z))) with G = clearedOuter f, dilated by the common denominator so that its roots are the candidate evaluations themselves rather than their denominator-cleared multiples. Zero-root removal and primitive normalization happen inside the bounded disambiguation search, per the SPEC.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.Roots.evalBall? {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (candidate : AlgebraicRoot) (prec : Nat) : Option DyadicComplexBall

Certified ball Horner evaluation at the selected fixed-field embedding and one absolute candidate root. Coefficient approximation retains its sound fallback; candidate refinement is checked because the bounded selector must observe the requested shrinking radius.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.Roots.componentRoots? {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (multiplicity : Nat) (hMultiplicity : 0 < multiplicity) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : Option (Array RootCount)

Isolate a component's norm roots and retain exactly the roots belonging to the selected embedding.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.Roots.sameValue? (a b : AlgebraicRoot) : Option Bool

Semantic equality of two lazy roots. Equal enclosing polynomials use the isolation comparison directly; distinct polynomials are first tested for a nonconstant gcd over Rat. Coprime polynomials cannot share a root, so only the remaining shared-factor case exactifies both roots.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.Roots.mergeRootList (candidate : RootCount) : List RootCount → Option (List RootCount)

Merge one root into a list, retaining the first representative of an existing semantic value and the incoming certified multiplicity.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PolyQuot.Roots.mergeRootList candidate [] = some [candidate]

def Hex.PolyQuot.Roots.mergeRoot (roots : Array RootCount) (candidate : RootCount) : Option (Array RootCount)

Merge one root using a complete scan of the current array.

Equations

• Hex.PolyQuot.Roots.mergeRoot roots candidate = do let merged ← Hex.PolyQuot.Roots.mergeRootList candidate roots.toList some merged.toArray

def Hex.PolyQuot.Roots.intListLe : List Int → List Int → Bool

Lexicographic non-strict order on integer coefficient lists.

Equations

• Hex.PolyQuot.Roots.intListLe [] x✝ = true
• Hex.PolyQuot.Roots.intListLe (head :: tail) [] = false
• Hex.PolyQuot.Roots.intListLe (a :: as) (b :: bs) = if a < b then true else if b < a then false else Hex.PolyQuot.Roots.intListLe as bs

def Hex.PolyQuot.Roots.rootLe (a b : RootCount) : Bool

Stable root order: enclosing polynomial coefficients, then isolation centre and precision.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.roots? {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : Option RootSet

Checked roots of a fixed-field polynomial. none is reserved for a certificate that did not appear within its prescribed finite bound.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PolyQuot.roots {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : RootSet

Total fixed-field root API. The loud .all fallback is unreachable once the companion discharges roots?_isSome.

Equations

• Hex.PolyQuot.roots f rep h = (Hex.PolyQuot.roots? f rep h).getD (Hex.panicWith Hex.RootSet.all "PolyQuot.roots: certification failed")

structure Hex.AlgebraicPoly.Common.Presentation : Type

A primitive fixed-field presentation of an algebraic coefficient array.

• generator : AlgebraicNumber

  The canonical primitive element of the common field.

• coefficients : Array (PolyQuot self.generator.p self.generator.x)

  The input coefficients rewritten in the generator's fixed field.

def Hex.AlgebraicPoly.Common.signedShift : Nat → Int

Deterministic signed shift order 0, 1, -1, 2, -2, ....

Equations

• Hex.AlgebraicPoly.Common.signedShift 0 = 0
• Hex.AlgebraicPoly.Common.signedShift fuel_1.succ = if fuel_1 % 2 = 0 then Int.ofNat (fuel_1 / 2 + 1) else -Int.ofNat (fuel_1 / 2 + 1)

def Hex.AlgebraicPoly.Common.rational? (q : Rat) : Option AlgebraicNumber

Checked canonical embedding of a rational number.

Equations

• One or more equations did not get rendered due to their size.

def Hex.AlgebraicPoly.Common.add? (a b : AlgebraicNumber) : Option AlgebraicNumber

Checked canonical sum.

Equations

• Hex.AlgebraicPoly.Common.add? a b = do let root ← a.toRoot.add? b.toRoot root.exact?

def Hex.AlgebraicPoly.Common.mul? (a b : AlgebraicNumber) : Option AlgebraicNumber

Checked canonical product.

Equations

• Hex.AlgebraicPoly.Common.mul? a b = do let root ← a.toRoot.mul? b.toRoot root.exact?

def Hex.AlgebraicPoly.Common.scale? (c : Int) (a : AlgebraicNumber) : Option AlgebraicNumber

Checked multiplication by an integer shift.

Equations

• Hex.AlgebraicPoly.Common.scale? c a = do let scalar ← Hex.AlgebraicPoly.Common.rational? ↑c Hex.AlgebraicPoly.Common.mul? scalar a

def Hex.AlgebraicPoly.Common.shift? (theta alpha : AlgebraicNumber) (c : Int) : Option AlgebraicNumber

One primitive-element shift candidate theta + c * alpha.

Equations

• Hex.AlgebraicPoly.Common.shift? theta alpha c = if c = 0 then some theta else do let scaled ← Hex.AlgebraicPoly.Common.scale? c alpha Hex.AlgebraicPoly.Common.add? theta scaled

def Hex.AlgebraicPoly.Common.degree (a : AlgebraicNumber) : Nat

Degree of a canonical algebraic number.

Equations

• Hex.AlgebraicPoly.Common.degree a = Hex.DensePoly.natDegree a.p

structure Hex.AlgebraicPoly.Common.ShiftCandidate : Type

A primitive-search candidate together with the signed shift that produced it.

• shift : Int

  The signed integer shift that produced this candidate.

• value : AlgebraicNumber

  The candidate primitive element theta + shift * alpha.

def Hex.AlgebraicPoly.Common.extendShiftStep (theta alpha : AlgebraicNumber) : Option ShiftCandidate → Nat → Option (Option ShiftCandidate)

One maximum-degree update that retains the producing signed shift.

Equations

• One or more equations did not get rendered due to their size.

def Hex.AlgebraicPoly.Common.extendShift? (theta alpha : AlgebraicNumber) : Option ShiftCandidate

Maximum-degree primitive candidate together with its producing shift.

Equations

• One or more equations did not get rendered due to their size.

def Hex.AlgebraicPoly.Common.extend? (theta alpha : AlgebraicNumber) : Option AlgebraicNumber

Extend a primitive presentation by one algebraic number. Testing choose(deg(theta) * deg(alpha), 2) + 1 shifts is a conservative bounded primitive-element search. The maximum-degree candidate generates the compositum even when the two fields overlap.

Equations

• Hex.AlgebraicPoly.Common.extend? theta alpha = Option.map Hex.AlgebraicPoly.Common.ShiftCandidate.value (Hex.AlgebraicPoly.Common.extendShift? theta alpha)

def Hex.AlgebraicPoly.Common.primitive? (coefficients : Array AlgebraicNumber) : Option AlgebraicNumber

Bounded primitive element for all nonzero coefficients.

Equations

• One or more equations did not get rendered due to their size.

def Hex.AlgebraicPoly.Common.powers? (gamma : AlgebraicNumber) (last : Nat) : Option (Array AlgebraicNumber)

Checked canonical powers 1, gamma, ..., gamma^last.

Equations

• One or more equations did not get rendered due to their size.

def Hex.AlgebraicPoly.Common.trace? (ambient : Nat) (a : AlgebraicNumber) : Option Rat

Field trace of a from a known ambient field degree. If m is the minimal-polynomial degree of a, this is (ambient / m) times the sum of its m conjugates.

Equations

• One or more equations did not get rendered due to their size.

def Hex.AlgebraicPoly.Common.coordinates? (gamma a : AlgebraicNumber) (powers : Array AlgebraicNumber) : Option (PolyQuot gamma.p gamma.x)

Recover one coefficient in the power basis of gamma through the nondegenerate trace pairing, then validate the recovered coordinate by canonical algebraic equality.

Equations

• One or more equations did not get rendered due to their size.

def Hex.AlgebraicPoly.Common.presentation? (coefficients : Array AlgebraicNumber) : Option Presentation

Construct and validate one primitive fixed-field presentation for an algebraic coefficient array.

Equations

• One or more equations did not get rendered due to their size.

def Hex.AlgebraicNumber.ofRat (q : Rat) : AlgebraicNumber

Total executable embedding of a rational number into canonical algebraic numbers. The companion proves that the checked constructor cannot fail.

Equations

• Hex.AlgebraicNumber.ofRat q = (Hex.AlgebraicPoly.Common.rational? q).getD (Hex.panicWith 0 "AlgebraicNumber.ofRat: certification failed")

@[instance_reducible]

instance Hex.AlgebraicNumber.instOne : One AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instOne = { one := Hex.AlgebraicNumber.ofRat 1 }

@[instance_reducible]

instance Hex.AlgebraicNumber.instNatCast : NatCast AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instNatCast = { natCast := fun (n : Nat) => Hex.AlgebraicNumber.ofRat ↑n }

@[instance_reducible]

instance Hex.AlgebraicNumber.instIntCast : IntCast AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instIntCast = { intCast := fun (n : Int) => Hex.AlgebraicNumber.ofRat ↑n }

@[instance_reducible, instance 90]

instance Hex.AlgebraicNumber.instOfNatHAddNatOfNat (n : Nat) : OfNat AlgebraicNumber (n + 2)

Equations

• Hex.AlgebraicNumber.instOfNatHAddNatOfNat n = { ofNat := Hex.AlgebraicNumber.ofRat ↑(n + 2) }

def Hex.AlgebraicNumber.smul (q : Rat) (a : AlgebraicNumber) : AlgebraicNumber

Executable scalar multiplication through the canonical rational embedding.

Equations

• Hex.AlgebraicNumber.smul q a = Hex.AlgebraicNumber.ofRat q * a

@[instance_reducible]

instance Hex.AlgebraicNumber.instSMulRat : SMul Rat AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instSMulRat = { smul := Hex.AlgebraicNumber.smul }

@[instance_reducible]

instance Hex.AlgebraicNumber.instSMulNat : SMul Nat AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instSMulNat = { smul := fun (n : Nat) (a : Hex.AlgebraicNumber) => Hex.AlgebraicNumber.smul (↑n) a }

@[instance_reducible]

instance Hex.AlgebraicNumber.instSMulInt : SMul Int AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instSMulInt = { smul := fun (n : Int) (a : Hex.AlgebraicNumber) => Hex.AlgebraicNumber.smul (↑n) a }

@[irreducible]

def Hex.AlgebraicNumber.natPow (a : AlgebraicNumber) : Nat → AlgebraicNumber

Natural powers by repeated squaring using executable canonical multiplication.

Equations

• a.natPow 0 = 1
• a.natPow fuel_1.succ = if (fuel_1 + 1) % 2 = 0 then a.natPow ((fuel_1 + 1) / 2) * a.natPow ((fuel_1 + 1) / 2) else a.natPow ((fuel_1 + 1) / 2) * a.natPow ((fuel_1 + 1) / 2) * a

@[instance_reducible]

instance Hex.AlgebraicNumber.instPowNat : Pow AlgebraicNumber Nat

Equations

• Hex.AlgebraicNumber.instPowNat = { pow := Hex.AlgebraicNumber.natPow }

def Hex.AlgebraicNumber.intPow (a : AlgebraicNumber) : Int → AlgebraicNumber

Integer powers assembled from executable multiplication and inversion.

Equations

• a.intPow (Int.ofNat n) = a.natPow n
• a.intPow (Int.negSucc n) = (a.natPow (n + 1))⁻¹

@[instance_reducible]

instance Hex.AlgebraicNumber.instPowInt : Pow AlgebraicNumber Int

Equations

• Hex.AlgebraicNumber.instPowInt = { pow := Hex.AlgebraicNumber.intPow }

def Hex.AlgebraicPoly.roots? (f : AlgebraicPoly) : Option RootSet

Checked roots of a polynomial with canonical algebraic coefficients. All nonzero coefficients are first embedded in one bounded deterministic primitive presentation, then the fixed-field root driver is reused.

Equations

• One or more equations did not get rendered due to their size.

def Hex.AlgebraicPoly.roots (f : AlgebraicPoly) : RootSet

Total roots of a polynomial with canonical algebraic coefficients.

Equations

• f.roots = f.roots?.getD (Hex.panicWith Hex.RootSet.all "AlgebraicPoly.roots: certification failed")