instance Hex.AlgebraicNumber.instCheckedIrreducibleP (a : AlgebraicNumber) : a.p.CheckedIrreducible

The minimal polynomial of a canonical algebraic number carries checked irreducibility, so PolyQuot a.p a.x has inversion and division without the evidence being registered by hand.

@[implicit_reducible]

def Hex.QAdjoin (a : AlgebraicNumber) : Type

The fixed field ℚ(a) of a canonical algebraic number: the presentation ring on its minimal polynomial, with the embedding fixed by the root it denotes. Reducible, so every PolyQuot operation, instance and theorem applies unchanged.

Equations

• Hex.QAdjoin a = Hex.PolyQuot a.p a.x

@[instance_reducible]

instance Hex.instDecidableEqQAdjoin {a : AlgebraicNumber} : DecidableEq (QAdjoin a)

Equations

• Hex.instDecidableEqQAdjoin = Hex.instDecidableEqQAdjoin._aux_1

@[instance_reducible]

instance Hex.instZeroQAdjoin {a : AlgebraicNumber} : Zero (QAdjoin a)

Equations

• Hex.instZeroQAdjoin = { zero := Hex.instZeroQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instOneQAdjoin {a : AlgebraicNumber} : One (QAdjoin a)

Equations

• Hex.instOneQAdjoin = { one := Hex.instOneQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instAddQAdjoin {a : AlgebraicNumber} : Add (QAdjoin a)

Equations

• Hex.instAddQAdjoin = { add := Hex.instAddQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instSubQAdjoin {a : AlgebraicNumber} : Sub (QAdjoin a)

Equations

• Hex.instSubQAdjoin = { sub := Hex.instSubQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instNegQAdjoin {a : AlgebraicNumber} : Neg (QAdjoin a)

Equations

• Hex.instNegQAdjoin = { neg := Hex.instNegQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instMulQAdjoin {a : AlgebraicNumber} : Mul (QAdjoin a)

Equations

• Hex.instMulQAdjoin = { mul := Hex.instMulQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instSMulRatQAdjoin {a : AlgebraicNumber} : SMul Rat (QAdjoin a)

Equations

• Hex.instSMulRatQAdjoin = { smul := Hex.instSMulRatQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instCoeDensePolyRatQAdjoin {a : AlgebraicNumber} : Coe (DensePoly Rat) (QAdjoin a)

Equations

• Hex.instCoeDensePolyRatQAdjoin = { coe := Hex.instCoeDensePolyRatQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instNatCastQAdjoin {a : AlgebraicNumber} : NatCast (QAdjoin a)

Equations

• Hex.instNatCastQAdjoin = { natCast := Hex.instNatCastQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instIntCastQAdjoin {a : AlgebraicNumber} : IntCast (QAdjoin a)

Equations

• Hex.instIntCastQAdjoin = { intCast := Hex.instIntCastQAdjoin._aux_1 }

@[instance_reducible, instance 90]

instance Hex.instOfNatQAdjoinHAddNatOfNat {a : AlgebraicNumber} (n : Nat) : OfNat (QAdjoin a) (n + 2)

Equations

• Hex.instOfNatQAdjoinHAddNatOfNat n = { ofNat := Hex.instOfNatQAdjoinHAddNatOfNat._aux_1 n }

@[instance_reducible]

instance Hex.instInvQAdjoin {a : AlgebraicNumber} : Inv (QAdjoin a)

Equations

• Hex.instInvQAdjoin = { inv := Hex.instInvQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instDivQAdjoin {a : AlgebraicNumber} : Div (QAdjoin a)

Equations

• Hex.instDivQAdjoin = { div := Hex.instDivQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instPowQAdjoinNat {a : AlgebraicNumber} : Pow (QAdjoin a) Nat

Equations

• Hex.instPowQAdjoinNat = { pow := Hex.instPowQAdjoinNat._aux_1 }

@[instance_reducible]

instance Hex.instPowQAdjoinInt {a : AlgebraicNumber} : Pow (QAdjoin a) Int

Equations

• Hex.instPowQAdjoinInt = { pow := Hex.instPowQAdjoinInt._aux_1 }

def Hex.QAdjoin.ofCoeffs (a : AlgebraicNumber) (f : DensePoly Rat) : QAdjoin a

The element of ℚ(a) with coordinates f in the power basis of a. Unlike PolyQuot.ofSquare this needs no square and no side conditions: the generating number already carries its own root.

Equations

• Hex.QAdjoin.ofCoeffs a f = Hex.PolyQuot.reduce a.p a.x f

def Hex.AlgebraicNumber.toQAdjoin (a : AlgebraicNumber) : QAdjoin a

The canonical algebraic number as the generator of its own fixed field.

Equations

• a.toQAdjoin = Hex.PolyQuot.reduce a.p a.x (Hex.DensePoly.ofList [0, 1])

def Hex.AlgebraicNumber.toRoot (a : AlgebraicNumber) : AlgebraicRoot

Forget minimality while retaining every checked root certificate.

Equations

• a.toRoot = { p := a.p, prim := ⋯, pos_lc := ⋯, pos_degree := ⋯, squarefree := ⋯, x := a.x, rep := a.rep, rep_mk := ⋯ }

def Hex.AlgebraicRoot.exactFactor? (a : AlgebraicRoot) (q : ZPoly) : Option AlgebraicNumber

Try one normalized factor of a lazy root's enclosing polynomial. Candidate isolations are refined to the enclosing polynomial's separation precision before their discs are compared.

Equations

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

theorem Hex.AlgebraicRoot.exactFactor?_eq (a : AlgebraicRoot) (q : ZPoly) : a.exactFactor? q = if hprim : q.content = 1 then if hpos : 0 < DensePoly.leadingCoeff q then if hdegree : 0 < DensePoly.natDegree q then if hirred : q.isIrreducible = true then if hsquarefree : HasOnlySimpleRoots q then do let isolations ← q.isolateComplexRoots? hsquarefree ↑(separationDepth q) let refined ← Array.mapM DyadicRootIsolation.toRefined? isolations let comparable ← Array.mapM (fun (r : RefinedIsolation q) => (r.refineTo? ↑(mahlerPrec a.p)).unattach) refined let matching ← List.find? (fun (r : RefinedIsolation q) => decide (↑(mahlerPrec a.p) ≤ r.val.square.prec) && r.val.square.discsMeet a.rep.val.square) comparable.toList AlgebraicNumber.ofNormalized? q hprim hpos hdegree ⋯ hsquarefree matching else none else none else none else none else none

Certified isolation reuse preserves the original exactification pipeline, including its canonical stored representative and all checked failures.

def Hex.AlgebraicRoot.exact? (a : AlgebraicRoot) : Option AlgebraicNumber

Factor a lazy root's enclosing polynomial and select the normalized irreducible factor containing its chosen root. none is a checked implementation branch whose unreachability is proved by the Mathlib companion.

Equations

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

def Hex.AlgebraicRoot.exactParent? (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) : Option AlgebraicNumber

Exactify the enclosing polynomial using a certified isolation run already computed by its producer. Reducible enclosing polynomials are rejected here.

Equations

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

theorem Hex.AlgebraicRoot.exactParent?_eq (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) : a.exactParent? isolations refined hisolate hrefine = a.exactFactor? a.p

Reusing the parent run preserves the complete factor selector result.

def Hex.AlgebraicRoot.exactIn? (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) : Option AlgebraicNumber

Exactification reusing the enclosing polynomial's certified isolation when a returned factor is that polynomial. Proper factors use their own runs.

Equations

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

theorem Hex.AlgebraicRoot.exactIn?_eq (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) : a.exactIn? isolations refined hisolate hrefine = a.exact?

Parent isolation reuse changes neither canonical representatives nor checked failures of exactification, including reducible enclosing polynomials.

def Hex.AlgebraicRoot.exact (a : AlgebraicRoot) : AlgebraicNumber

Canonicalize a lazy root: the total form of exact?, whose none branch the theory companion proves unreachable.

Equations

• a.exact = a.exact?.getD (Hex.panicWith 0 "AlgebraicRoot.exact: certification failed")

def Hex.PolyQuot.krylovPowers {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) (n : Nat) : Vector (PolyQuot p x) (n + 1)

The first n + 1 Krylov powers, built with one multiplication per step.

Equations

• a.krylovPowers 0 = #v[1]
• a.krylovPowers n.succ = (a.krylovPowers n).push ((a.krylovPowers n).get (Fin.last n) * a)

def Hex.PolyQuot.krylovOrbit {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) : Vector (PolyQuot p x) (DensePoly.natDegree p + 1)

Krylov orbit 1, a, a², ... through the defining-field dimension.

Equations

• a.krylovOrbit = a.krylovPowers (Hex.DensePoly.natDegree p)

def Hex.PolyQuot.relationPoly {k : Nat} (coeffs : Vector Rat k) : DensePoly Rat

The monic polynomial encoded by a Krylov dependence vector.

Equations

• Hex.PolyQuot.relationPoly coeffs = Hex.DensePoly.ofCoeffs ((Array.map (fun (c : Rat) => -c) coeffs.toArray).push 1)

def Hex.PolyQuot.relationAt? {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (_a : PolyQuot p x) (orbit : Vector (PolyQuot p x) (DensePoly.natDegree p + 1)) (k : Nat) : Option ZPoly

The monic relation at one Krylov-orbit index, when the new power is in the span of its predecessors.

Equations

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

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

First monic relation in the Krylov orbit of the multiplication operator, normalized as a primitive positive-leading integer polynomial.

Equations

• a.minpoly? = List.findSome? (fun (i : Nat) => a.relationAt? a.krylovOrbit (i + 1)) (List.range (Hex.DensePoly.natDegree p))

def Hex.PolyQuot.toAlgebraicNumber? {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (_h : SimpleRoot.mk rep = x) : Option AlgebraicNumber

Convert a fixed-presentation value to its canonical irreducible representation. Every stored certificate and every precision-sensitive step is checked before construction.

Equations

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

theorem Hex.PolyQuot.toAlgebraicNumber?_eq {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : a.toAlgebraicNumber? rep h = do let q ← a.minpoly? if hprim : q.content = 1 then if hpos : 0 < DensePoly.leadingCoeff q then if hdegree : 0 < DensePoly.natDegree q then if hirred : q.isIrreducible = true then if hsquarefree : HasOnlySimpleRoots q then do let isolations ← q.isolateComplexRoots? hsquarefree ↑(separationDepth q) let refined ← Array.mapM DyadicRootIsolation.toRefined? isolations have requested : Int := ↑(mahlerPrec q) have target : Int := requested + ↑(approxGuardBits rep.val.square a.coeffs) let threaded ← rep.refineTo? target have valueBall : DyadicComplexBall := evalRatBall a.coeffs threaded.val.val.square target let matching ← List.find? (fun (r : RefinedIsolation q) => r.val.square.meetsBall valueBall) refined.toList AlgebraicNumber.ofNormalized? q hprim hpos hdegree ⋯ hsquarefree matching else none else none else none else none else none

Reusing the certified isolation run preserves the complete canonical conversion result, including every stored representative and checked failure.

def Hex.PolyQuot.toAlgebraicNumber {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : AlgebraicNumber

Total fixed-presentation conversion. The checked failure branch is proved unreachable by the theory companion.

Equations

• a.toAlgebraicNumber rep h = (a.toAlgebraicNumber? rep h).getD (Hex.panicWith 0 "PolyQuot.toAlgebraicNumber: certification failed")

def Hex.QAdjoin.toAlgebraicNumber? {a : AlgebraicNumber} (c : QAdjoin a) : Option AlgebraicNumber

The canonical number an element of ℚ(a) denotes, or none if the certification failed. The general form applied with a's own representative.

Equations

• c.toAlgebraicNumber? = Hex.PolyQuot.toAlgebraicNumber? c a.rep ⋯

def Hex.QAdjoin.toAlgebraicNumber {a : AlgebraicNumber} (c : QAdjoin a) : AlgebraicNumber

The canonical number an element of ℚ(a) denotes.

Equations

• c.toAlgebraicNumber = Hex.PolyQuot.toAlgebraicNumber c a.rep ⋯