def Hex.ZPoly.liftOuter (p : ZPoly) : DensePoly ZPoly

Regard an integer polynomial in y as a polynomial in y whose coefficients are constant polynomials in a second variable t.

Equations

• p.liftOuter = Hex.DensePoly.ofCoeffs (Array.map Hex.DensePoly.C (Hex.DensePoly.toArray p))

@[simp]

theorem Hex.ZPoly.coeff_liftOuter (p : ZPoly) (n : Nat) : p.liftOuter.coeff n = DensePoly.C (DensePoly.coeff p n)

Coefficients of the outer lift are the corresponding constant polynomials.

def Hex.ZPoly.addEliminant (p q : ZPoly) : ZPoly

The eliminant whose roots are pairwise sums of roots of p and q.

Equations

• p.addEliminant q = p.liftOuter.resultant (q.liftOuter.compose (Hex.DensePoly.C Hex.ZPoly.X - Hex.DensePoly.monomial 1 1))

def Hex.ZPoly.mulSubstitute (q : ZPoly) : DensePoly ZPoly

The polynomial y^degree(q) q(t/y), viewed as a polynomial in y with coefficients in Int[t].

Equations

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

def Hex.ZPoly.mulEliminant (p q : ZPoly) : ZPoly

The eliminant whose roots are pairwise products of roots of p and q.

Equations

• p.mulEliminant q = p.liftOuter.resultant q.mulSubstitute

def Hex.ZPoly.removeX (p : ZPoly) : ZPoly

Remove the largest power of X dividing an integer polynomial.

Equations

• p.removeX = Hex.DensePoly.ofCoeffs (Array.popWhile (fun (x : Int) => x == 0) (Hex.DensePoly.toArray p).reverse).reverse

def Hex.ZPoly.reciprocal (p : ZPoly) : ZPoly

Reverse coefficients, automatically trimming the degree drop caused by an original zero constant coefficient.

Equations

• p.reciprocal = Hex.DensePoly.ofCoeffs (Hex.DensePoly.toArray p).reverse

theorem Hex.ZPoly.negRoots_primitive (p : ZPoly) (h : p.Primitive) : p.negRoots.Primitive

Negating roots preserves primitive normalization.

theorem Hex.ZPoly.negRoots_lc_pos (p : ZPoly) (hprim : p.Primitive) (h : 0 < DensePoly.leadingCoeff p) : 0 < DensePoly.leadingCoeff p.negRoots

Negating roots preserves positive leading normalization.

theorem Hex.ZPoly.negRoots_degree_pos (p : ZPoly) (hprim : p.Primitive) (h : 0 < DensePoly.natDegree p) : 0 < DensePoly.natDegree p.negRoots

Negating roots preserves positive degree.

theorem Hex.ZPoly.negRoots_simple (p : ZPoly) (hprim : p.Primitive) (h : HasOnlySimpleRoots p) : HasOnlySimpleRoots p.negRoots

Negating roots preserves squarefreeness.

theorem Hex.ZPoly.mahlerPrec_negRoots (p : ZPoly) (h : p.Primitive) : mahlerPrec p.negRoots = mahlerPrec p

The Mahler precision is invariant under reflection and unit normalization.

def Hex.DyadicComplexBall.neg (b : DyadicComplexBall) : DyadicComplexBall

Reflection of a complex ball.

Equations

• b.neg = { re := -b.re, im := -b.im, radius := b.radius }

def Hex.DyadicComplexBall.sub (a b : DyadicComplexBall) : DyadicComplexBall

Minkowski difference of complex balls.

Equations

• a.sub b = a.add b.neg

def Hex.DyadicComplexBall.inv? (b : DyadicComplexBall) (prec : Int) : Option DyadicComplexBall

Checked reciprocal enclosure. The centre reciprocal is rounded downward coordinatewise; three ulps cover both coordinate errors and the downward rounding of the radial distortion bound.

Equations

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

def Hex.RefinedIsolation.neg {p : ZPoly} (r : RefinedIsolation p) (hprim : p.Primitive) : RefinedIsolation p.negRoots

Reflect a refined isolation while preserving its root certificate and separation precision.

Equations

• r.neg hprim = ⟨{ square := r.val.square.neg, witness := Hex.AtomCertificate.neg hprim r.val.witness }, ⋯⟩

def Hex.AlgebraicRoot.ofEliminant? (raw : ZPoly) (ballAt : Int → Option DyadicComplexBall) : Option AlgebraicRoot

Normalize an eliminant, isolate all of its distinct roots, and retain the root meeting the supplied certified operation ball.

Equations

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

def Hex.AlgebraicRoot.neg (a : AlgebraicRoot) : AlgebraicRoot

Certificate-free negation by reflection.

Equations

• a.neg = { p := a.p.negRoots, prim := ⋯, pos_lc := ⋯, pos_degree := ⋯, squarefree := ⋯, x := Hex.SimpleRoot.mk (a.rep.neg ⋯), rep := a.rep.neg ⋯, rep_mk := ⋯ }

def Hex.AlgebraicRoot.add? (a b : AlgebraicRoot) : Option AlgebraicRoot

Checked lazy sum through the addition eliminant.

Equations

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

def Hex.AlgebraicRoot.add (a b : AlgebraicRoot) : AlgebraicRoot

Total lazy sum.

Equations

