@[implicit_reducible]

def Hex.instCommRingZPoly_hexNumberFieldMathlib : CommRing ZPoly

Proof-local Mathlib CommRing view of ZPoly, assembled from the executable library's verified Lean.Grind.CommRing instance.

Equations

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

theorem Hex.instIsDomainZPoly_hexNumberFieldMathlib : IsDomain ZPoly

Proof-local domain structure on ZPoly, transported from Polynomial Int.

theorem Hex.ZPoly.map_liftOuterAt (p : ZPoly) (t : ℂ) : Polynomial.map ((Polynomial.eval₂RingHom (Int.castRingHom ℂ) t).comp HexPolyMathlib.equiv.toRingHom) (HexPolyMathlib.toPolynomial p.liftOuter) = HexRootsMathlib.toPolyℂ p

Specialization of the coefficient variable commutes with the constant bivariate lift.

theorem Hex.ZPoly.eval_liftOuter (p : ZPoly) (t y : ℂ) : Polynomial.eval y (Polynomial.map ((Polynomial.eval₂RingHom (Int.castRingHom ℂ) t).comp HexPolyMathlib.equiv.toRingHom) (HexPolyMathlib.toPolynomial p.liftOuter)) = Polynomial.eval y (HexRootsMathlib.toPolyℂ p)

Specializing the coefficient variable of the constant bivariate lift recovers the original complex polynomial.

theorem Hex.ZPoly.natDegree_liftOuter (p : ZPoly) : (HexPolyMathlib.toPolynomial p.liftOuter).natDegree = DensePoly.natDegree p

The constant bivariate lift preserves the degree of the source integer polynomial.

theorem Hex.ZPoly.removeX_ne_zero {p : ZPoly} (hp : p ≠ 0) : p.removeX ≠ 0

Removing the maximal power of X preserves nonzeroness.

theorem Hex.ZPoly.removeX_isRoot {p : ZPoly} {z : ℂ} (hz : z ≠ 0) (hroot : (HexRootsMathlib.toPolyℂ p).IsRoot z) : (HexRootsMathlib.toPolyℂ p.removeX).IsRoot z

Removing the maximal power of X preserves every nonzero complex root.

theorem Hex.ZPoly.root_norm_lower {p : ZPoly} {z : ℂ} (hp : p ≠ 0) (hz : z ≠ 0) (hroot : (HexRootsMathlib.toPolyℂ p).IsRoot z) : (↑(p.coeffAbsMax + 1))⁻¹ < ‖z‖

A nonzero complex root of a nonzero integer polynomial is bounded away from zero by the reciprocal Cauchy bound of its coefficient height.

theorem Hex.resultant_isRoot (f g : DensePoly ZPoly) (t y : ℂ) (hpos : 1 < f.size ∨ 1 < g.size) (hf : Polynomial.eval y (Polynomial.map ((Polynomial.eval₂RingHom (Int.castRingHom ℂ) t).comp HexPolyMathlib.equiv.toRingHom) (HexPolyMathlib.toPolynomial f)) = 0) (hg : Polynomial.eval y (Polynomial.map ((Polynomial.eval₂RingHom (Int.castRingHom ℂ) t).comp HexPolyMathlib.equiv.toRingHom) (HexPolyMathlib.toPolynomial g)) = 0) : Polynomial.eval t (HexRootsMathlib.toPolyℂ (f.resultant g)) = 0

A common complex root after specializing the coefficient variable is a root of the executable bivariate resultant.

theorem Hex.AlgebraicRoot.ofEliminant?_sound (raw : ZPoly) (ballAt : ℤ → Option DyadicComplexBall) {c : AlgebraicRoot} {z : ℂ} (h : ofEliminant? raw ballAt = some c) (hroot : (HexRootsMathlib.toPolyℂ raw).IsRoot z) (hball : ∀ (ball : DyadicComplexBall), ballAt ↑(separationDepth raw.squareFreeCore) = some ball → z ∈ ball.set) : c.toComplex = z

A successful eliminant search selects the supplied semantic root whenever the operation ball contains it.

theorem Hex.AlgebraicRoot.ofEliminant?_isSome (raw : ZPoly) (ballAt : ℤ → Option DyadicComplexBall) {z : ℂ} (hraw : raw ≠ 0) (hroot : (HexRootsMathlib.toPolyℂ raw).IsRoot z) (ball : DyadicComplexBall) (hballAt : ballAt ↑(separationDepth raw.squareFreeCore) = some ball) (hzball : z ∈ ball.set) (hballRadius : ball.realRadius ≤ 2 ^ (-↑(mahlerPrec raw.squareFreeCore))) : (ofEliminant? raw ballAt).isSome = true

