29.1. Introduction🔗

HexNumberField computes with algebraic numbers exactly. An algebraic number is stored as its minimal polynomial over the integers together with a certified disc that singles out one complex root. For example, √2 + √3 is represented by the polynomial X⁴ − 10X² + 1 and a small disc around 3.146. Addition, multiplication, inversion and powers return numbers in the same normal form.

There's an important subtlety here: many discs isolate the same root, so a number could have many representations. The library carefully arranges that there is always a canonically specified disc. This means that equality works the way you expect it to, and cheaply: two numbers are equal exactly when their polynomials agree and their stored discs meet, so no refinement happens while comparing. The library doesn't use floating-point numbers anywhere. The discs have dyadic rational centres and radii, and each carries a certificate, checked by ordinary evaluation, that it contains exactly one root.

This representation is very convenient, but sometimes for efficiency it is useful to have more control over the representation. We additionally provide Hex.AlgebraicRoot and Hex.QAdjoin.

A term of type Hex.AlgebraicRoot is a root of some squarefree integer polynomial that need not be minimal. This gives up unique representatives, but can be more efficient for intermediate results. In particular, the sum of two roots is a root of a resultant, and factoring that resultant is postponed until a canonical answer is requested with Hex.AlgebraicRoot.exact.

A term of type Hex.QAdjoin is an element of the field ℚ(a) generated by one single algebraic number, with elements written as rational coordinates in the power basis. Arithmetic here is just polynomial arithmetic modulo the minimal polynomial and never involves further root isolation.

The correspondence library HexNumberFieldMathlib interprets every representation in ℂ. It proves that the interpretation of canonical numbers is injective, that each executable operation computes the corresponding complex operation, and it provides a computable Field instance on Hex.AlgebraicNumber.

The first entry point into the library is Hex.ZPoly.algebraicRoots, which turns an integer polynomial into its roots as canonical algebraic numbers.

structure

Hex.AlgebraicNumber : Type
Hex.AlgebraicNumber : Type

A canonical algebraic number. Construction is sealed so each normalized polynomial/root pair receives one fixed representative.

Fields

p : Hex.ZPoly

The normalized minimal integer polynomial of the represented value.

prim : self.p.Primitive

p has unit content.

pos_lc : 0 < Hex.DensePoly.leadingCoeff self.p

p has positive leading coefficient.

pos_degree : 0 < Hex.DensePoly.natDegree self.p

p has positive degree.

checked : self.p.CheckedIrreducible

The Boolean irreducibility checker accepted p.

squarefree : Hex.HasOnlySimpleRoots self.p

p has only simple roots.

rep : Hex.RefinedIsolation self.p

The certified refined isolation of the represented root.

canonical : Hex.AlgebraicNumber.IsCanonical self.p ⋯ self.rep

The stored representative comes from the deterministic canonical isolation pipeline (or is the fixed representative of zero).

def

Hex.ZPoly.algebraicRoots (p : Hex.ZPoly) : Array Hex.AlgebraicNumber
Hex.ZPoly.algebraicRoots (p : Hex.ZPoly) :
  Array Hex.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, in increasing order, then the nonreal roots in a deterministic order set by their isolations. 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?.

Roots of polynomials whose coefficients are themselves algebraic numbers are found with Hex.AlgebraicPoly.roots.