• a.add b = (a.add? b).getD (Hex.panicWith Hex.AlgebraicNumber.zero.toRoot "AlgebraicRoot.add: certification failed")

def Hex.AlgebraicRoot.sub? (a b : AlgebraicRoot) : Option AlgebraicRoot

Checked lazy difference.

Equations

• a.sub? b = a.add? b.neg

def Hex.AlgebraicRoot.sub (a b : AlgebraicRoot) : AlgebraicRoot

Total lazy difference.

Equations

• a.sub b = (a.sub? b).getD (Hex.panicWith Hex.AlgebraicNumber.zero.toRoot "AlgebraicRoot.sub: certification failed")

def Hex.AlgebraicRoot.mulGuardBits (a b : AlgebraicRoot) : Nat

Guard bits for multiplication-ball amplification.

Equations

• a.mulGuardBits b = 8 + Hex.PolyQuot.rootBits a.rep.val.square + Hex.PolyQuot.rootBits b.rep.val.square

def Hex.AlgebraicRoot.invGuardBits (a : AlgebraicRoot) : Nat

Guard bits for reciprocal-ball amplification. For a nonzero root of the primitive integer polynomial p, reciprocal Cauchy gives |a| ≥ 1 / (1 + coeffAbsMax p). Doubling the bit bound pays for the |a|⁻² distortion in inversion; sixteen further bits cover the strict nonzero guard and dyadic rounding.

Equations

• a.invGuardBits = 2 * Hex.ceilLog2 (a.p.coeffAbsMax + 1) + 16

def Hex.AlgebraicRoot.mul? (a b : AlgebraicRoot) : Option AlgebraicRoot

Checked lazy product through the product eliminant.

Equations

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

def Hex.AlgebraicRoot.mul (a b : AlgebraicRoot) : AlgebraicRoot

Total lazy product.

Equations

• a.mul b = (a.mul? b).getD (Hex.panicWith Hex.AlgebraicNumber.zero.toRoot "AlgebraicRoot.mul: certification failed")

def Hex.AlgebraicRoot.inv? (a : AlgebraicRoot) : Option AlgebraicRoot

Checked lazy inverse through coefficient reversal.

Equations

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

def Hex.AlgebraicRoot.inv (a : AlgebraicRoot) : AlgebraicRoot

Total lazy inverse, with inv 0 = 0.

Equations

• a.inv = a.inv?.getD (Hex.panicWith Hex.AlgebraicNumber.zero.toRoot "AlgebraicRoot.inv: certification failed")

def Hex.AlgebraicRoot.div? (a b : AlgebraicRoot) : Option AlgebraicRoot

Checked lazy quotient.

Equations

• a.div? b = do let bInv ← b.inv? a.mul? bInv

def Hex.AlgebraicRoot.div (a b : AlgebraicRoot) : AlgebraicRoot

Total lazy quotient.

Equations

• a.div b = (a.div? b).getD (Hex.panicWith Hex.AlgebraicNumber.zero.toRoot "AlgebraicRoot.div: certification failed")

def Hex.AlgebraicNumber.add (a b : AlgebraicNumber) : AlgebraicNumber

Canonical sum: perform the lazy operation, then exactify.

Equations

• a.add b = (a.toRoot.add b.toRoot).exact

def Hex.AlgebraicNumber.sub (a b : AlgebraicNumber) : AlgebraicNumber

Canonical difference: perform the lazy operation, then exactify.

Equations

• a.sub b = (a.toRoot.sub b.toRoot).exact

def Hex.AlgebraicNumber.mul (a b : AlgebraicNumber) : AlgebraicNumber

Canonical product: perform the lazy operation, then exactify.

Equations

• a.mul b = (a.toRoot.mul b.toRoot).exact

def Hex.AlgebraicNumber.neg (a : AlgebraicNumber) : AlgebraicNumber

Canonical negation: reflect the lazy root, then exactify.

Equations

• a.neg = a.toRoot.neg.exact

def Hex.AlgebraicNumber.inv (a : AlgebraicNumber) : AlgebraicNumber

Canonical inverse, with inv 0 = 0: perform the lazy operation, then exactify.

Equations

• a.inv = a.toRoot.inv.exact

def Hex.AlgebraicNumber.div (a b : AlgebraicNumber) : AlgebraicNumber

Canonical quotient: perform the lazy operation, then exactify.

Equations

• a.div b = (a.toRoot.div b.toRoot).exact

@[instance_reducible]

instance Hex.AlgebraicNumber.instAdd : Add AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instAdd = { add := Hex.AlgebraicNumber.add }

@[instance_reducible]

instance Hex.AlgebraicNumber.instSub : Sub AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instSub = { sub := Hex.AlgebraicNumber.sub }

@[instance_reducible]

instance Hex.AlgebraicNumber.instMul : Mul AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instMul = { mul := Hex.AlgebraicNumber.mul }

@[instance_reducible]

instance Hex.AlgebraicNumber.instNeg : Neg AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instNeg = { neg := Hex.AlgebraicNumber.neg }

@[instance_reducible]

instance Hex.AlgebraicNumber.instInv : Inv AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instInv = { inv := Hex.AlgebraicNumber.inv }

@[instance_reducible]

instance Hex.AlgebraicNumber.instDiv : Div AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instDiv = { div := Hex.AlgebraicNumber.div }