def Hex.AlgebraicRoot.isReal (a : AlgebraicRoot) : Bool

The selected root is real. Exact at the stored separation precision.

Equations

• a.isReal = a.rep.val.square.meetsRealAxis

def Hex.AlgebraicNumber.isReal (a : AlgebraicNumber) : Bool

The represented number is real. Exact at the stored separation precision.

Equations

• a.isReal = decide (a.side = Hex.AlgebraicNumber.RootSide.real)

@[simp]

theorem Hex.AlgebraicNumber.conj_of_isReal (a : AlgebraicNumber) (h : a.isReal = true) : a.conj = a

A successful reality test makes conjugation the identity.

def Hex.AlgebraicNumber.rootLe (a b : AlgebraicNumber) : Bool

Deterministic root enumeration: real roots first by their isolation centres; then adjacent conjugate pairs, ordered by the upper base's height and real coordinate. Precision and minimal polynomial distinguish pairs before the negative-imaginary member is placed first. This is an order of stored data, not exact lexicographic comparison of the complex coordinates.

Equations

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

def Hex.AlgebraicNumber.approx (a : AlgebraicNumber) (prec : Int := 64) : DyadicComplexBall

A dyadic complex ball of radius at most 2^(-prec) around the value, evaluated on the stored representative.

Equations

• a.approx prec = (Hex.PolyQuot.approx a.toQAdjoin a.rep ⋯ prec).snd

def Hex.AlgebraicRoot.ofRefined (q : ZPoly) (prim : q.content = 1) (pos_lc : 0 < DensePoly.leadingCoeff q) (pos_degree : 0 < DensePoly.natDegree q) (squarefree : HasOnlySimpleRoots q) (rep : RefinedIsolation q) : AlgebraicRoot

The lazy root selected by one refined isolation of a normalized squarefree polynomial.

Equations

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

@[irreducible]

def Hex.ZPoly.algebraicRoots? (p : ZPoly) : Option (Array AlgebraicNumber)

Every distinct complex root of p as a canonical algebraic number, or none if a certificate could not be produced. See algebraicRoots.

Irreducible, like algebraicRoots, so that a type such as PolyQuot a.p a.x for a root a found here is cheap to reduce: #eval reduces the type of a value while looking for a printing instance, and must not run the root isolation symbolically. Proofs unfold it explicitly.

Equations

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

@[irreducible]

def Hex.ZPoly.algebraicRoots (p : ZPoly) : Array AlgebraicNumber

Every distinct complex root of p as a canonical algebraic number: the squarefree primitive part of p is isolated, and each isolated root is exactified. Real roots come first by isolation centre, then adjacent nonreal conjugate pairs with the lower member first. For exact value ordering of real roots use ZPoly.realAlgebraicRoots from HexRealAlgebraic. Multiplicities are not returned; use AlgebraicPoly.roots for them. A constant polynomial, including zero, has no roots here. Irreducible for the reason given at algebraicRoots?.

Equations

• p.algebraicRoots = p.algebraicRoots?.getD (Hex.panicWith #[] "ZPoly.algebraicRoots: certification failed")

def Hex.Display.dyadic : Dyadic → String

A dyadic as the expression that rebuilds it. Dyadic is a core inductive with no Repr; ofOdd n k denotes n · 2⁻ᵏ, which is ofIntWithPrec n k.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Display.dyadic Dyadic.zero = "0"

def Hex.Display.square (s : DyadicSquare) : String

A square as the anonymous constructor its three fields rebuild.

Equations

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

def Hex.Display.certificate {p : ZPoly} {s : DyadicSquare} : AtomCertificate p s → String

Replay a certificate's actual constructors; transported certificates need not pass a fresh numerical check at their final square.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Display.certificate (Hex.AtomCertificate.nk h) = toString "(@Hex.AtomCertificate.nk (" ++ toString (repr p) ++ toString ") (" ++ toString (Hex.Display.square s) ++ toString ") (by decide))"

@[instance_reducible]

unsafe instance Hex.instReprPolyQuot {p : ZPoly} {x : SimpleRoot p} : Repr (PolyQuot p x)

A fixed-field element prints as the expression that rebuilds it: PolyQuot.ofSquare replays a direct NK/Pellet certificate; PolyQuot.ofIsolation replays the actual certificate constructors when the representative was transported. Both include the reduced coordinates and select the same root. A transported square need not pass a fresh checker.

The representative comes out of the Quot by unquot, as Mathlib's Multiset and Finset instances do, so the instance is unsafe and the printed square is whichever representative the value happens to carry. That choice is invisible in the result: Intersects compares stored squares, so every representative of the root rebuilds the same element.

Equations

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