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.isolateAt? (p : ZPoly) (ball : DyadicComplexBall) (prec : Int) : Option (RefinedIsolation p)

Certify the enclosed root using a rounded centre and checked containment. Linear polynomials retain global isolation and canonical parent reuse. Failure leaves the global isolation route available.

Equations

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

def Hex.AlgebraicRoot.withEliminant? {α : Type} (raw : ZPoly) (ballAt : Int → Option DyadicComplexBall) (finish : (a : AlgebraicRoot) → (isolations : Array (DyadicRootIsolation a.p)) → (refined : Array (RefinedIsolation a.p)) → a.p.isolateComplexRoots? ⋯ ↑(separationDepth a.p) = some isolations → Array.mapM DyadicRootIsolation.toRefined? isolations = some refined → Option α) (localFinish : AlgebraicRoot → Option α) : Option α

Select the enclosed root directly when possible. Otherwise run the consumer while the global producer's certified isolations are available. Callers prove the consumers agree using withEliminant?_eq.

Equations

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

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

Normalize an eliminant and certify the root enclosed by the supplied operation ball. If direct certification fails, isolate all distinct roots and retain the unique root meeting that ball.

Equations

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

theorem Hex.AlgebraicRoot.ofEliminant?_eq (raw : ZPoly) (ballAt : Int → Option DyadicComplexBall) : ofEliminant? raw ballAt = have p := raw.squareFreeCore; if hprim : p.content = 1 then if hpos : 0 < DensePoly.leadingCoeff p then if hdegree : 0 < DensePoly.natDegree p then if hsimple : HasOnlySimpleRoots p then have prec := ↑(separationDepth p); do let ball ← ballAt prec match isolateAt? p ball prec with | some matching => some { p := p, prim := hprim, pos_lc := hpos, pos_degree := hdegree, squarefree := hsimple, x := SimpleRoot.mk matching, rep := matching, rep_mk := ⋯ } | none => do let isolations ← p.isolateComplexRoots? hsimple prec let refined ← Array.mapM DyadicRootIsolation.toRefined? isolations match List.filter (fun (r : RefinedIsolation p) => r.val.square.meetsBall ball) refined.toList with | [matching] => some { p := p, prim := hprim, pos_lc := hpos, pos_degree := hdegree, squarefree := hsimple, x := SimpleRoot.mk matching, rep := matching, rep_mk := ⋯ } | x => none else none else none else none else none

Expose direct selection and its global fallback without consumer callbacks.

theorem Hex.AlgebraicRoot.withEliminant?_eq {α : Type} (raw : ZPoly) (ballAt : Int → Option DyadicComplexBall) (finish : (a : AlgebraicRoot) → (isolations : Array (DyadicRootIsolation a.p)) → (refined : Array (RefinedIsolation a.p)) → a.p.isolateComplexRoots? ⋯ ↑(separationDepth a.p) = some isolations → Array.mapM DyadicRootIsolation.toRefined? isolations = some refined → Option α) (f : AlgebraicRoot → Option α) (hfinish : ∀ (a : AlgebraicRoot) (isolations : Array (DyadicRootIsolation a.p)) (refined : Array (RefinedIsolation a.p)) (hisolate : a.p.isolateComplexRoots? ⋯ ↑(separationDepth a.p) = some isolations) (hrefine : Array.mapM DyadicRootIsolation.toRefined? isolations = some refined), finish a isolations refined hisolate hrefine = f a) : withEliminant? raw ballAt finish f = (ofEliminant? raw ballAt).bind f

A consumer using the certified producer run returns exactly the result of selecting the lazy root first and then applying its ordinary consumer.

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

Canonicalize a selected eliminant root, reusing its producer run for a factor equal to the whole enclosing polynomial.

Equations

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

theorem Hex.AlgebraicRoot.exactEliminant?_eq (raw : ZPoly) (ballAt : Int → Option DyadicComplexBall) : exactEliminant? raw ballAt = (ofEliminant? raw ballAt).bind exact?

Fusing selection and exactification preserves the complete checked result.

def Hex.AlgebraicRoot.exactEliminant (raw : ZPoly) (ballAt : Int → Option DyadicComplexBall) (fallback : Unit → AlgebraicRoot) : AlgebraicNumber

Total canonical consumption of an eliminant, retaining the original lazy-operation fallback and exactification fallback separately. The producer fallback is thunked so successful selection never evaluates its panic branch.

Equations

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

theorem Hex.AlgebraicRoot.exactEliminant_eq (raw : ZPoly) (ballAt : Int → Option DyadicComplexBall) (fallback : Unit → AlgebraicRoot) : exactEliminant raw ballAt fallback = ((ofEliminant? raw ballAt).getD (fallback ())).exact

Reuse preserves the total pipeline and both original fallback branches.

def Hex.AlgebraicRoot.addBall? (a b : AlgebraicRoot) (prec : Int) : Option DyadicComplexBall

Certified operation ball shared by lazy and canonical addition.

Equations

• a.addBall? b prec = do let ar ← a.rep.refineTo? (prec + 4) let br ← b.rep.refineTo? (prec + 4) some (ar.val.val.square.toBall.add br.val.val.square.toBall)

def Hex.AlgebraicRoot.exactAdd? (a b : AlgebraicRoot) : Option AlgebraicNumber

Checked canonical sum, consuming the producer's isolation before its transient certificates go out of scope.

Equations

• a.exactAdd? b = Hex.AlgebraicRoot.exactEliminant? (a.p.addEliminant b.p) (a.addBall? b)

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

• a.add? b = Hex.AlgebraicRoot.ofEliminant? (a.p.addEliminant b.p) (a.addBall? b)

theorem Hex.AlgebraicRoot.exactAdd?_eq (a b : AlgebraicRoot) : a.exactAdd? b = (a.add? b).bind exact?

Fused canonical addition preserves the original lazy-then-exact pipeline.

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.mulBall? (a b : AlgebraicRoot) (prec : Int) : Option DyadicComplexBall

Certified operation ball shared by lazy and canonical multiplication.

Equations

• a.mulBall? b prec = do let ar ← a.rep.refineTo? (prec + ↑(a.mulGuardBits b)) let br ← b.rep.refineTo? (prec + ↑(a.mulGuardBits b)) some (ar.val.val.square.toBall.mul br.val.val.square.toBall)

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

Checked lazy product through the product eliminant.

Equations

• a.mul? b = if (a.isZero || b.isZero) = true then some Hex.AlgebraicNumber.zero.toRoot else have raw := (a.p.mulEliminant b.p).removeX; Hex.AlgebraicRoot.ofEliminant? raw (a.mulBall? b)

def Hex.AlgebraicRoot.exactMul? (a b : AlgebraicRoot) : Option AlgebraicNumber

Checked canonical product reusing its eliminant producer's isolation.

Equations

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

theorem Hex.AlgebraicRoot.exactMul?_eq (a b : AlgebraicRoot) : a.exactMul? b = (a.mul? b).bind exact?

Fused canonical multiplication preserves zeros, representatives and failures.

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, reusing the producer's isolation when the chosen factor is the whole eliminant.

Equations

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

theorem Hex.AlgebraicNumber.add_eq (a b : AlgebraicNumber) : a.add b = (a.toRoot.add b.toRoot).exact

Canonical addition keeps the exact result of lazy addition followed by exactification.

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, reusing the producer's isolation when the chosen factor is the whole eliminant.

Equations

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

theorem Hex.AlgebraicNumber.mul_eq (a b : AlgebraicNumber) : a.mul b = (a.toRoot.mul b.toRoot).exact

Canonical multiplication keeps the exact old result, including its zero case.

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 }