A nonzero eliminant root enclosed by a sufficiently small operation ball survives normalization, isolation, and the singleton selection filter.

theorem Hex.AlgebraicRoot.neg_toComplex (a : AlgebraicRoot) : a.neg.toComplex = -a.toComplex

Reflection computes complex negation.

theorem Hex.AlgebraicRoot.add?_sound (a b : AlgebraicRoot) {c : AlgebraicRoot} (h : a.add? b = some c) : c.toComplex = a.toComplex + b.toComplex

A certified lazy sum denotes the sum of its inputs.

theorem Hex.AlgebraicRoot.add?_isSome (a b : AlgebraicRoot) : (a.add? b).isSome = true

The bounded lazy addition search always finds its certificate.

theorem Hex.AlgebraicRoot.add_toComplex (a b : AlgebraicRoot) : (a.add b).toComplex = a.toComplex + b.toComplex

Total lazy addition computes complex addition.

theorem Hex.AlgebraicRoot.sub?_sound (a b : AlgebraicRoot) {c : AlgebraicRoot} (h : a.sub? b = some c) : c.toComplex = a.toComplex - b.toComplex

A certified lazy difference denotes the difference of its inputs.

theorem Hex.AlgebraicRoot.sub?_isSome (a b : AlgebraicRoot) : (a.sub? b).isSome = true

The bounded lazy subtraction search always finds its certificate.

theorem Hex.AlgebraicRoot.sub_toComplex (a b : AlgebraicRoot) : (a.sub b).toComplex = a.toComplex - b.toComplex

Total lazy subtraction computes complex subtraction.

theorem Hex.AlgebraicRoot.mul?_sound (a b : AlgebraicRoot) {c : AlgebraicRoot} (h : a.mul? b = some c) : c.toComplex = a.toComplex * b.toComplex

A certified lazy product denotes the product of its inputs.

theorem Hex.AlgebraicRoot.mul?_isSome (a b : AlgebraicRoot) : (a.mul? b).isSome = true

The bounded lazy multiplication search always finds its certificate.

theorem Hex.AlgebraicRoot.mul_toComplex (a b : AlgebraicRoot) : (a.mul b).toComplex = a.toComplex * b.toComplex

Total lazy multiplication computes complex multiplication.

theorem Hex.AlgebraicRoot.inv?_sound (a : AlgebraicRoot) {b : AlgebraicRoot} (h : a.inv? = some b) : b.toComplex = a.toComplex⁻¹

A certified lazy inverse denotes the reciprocal of its input, including the executable convention 0⁻¹ = 0.

theorem Hex.AlgebraicRoot.inv?_isSome (a : AlgebraicRoot) : a.inv?.isSome = true

The bounded lazy inverse search always finds its certificate.

theorem Hex.AlgebraicRoot.inv_toComplex (a : AlgebraicRoot) : a.inv.toComplex = a.toComplex⁻¹

Total lazy inversion computes complex inversion.

theorem Hex.AlgebraicRoot.div?_sound (a b : AlgebraicRoot) {c : AlgebraicRoot} (h : a.div? b = some c) : c.toComplex = a.toComplex / b.toComplex

A certified lazy quotient denotes the quotient of its inputs.

theorem Hex.AlgebraicRoot.div?_isSome (a b : AlgebraicRoot) : (a.div? b).isSome = true

The bounded lazy division search always finds its certificate.

theorem Hex.AlgebraicRoot.div_toComplex (a b : AlgebraicRoot) : (a.div b).toComplex = a.toComplex / b.toComplex

Total lazy division computes complex division.

theorem Hex.AlgebraicNumber.add_toComplex (a b : AlgebraicNumber) : (a + b).toComplex = a.toComplex + b.toComplex

Canonical addition computes complex addition.

theorem Hex.AlgebraicNumber.sub_toComplex (a b : AlgebraicNumber) : (a - b).toComplex = a.toComplex - b.toComplex

Canonical subtraction computes complex subtraction.

theorem Hex.AlgebraicNumber.mul_toComplex (a b : AlgebraicNumber) : (a * b).toComplex = a.toComplex * b.toComplex

Canonical multiplication computes complex multiplication.

theorem Hex.AlgebraicNumber.neg_toComplex (a : AlgebraicNumber) : (-a).toComplex = -a.toComplex

Canonical negation computes complex negation.

theorem Hex.AlgebraicNumber.inv_toComplex (a : AlgebraicNumber) : a⁻¹.toComplex = a.toComplex⁻¹

Canonical inversion computes complex inversion.

theorem Hex.AlgebraicNumber.div_toComplex (a b : AlgebraicNumber) : (a / b).toComplex = a.toComplex / b.toComplex

Canonical division computes complex division.