def Hex.AlgebraicNumber.Radical.rank (a : AlgebraicNumber) : Int

Rank the sign of the imaginary coordinate without computing the coordinate.

Equations

• Hex.AlgebraicNumber.Radical.rank a = match a.side with | Hex.AlgebraicNumber.RootSide.lower => -1 | Hex.AlgebraicNumber.RootSide.real => 0 | Hex.AlgebraicNumber.RootSide.upper => 1

structure Hex.AlgebraicNumber.Radical.Candidate : Type

A root candidate with its doubled real part computed once.

• value : AlgebraicNumber
• twiceRe : AlgebraicNumber
• correct : self.twiceRe = self.value + self.value.conj

def Hex.AlgebraicNumber.Radical.candidate (r : RootCount) : Candidate

Exactify a root and cache the real coordinate used in branch selection.

Equations

• Hex.AlgebraicNumber.Radical.candidate r = { value := r.root.exact, twiceRe := r.root.exact + r.root.exact.conj, correct := ⋯ }

def Hex.AlgebraicNumber.Radical.choose (a b : Candidate) : Candidate

Prefer greater real part, then the upper imaginary side.

Equations

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

def Hex.AlgebraicNumber.Radical.select (roots : Array RootCount) : Option Candidate

Select one principal candidate, sharing cached coordinates throughout the fold.

Equations

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

def Hex.AlgebraicRoot.side (a : AlgebraicRoot) : AlgebraicNumber.RootSide

The exact imaginary side of a lazy root, without factorization.

Equations

• a.side = Hex.AlgebraicNumber.sideOf a.rep

structure Hex.RootSelection.Work : Type

One lazy root with its original precision, retained across refinement rounds.

• root : AlgebraicRoot
• prec : Int

def Hex.RootSelection.same (a b : AlgebraicRoot) : Bool

Same-polynomial root identity needs only the stored isolations.

Equations

• Hex.RootSelection.same a b = if h : a.p = b.p then (h ▸ a.rep).sameRoot b.rep else false

def Hex.RootSelection.pick (a b : Work) : Work

Choose a proposed maximum by its centre; the proposal is checked separately.

Equations

• Hex.RootSelection.pick a b = if a.root.rep.val.square.re < b.root.rep.val.square.re then b else a

def Hex.RootSelection.dominates (a b : Work) : Bool

A candidate is accepted only if every other value is equal or strictly to its left.

Equations

• Hex.RootSelection.dominates a b = (Hex.RootSelection.same a.root b.root || Hex.Interval.realOrder? b.root.rep.val.square a.root.rep.val.square == some Ordering.lt)

def Hex.RootSelection.probe : List Work → Option Work

Linear-time proposal and validation; no candidate is exactified.

Equations

• One or more equations did not get rendered due to their size.
• Hex.RootSelection.probe [] = none

def Hex.RootSelection.refine? (bits : Nat) (a : Work) : Option Work

Refine from the cached representative, relative to its original precision.

Equations

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

def Hex.RootSelection.search : List Nat → List Work → Option AlgebraicRoot

Bounded selection with one cached representative per candidate.

Equations

• One or more equations did not get rendered due to their size.
• Hex.RootSelection.search [] x✝ = match Hex.RootSelection.probe x✝ with | some best => some best.root | none => none

def Hex.RootSelection.select? (roots : List AlgebraicRoot) : Option AlgebraicRoot

Select a certified maximum real part, or leave the decision to an exact fallback.

Equations

• Hex.RootSelection.select? roots = Hex.RootSelection.search [16, 64] (List.map (fun (r : Hex.AlgebraicRoot) => { root := r, prec := r.rep.val.square.prec }) roots)

def Hex.RootSelection.maximum? (roots : List AlgebraicRoot) : Option AlgebraicNumber

A total-on-nonempty maximum selector, with the exact coordinate comparison retained only as a fallback for inconclusive interval probes.

Equations

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

def Hex.RootSelection.integerRoots? (p : ZPoly) : Option (Array AlgebraicRoot)

The integer root solver before exactification. This shares the checked normalization/isolation pipeline of ZPoly.algebraicRoots?, without factoring or canonicalizing every root.

Equations

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