def Hex.AlgebraicNumber.separationPrec (p : ZPoly) : Int

A precision at which the approximation balls of two distinct roots of p are disjoint: mahlerPrec p separates the roots by more than four ball radii at mahlerPrec p, and two more bits leave room for the centre errors.

Equations

• Hex.AlgebraicNumber.separationPrec p = ↑(Hex.mahlerPrec p) + 2

def Hex.AlgebraicNumber.I : AlgebraicNumber

The imaginary unit: the root of X² + 1 whose stored isolation lies in the upper half plane.

Equations

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

def Hex.AlgebraicNumber.mirrorBall (b : DyadicComplexBall) : DyadicComplexBall

The mirror image of a ball in the real axis.

Equations

• Hex.AlgebraicNumber.mirrorBall b = { re := b.re, im := -b.im, radius := b.radius }

def Hex.AlgebraicNumber.conj (a : AlgebraicNumber) : AlgebraicNumber

Complex conjugation. A real number is its own conjugate. Otherwise the conjugate is a root of the same minimal polynomial, and at separationPrec it is the unique root whose approximation ball meets the mirror image of this number's ball.

Equations

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

def Hex.AlgebraicNumber.realCompare (a b : AlgebraicNumber) : Ordering

Exact comparison of two real algebraic numbers. Equal numbers compare equal; distinct ones are distinct roots of the product of their minimal polynomials, whose approximation balls at separationPrec of that product are disjoint, so the order of the ball centres is the order of the numbers.

Equations

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

def Hex.AlgebraicNumber.ofPoint (re im : Rat) : AlgebraicNumber

The rational point re + im·i as an algebraic number.

Equations

• Hex.AlgebraicNumber.ofPoint re im = Hex.AlgebraicNumber.ofRat re + Hex.AlgebraicNumber.ofRat im * Hex.AlgebraicNumber.I

def Hex.AlgebraicNumber.distSqTo (a : AlgebraicNumber) (re im : Rat) : AlgebraicNumber

The squared distance from re + im·i to a, as an exact real algebraic number: (a − z)(ā − z̄).

Equations

• a.distSqTo re im = (a - Hex.AlgebraicNumber.ofPoint re im) * (a.conj - Hex.AlgebraicNumber.ofPoint re (-im))

def Hex.AlgebraicNumber.absRat (q : Rat) : Rat

Absolute value of a rational.

Equations

• Hex.AlgebraicNumber.absRat q = if q < 0 then -q else q

def Hex.AlgebraicNumber.ballDistSq (b : DyadicComplexBall) (re im : Rat) : Rat

The squared distance from re + im·i to a ball's centre.

Equations

• Hex.AlgebraicNumber.ballDistSq b re im = (b.re.toRat - re) * (b.re.toRat - re) + (b.im.toRat - im) * (b.im.toRat - im)

def Hex.AlgebraicNumber.ballDistBound (b : DyadicComplexBall) (re im : Rat) : Rat

A square-root-free upper bound on the distance from re + im·i to a ball's centre: the sum of the absolute coordinate differences.

Equations

• Hex.AlgebraicNumber.ballDistBound b re im = Hex.AlgebraicNumber.absRat (b.re.toRat - re) + Hex.AlgebraicNumber.absRat (b.im.toRat - im)

def Hex.AlgebraicNumber.ballUpper (b : DyadicComplexBall) (re im : Rat) : Rat

Upper bound on the squared distance from re + im·i to a ball's points: d + 2rl + r² with d the squared centre distance, r the radius and l the centre distance bound.

Equations

• Hex.AlgebraicNumber.ballUpper b re im = Hex.AlgebraicNumber.ballDistSq b re im + 2 * b.radius.toRat * Hex.AlgebraicNumber.ballDistBound b re im + b.radius.toRat * b.radius.toRat

def Hex.AlgebraicNumber.ballLower (b : DyadicComplexBall) (re im : Rat) : Rat

Lower bound on the squared distance from re + im·i to a ball's points: d − 2rl + r² when the ball does not reach the point (r² ≤ d), else 0.

Equations

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

def Hex.AlgebraicNumber.certifiedNearest (roots : Array AlgebraicNumber) (a : AlgebraicNumber) (prec : Int) (re im : Rat) : Bool

Whether a is certified nearer to re + im·i than every other listed root, by ball bounds alone.

Equations

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

def Hex.AlgebraicNumber.exactStep (re im : Rat) (best : Option AlgebraicNumber) (c : AlgebraicNumber) : Option AlgebraicNumber

One step of the exact choice: keep the incumbent unless the candidate is strictly nearer.

Equations

• Hex.AlgebraicNumber.exactStep re im none c = some c
• Hex.AlgebraicNumber.exactStep re im (some b) c = if ((c.distSqTo re im).realCompare (b.distSqTo re im) == Ordering.lt) = true then some c else some b

def Hex.AlgebraicNumber.exactNearest (roots : Array AlgebraicNumber) (re im : Rat) : Option AlgebraicNumber

The exact choice: the first root in the array order whose squared distance to the point is minimal.

Equations

• Hex.AlgebraicNumber.exactNearest roots re im = Array.foldl (Hex.AlgebraicNumber.exactStep re im) none roots

@[irreducible]

def Hex.ZPoly.rootNear (p : ZPoly) (re : Rat) (im : Rat := 0) : AlgebraicNumber

The root of p nearest to re + im·i; among roots at the same distance, the first in algebraicRoots order. The fast path certifies a nearest root from approximation balls at AlgebraicNumber.separationPrec p; when that fails, because two roots are nearly or exactly equidistant, the exact squared distances decide. A constant polynomial has no roots and yields 0.

Irreducible, like algebraicRoots: a type such as QAdjoin (rootNear p re) is reduced by #eval while it looks for a printing instance, and must not run the root search symbolically. Proofs unfold it explicitly.

Equations

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

def Hex.AlgebraicNumber.Display.decimal (q : Rat) (digits : Nat) : String

q truncated toward zero to digits decimal places, as a Lean literal: an integer when the fraction is zero, otherwise d.ddd, negatives in parentheses. A display helper; it carries no contract.

Equations

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

def Hex.AlgebraicNumber.Display.digitsFor (mahler : Nat) : Nat

Decimal places at which a truncated isolation centre still names its root: 10 ^ -digits ≤ 2 ^ -mahlerPrec, so the printed point is within (1 + √2) · 2 ^ -mahlerPrec of the root, less than half the root separation.

Equations

• Hex.AlgebraicNumber.Display.digitsFor mahler = mahler / 3 + 1

@[instance_reducible]

instance Hex.AlgebraicNumber.instRepr : Repr AlgebraicNumber

A canonical number prints as the expression that rebuilds it: ZPoly.rootNear p re for a real number and ZPoly.rootNear p re im otherwise, with re and im the stored isolation centre truncated to digitsFor (mahlerPrec p) decimals, few enough to read and enough that the printed point is nearer to this root than to any other (rootNear_of_close).

Equations

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

@[instance_reducible]

instance Hex.instReprQAdjoin (a : AlgebraicNumber) : Repr (QAdjoin a)

An element of ℚ(a) prints as the expression that rebuilds it: the generating number, which prints round-trippably itself, and the reduced coordinates. This is why QAdjoin is a def rather than an abbrev: the PolyQuot instance would otherwise win, and that one can only name the root by its isolating square. Carrying the number instead of a square, this form also leaves no decide side conditions to discharge when it is pasted back.

Equations

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