def Hex.PolyQuot.reduceCoeffs (p : ZPoly) (f : DensePoly Rat) : DensePoly Rat

Canonical rational-polynomial remainder modulo p.

Equations

• Hex.PolyQuot.reduceCoeffs p f = f % p.toRatPoly

def Hex.PolyQuot.reduce (p : ZPoly) (x : SimpleRoot p) (f : DensePoly Rat) : PolyQuot p x

Package a rational polynomial after canonical modular reduction.

Equations

• Hex.PolyQuot.reduce p x f = { coeffs := Hex.PolyQuot.reduceCoeffs p f, degree_lt := ⋯ }

theorem Hex.PolyQuot.ext {p : ZPoly} {x : SimpleRoot p} {a b : PolyQuot p x} (h : a.coeffs = b.coeffs) : a = b

Fixed-presentation elements are equal when their canonical coordinates are equal.

theorem Hex.PolyQuot.ext_iff {p : ZPoly} {x : SimpleRoot p} {a b : PolyQuot p x} : a = b ↔ a.coeffs = b.coeffs

Equality is exactly equality of canonical coordinate polynomials; the generated iff form of Hex.PolyQuot.ext.

theorem Hex.PolyQuot.eq_iff_coeffs {p : ZPoly} {x : SimpleRoot p} {a b : PolyQuot p x} : a = b ↔ a.coeffs = b.coeffs

Equality is exactly equality of canonical coordinate polynomials.

@[instance_reducible]

instance Hex.PolyQuot.instDecidableEq {p : ZPoly} {x : SimpleRoot p} : DecidableEq (PolyQuot p x)

Equations

• a.instDecidableEq b = if h : a.coeffs = b.coeffs then isTrue ⋯ else isFalse ⋯

def Hex.PolyQuot.isZero {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) : Bool

Boolean zero test on canonical coordinates.

Equations

• a.isZero = a.coeffs.isZero

@[instance_reducible]

instance Hex.PolyQuot.instZero {p : ZPoly} {x : SimpleRoot p} : Zero (PolyQuot p x)

Equations

• Hex.PolyQuot.instZero = { zero := { coeffs := 0, degree_lt := ⋯ } }

@[instance_reducible]

instance Hex.PolyQuot.instOne {p : ZPoly} {x : SimpleRoot p} : One (PolyQuot p x)

Equations

• Hex.PolyQuot.instOne = { one := { coeffs := 1, degree_lt := ⋯ } }

def Hex.PolyQuot.add {p : ZPoly} {x : SimpleRoot p} (a b : PolyQuot p x) : PolyQuot p x

Reduced coordinate addition.

Equations

• a.add b = Hex.PolyQuot.reduce p x (a.coeffs + b.coeffs)

@[instance_reducible]

instance Hex.PolyQuot.instAdd {p : ZPoly} {x : SimpleRoot p} : Add (PolyQuot p x)

Equations

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

def Hex.PolyQuot.sub {p : ZPoly} {x : SimpleRoot p} (a b : PolyQuot p x) : PolyQuot p x

Reduced coordinate subtraction.

Equations

• a.sub b = Hex.PolyQuot.reduce p x (a.coeffs - b.coeffs)

@[instance_reducible]

instance Hex.PolyQuot.instSub {p : ZPoly} {x : SimpleRoot p} : Sub (PolyQuot p x)

Equations

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

def Hex.PolyQuot.neg {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) : PolyQuot p x

Reduced coordinate negation.

Equations

• a.neg = Hex.PolyQuot.reduce p x (-a.coeffs)

@[instance_reducible]

instance Hex.PolyQuot.instNeg {p : ZPoly} {x : SimpleRoot p} : Neg (PolyQuot p x)

Equations

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

def Hex.PolyQuot.mul {p : ZPoly} {x : SimpleRoot p} (a b : PolyQuot p x) : PolyQuot p x

Reduced coordinate multiplication.

Equations

• a.mul b = Hex.PolyQuot.reduce p x (a.coeffs * b.coeffs)

@[instance_reducible]

instance Hex.PolyQuot.instMul {p : ZPoly} {x : SimpleRoot p} : Mul (PolyQuot p x)

Equations

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

def Hex.PolyQuot.smul {p : ZPoly} {x : SimpleRoot p} (c : Rat) (a : PolyQuot p x) : PolyQuot p x

Rational scalar action followed by canonical reduction.

Equations

• Hex.PolyQuot.smul c a = Hex.PolyQuot.reduce p x (Hex.DensePoly.scale c a.coeffs)

@[instance_reducible]

instance Hex.PolyQuot.instSMulRat {p : ZPoly} {x : SimpleRoot p} : SMul Rat (PolyQuot p x)

Equations

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

def Hex.PolyQuot.ofRat {p : ZPoly} {x : SimpleRoot p} (q : Rat) : PolyQuot p x

The rational constant q in reduced coordinates.

Equations

• Hex.PolyQuot.ofRat q = q • 1

def Hex.PolyQuot.ofSquare (p : ZPoly) (s : DyadicSquare) (f : DensePoly Rat) (hw : atomWitness p s := by decide) (hp : ↑(mahlerPrec p) ≤ s.prec := by decide) : PolyQuot p (SimpleRoot.ofSquare p s hw hp)

The element of ℚ(root of pisolated bys) with coordinates f. This is the self-contained form Repr emits: every argument is printable data, and the two root side conditions are decide-discharged auto-params of SimpleRoot.ofSquare.

Equations

• Hex.PolyQuot.ofSquare p s f hw hp = Hex.PolyQuot.reduce p (Hex.SimpleRoot.ofSquare p s hw hp) f

@[instance_reducible]

instance Hex.PolyQuot.instCoeDensePolyRat {p : ZPoly} {x : SimpleRoot p} : Coe (DensePoly Rat) (PolyQuot p x)

A rational polynomial denotes its reduction, so #p[0, 0, 2] names the element 2x² when the expected type is PolyQuot p x.

Equations

• Hex.PolyQuot.instCoeDensePolyRat = { coe := Hex.PolyQuot.reduce p x }

@[instance_reducible]

instance Hex.PolyQuot.instNatCast {p : ZPoly} {x : SimpleRoot p} : NatCast (PolyQuot p x)

Equations

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

@[instance_reducible]

instance Hex.PolyQuot.instIntCast {p : ZPoly} {x : SimpleRoot p} : IntCast (PolyQuot p x)

Equations

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

@[instance_reducible, instance 90]

instance Hex.PolyQuot.instOfNatHAddNatOfNat {p : ZPoly} {x : SimpleRoot p} (n : Nat) : OfNat (PolyQuot p x) (n + 2)

Equations

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

def Hex.PolyQuot.inv {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) : PolyQuot p x

Inversion in a checked irreducible presentation, with 0⁻¹ = 0. The one-sided extended gcd tracks only the Bezout coefficient used for the inverse; the constant-gcd check is a defensive executable guard whose failure is unreachable under checked irreducibility.

Equations

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

@[instance_reducible]

instance Hex.PolyQuot.instInvOfCheckedIrreducible {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] : Inv (PolyQuot p x)

Equations

• Hex.PolyQuot.instInvOfCheckedIrreducible = { inv := Hex.PolyQuot.inv }

def Hex.PolyQuot.div {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a b : PolyQuot p x) : PolyQuot p x

Division in a checked irreducible presentation.

Equations

• a.div b = a * b⁻¹

@[instance_reducible]

instance Hex.PolyQuot.instDivOfCheckedIrreducible {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] : Div (PolyQuot p x)

Equations

• Hex.PolyQuot.instDivOfCheckedIrreducible = { div := Hex.PolyQuot.div }

@[irreducible]

def Hex.PolyQuot.natPow {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) : Nat → PolyQuot p x

Natural powers by repeated squaring using executable fixed-presentation multiplication.

Equations

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

@[instance_reducible]

instance Hex.PolyQuot.instPowNat {p : ZPoly} {x : SimpleRoot p} : Pow (PolyQuot p x) Nat

Equations

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

def Hex.PolyQuot.intPow {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) : Int → PolyQuot p x

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.PolyQuot.instPowIntOfCheckedIrreducible {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] : Pow (PolyQuot p x) Int

Equations

• Hex.PolyQuot.instPowIntOfCheckedIrreducible = { pow := Hex.PolyQuot.intPow }

def Hex.PolyQuot.approx {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (prec : Int) : RefinedIsolation p × DyadicComplexBall

Refine a fixed-field generator representative once and evaluate canonical coordinates on its disc. The checked driver's none fallback retains the original representative and therefore still returns a sound ball; the companion proves that branch unreachable and proves the requested radius.

Equations

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

theorem Hex.PolyQuot.approx_root {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (prec : Int) : SimpleRoot.mk (a.approx rep h prec).fst = x

The representative returned by Hex.PolyQuot.approx denotes the input root, so callers can pass it directly to their next approximation request.