21.7. HexNumberField: exact algebraic numbers🔗

21.7.1. Introduction🔗

HexNumberField provides executable exact arithmetic for selected complex algebraic roots, both in a fixed rational presentation and in a canonical minimal-polynomial form.

21.7.2. Three representations🔗

HexNumberField provides three complementary exact representations. Hex.QAdjoin stores rational power-basis coordinates in one fixed irreducible presentation. Hex.AlgebraicRoot stores a certified selected root of a squarefree integer polynomial without requiring that polynomial to be minimal. Hex.AlgebraicNumber is the canonical form: a selected root of its normalized irreducible minimal polynomial.

The distinction makes routine arithmetic cheaper. Addition and multiplication first build a resultant eliminant and isolate the intended result; factoring to a minimal polynomial is postponed until a caller requests Hex.AlgebraicRoot.exact.

21.7.3. Fixed-field arithmetic and approximation🔗

Fixed-presentation coordinates are always reduced modulo the defining integer polynomial. Inversion uses polynomial extended gcd and follows the total field convention 0⁻¹ = 0.

def

Hex.QAdjoin.reduce (p : Hex.ZPoly) (x : Hex.SimpleRoot p)
  (f : Hex.DensePoly ℚ) : Hex.QAdjoin p x
Hex.QAdjoin.reduce (p : Hex.ZPoly)
  (x : Hex.SimpleRoot p)
  (f : Hex.DensePoly ℚ) : Hex.QAdjoin p x

Package a rational polynomial after canonical modular reduction.

def

Hex.QAdjoin.inv {p : Hex.ZPoly} {x : Hex.SimpleRoot p}
  [p.CheckedIrreducible] (a : Hex.QAdjoin p x) : Hex.QAdjoin p x
Hex.QAdjoin.inv {p : Hex.ZPoly}
  {x : Hex.SimpleRoot p}
  [p.CheckedIrreducible]
  (a : Hex.QAdjoin p x) : Hex.QAdjoin p x

Inversion in a checked irreducible presentation, with 0⁻¹ = 0. The one-sided extended gcd tracks only the Bezout coefficient used for the inverse; the constant-gcd check is a defensive executable guard whose failure is unreachable under checked irreducibility.

Approximation takes a root representative, refines it, and evaluates the reduced coordinate polynomial with dyadic complex-ball Horner arithmetic. The returned representative can be threaded into the next request so earlier work is not repeated.

def

Hex.QAdjoin.approx {p : Hex.ZPoly} {x : Hex.SimpleRoot p}
  (a : Hex.QAdjoin p x) (rep : Hex.RefinedIsolation p)
  (h : Hex.SimpleRoot.mk rep = x) (prec : ℤ) :
  Hex.RefinedIsolation p × Hex.DyadicComplexBall
Hex.QAdjoin.approx {p : Hex.ZPoly}
  {x : Hex.SimpleRoot p}
  (a : Hex.QAdjoin p x)
  (rep : Hex.RefinedIsolation p)
  (h : Hex.SimpleRoot.mk rep = x)
  (prec : ℤ) :
  Hex.RefinedIsolation p ×
    Hex.DyadicComplexBall

Refine a fixed-field generator representative once and evaluate canonical coordinates on its disc. The checked driver's none fallback retains the original representative and therefore still returns a sound ball; the companion proves that branch unreachable and proves the requested radius.

Here is fixed-field multiplication and inversion in ℚ(√2):

open Hex

namespace HexNumberFieldChapter

private def sqrtTwoPoly : ZPoly :=
  DensePoly.ofList [-2, 0, 1]

private def sqrtTwoSquare : DyadicSquare :=
  ⟨Dyadic.ofIntWithPrec 181 7, 0, 8⟩

private def sqrtTwoRep : RefinedIsolation sqrtTwoPoly :=
  ⟨⟨sqrtTwoSquare, .ofWitness (by⊢ atomWitness sqrtTwoPoly sqrtTwoSquare decideAll goals completed! 🐙)⟩, by⊢ ↑(mahlerPrec sqrtTwoPoly) ≤ { square := sqrtTwoSquare, witness := AtomCertificate.ofWitness ⋯ }.square.prec decideAll goals completed! 🐙⟩

private def sqrtTwoRoot : SimpleRoot sqrtTwoPoly :=
  SimpleRoot.mk sqrtTwoRep

#guard
  if hirred : ZPoly.isIrreducible sqrtTwoPoly = true then
    letI : ZPoly.CheckedIrreducible sqrtTwoPoly :=
      ⟨hirred, byhirred:sqrtTwoPoly.isIrreducible = true⊢ 0 < (DensePoly.degree? sqrtTwoPoly).getD 0 decideAll goals completed! 🐙⟩
    let xPoly :=
      DensePoly.ofList ([0, 1] : List Rat)
    let x : QAdjoin sqrtTwoPoly sqrtTwoRoot :=
      QAdjoin.reduce sqrtTwoPoly sqrtTwoRoot xPoly
    let two : QAdjoin sqrtTwoPoly sqrtTwoRoot :=
      QAdjoin.reduce sqrtTwoPoly sqrtTwoRoot
        (DensePoly.C 2)
    x * x = two && x * x⁻¹ = 1
  else
    false

end HexNumberFieldChapter

21.7.4. Lazy arithmetic and exactification🔗

Every certificate-producing operation has an Option form. The total form is the primary algebraic API; its loud fallback is paired with a companion completeness contract. In particular, the Mathlib companion proves that the bounded searches for addition, multiplication, inversion, and division always return a certificate. Their total wrappers therefore compute the corresponding complex operations, including the convention 0⁻¹ = 0. Subtraction composes addition with certificate-free polynomial reflection.

def

Hex.AlgebraicRoot.add? (a b : Hex.AlgebraicRoot) :
  Option Hex.AlgebraicRoot
Hex.AlgebraicRoot.add?
  (a b : Hex.AlgebraicRoot) :
  Option Hex.AlgebraicRoot

Checked lazy sum through the addition eliminant.

def

Hex.AlgebraicRoot.sub? (a b : Hex.AlgebraicRoot) :
  Option Hex.AlgebraicRoot
Hex.AlgebraicRoot.sub?
  (a b : Hex.AlgebraicRoot) :
  Option Hex.AlgebraicRoot

Checked lazy difference.

def

Hex.AlgebraicRoot.mul? (a b : Hex.AlgebraicRoot) :
  Option Hex.AlgebraicRoot
Hex.AlgebraicRoot.mul?
  (a b : Hex.AlgebraicRoot) :
  Option Hex.AlgebraicRoot

Checked lazy product through the product eliminant.

def

Hex.AlgebraicRoot.inv? (a : Hex.AlgebraicRoot) :
  Option Hex.AlgebraicRoot
Hex.AlgebraicRoot.inv?
  (a : Hex.AlgebraicRoot) :
  Option Hex.AlgebraicRoot

Checked lazy inverse through coefficient reversal.

def

Hex.AlgebraicRoot.div? (a b : Hex.AlgebraicRoot) :
  Option Hex.AlgebraicRoot
Hex.AlgebraicRoot.div?
  (a b : Hex.AlgebraicRoot) :
  Option Hex.AlgebraicRoot

Checked lazy quotient.

def

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

Factor a lazy root's enclosing polynomial and select the normalized irreducible factor containing its chosen root.

def

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

Canonicalize a lazy root. Failure is a checked implementation branch whose unreachability is proved by the Mathlib companion.

theorem

Hex.AlgebraicRoot.add?_isSome (a b : Hex.AlgebraicRoot) :
  (a.add? b).isSome = true
Hex.AlgebraicRoot.add?_isSome
  (a b : Hex.AlgebraicRoot) :
  (a.add? b).isSome = true

The bounded lazy addition search always finds its certificate.

theorem

Hex.AlgebraicRoot.mul?_isSome (a b : Hex.AlgebraicRoot) :
  (a.mul? b).isSome = true
Hex.AlgebraicRoot.mul?_isSome
  (a b : Hex.AlgebraicRoot) :
  (a.mul? b).isSome = true

The bounded lazy multiplication search always finds its certificate.

theorem

Hex.AlgebraicRoot.inv?_isSome (a : Hex.AlgebraicRoot) :
  a.inv?.isSome = true
Hex.AlgebraicRoot.inv?_isSome
  (a : Hex.AlgebraicRoot) :
  a.inv?.isSome = true

The bounded lazy inverse search always finds its certificate.

theorem

Hex.AlgebraicRoot.div?_isSome (a b : Hex.AlgebraicRoot) :
  (a.div? b).isSome = true
Hex.AlgebraicRoot.div?_isSome
  (a b : Hex.AlgebraicRoot) :
  (a.div? b).isSome = true

The bounded lazy division search always finds its certificate.

theorem

Hex.AlgebraicRoot.mul_toComplex (a b : Hex.AlgebraicRoot) :
  (a.mul b).toComplex = a.toComplex * b.toComplex
Hex.AlgebraicRoot.mul_toComplex
  (a b : Hex.AlgebraicRoot) :
  (a.mul b).toComplex =
    a.toComplex * b.toComplex

Total lazy multiplication computes complex multiplication.

theorem

Hex.AlgebraicRoot.inv_toComplex (a : Hex.AlgebraicRoot) :
  a.inv.toComplex = a.toComplex⁻¹
Hex.AlgebraicRoot.inv_toComplex
  (a : Hex.AlgebraicRoot) :
  a.inv.toComplex = a.toComplex⁻¹

Total lazy inversion computes complex inversion.

Canonical algebraic numbers reuse these lazy operations and exactify the answer. Their Boolean equality compares represented values rather than record layout. Lazy roots deliberately have no BEq; the root driver uses checked Hex.QAdjoin.Roots.sameValue? instead.

21.7.5. Canonical field arithmetic🔗

Canonical algebraic numbers also provide executable rational construction, casts, scalar multiplication, and natural and integer powers. The Mathlib companion proves that the complex interpretation is injective and installs a lawful Field instance on Hex.AlgebraicNumber whose data fields are these same executable operations.

def

Hex.AlgebraicNumber.ofRat (q : ℚ) : Hex.AlgebraicNumber
Hex.AlgebraicNumber.ofRat (q : ℚ) :
  Hex.AlgebraicNumber

Total executable embedding of a rational number into canonical algebraic numbers. The companion proves that the checked constructor cannot fail.

theorem

Hex.AlgebraicNumber.ofRat_toComplex (q : ℚ) :
  (Hex.AlgebraicNumber.ofRat q).toComplex = ↑q
Hex.AlgebraicNumber.ofRat_toComplex
  (q : ℚ) :
  (Hex.AlgebraicNumber.ofRat
        q).toComplex =
    ↑q

The executable rational embedding has its expected complex value.

theorem

Hex.AlgebraicNumber.toComplex_injective :
  Function.Injective Hex.AlgebraicNumber.toComplex
Hex.AlgebraicNumber.toComplex_injective :
  Function.Injective
    Hex.AlgebraicNumber.toComplex

Canonical algebraic numbers are determined by their represented complex value.

open Hex

example : (2 : AlgebraicNumber) =
    AlgebraicNumber.ofRat 2 := rfl
example (a b : AlgebraicNumber) : a + b =
    AlgebraicNumber.add a b := rfl
example (a : AlgebraicNumber) : a ^ (3 : Nat) =
    AlgebraicNumber.natPow a 3 := rfl

21.7.6. Polynomials and roots🔗

An Hex.AlgebraicPoly owns semantic trailing-zero normalization. This is separate from DensePoly AlgebraicNumber, whose normalizer would require a structural equality decision that is not the intended algebraic equality.

def

Hex.AlgebraicPoly.ofArray (coeffs : Array Hex.AlgebraicNumber) :
  Hex.AlgebraicPoly
Hex.AlgebraicPoly.ofArray
  (coeffs : Array Hex.AlgebraicNumber) :
  Hex.AlgebraicPoly

Construct a polynomial and remove all trailing coefficients whose canonical minimal polynomial is X.

open Hex

-- Trailing canonical zeros are removed semantically.
#guard
  let f := AlgebraicPoly.ofArray
    #[AlgebraicNumber.zero, AlgebraicNumber.zero]
  f.isZero && f.coeffs.isEmpty

Root APIs distinguish the zero polynomial, whose root set is universal, from a finite root array carrying positive multiplicities.

def

Hex.QAdjoin.roots? {p : Hex.ZPoly} {x : Hex.SimpleRoot p}
  [p.CheckedIrreducible] (f : Hex.DensePoly (Hex.QAdjoin p x))
  (rep : Hex.RefinedIsolation p) (h : Hex.SimpleRoot.mk rep = x) :
  Option Hex.RootSet
Hex.QAdjoin.roots? {p : Hex.ZPoly}
  {x : Hex.SimpleRoot p}
  [p.CheckedIrreducible]
  (f : Hex.DensePoly (Hex.QAdjoin p x))
  (rep : Hex.RefinedIsolation p)
  (h : Hex.SimpleRoot.mk rep = x) :
  Option Hex.RootSet

Checked roots of a fixed-field polynomial. none is reserved for a certificate that did not appear within its prescribed finite bound.

def

Hex.AlgebraicPoly.roots? (f : Hex.AlgebraicPoly) : Option Hex.RootSet
Hex.AlgebraicPoly.roots?
  (f : Hex.AlgebraicPoly) :
  Option Hex.RootSet

Checked roots of a polynomial with canonical algebraic coefficients. All nonzero coefficients are first embedded in one bounded deterministic primitive presentation, then the fixed-field root driver is reused.

21.7.7. Companion contracts🔗

HexNumberFieldMathlib interprets selected roots in ℂ. For a checked fixed presentation, the reduced coordinates are ring-equivalent to the monic rational AdjoinRoot quotient. Their executable extended-GCD inverse is validated, and an opt-in Field instance preserves the existing computational operations and rational scalar action. Open the Hex.QAdjoin.QAdjoinField scope when Mathlib field notation and laws are wanted. Opening this scope makes that notation proof-bearing and noncomputable; executable code continues to use the unscoped operations.

def

Hex.AlgebraicRoot.toComplex (a : Hex.AlgebraicRoot) : ℂ
Hex.AlgebraicRoot.toComplex
  (a : Hex.AlgebraicRoot) : ℂ

The complex value selected by a factorization-lazy algebraic root.

def

Hex.QAdjoin.toComplex {p : Hex.ZPoly} {x : Hex.SimpleRoot p}
  (a : Hex.QAdjoin p x) (rep : Hex.RefinedIsolation p)
  (_h : Hex.SimpleRoot.mk rep = x) : ℂ
Hex.QAdjoin.toComplex {p : Hex.ZPoly}
  {x : Hex.SimpleRoot p}
  (a : Hex.QAdjoin p x)
  (rep : Hex.RefinedIsolation p)
  (_h : Hex.SimpleRoot.mk rep = x) : ℂ

Evaluate canonical fixed-field coordinates at their selected complex root. The representative and quotient equality are explicit inputs so this semantic map does not depend on an irreducibility proof.

def

Hex.QAdjoin.adjoinRootEquiv {p : Hex.ZPoly} {x : Hex.SimpleRoot p}
  [p.CheckedIrreducible] :
  Hex.QAdjoin p x ≃+* AdjoinRoot (Hex.QAdjoin.definingPolynomial p)
Hex.QAdjoin.adjoinRootEquiv
  {p : Hex.ZPoly} {x : Hex.SimpleRoot p}
  [p.CheckedIrreducible] :
  Hex.QAdjoin p x ≃+*
    AdjoinRoot
      (Hex.QAdjoin.definingPolynomial p)

Reduced executable coordinates are ring-equivalent to the monic rational AdjoinRoot presentation.

def

Hex.QAdjoin.embedding {p : Hex.ZPoly} {x : Hex.SimpleRoot p}
  [p.CheckedIrreducible] (rep : Hex.RefinedIsolation p)
  (h : Hex.SimpleRoot.mk rep = x) : Hex.QAdjoin p x →+* ℂ
Hex.QAdjoin.embedding {p : Hex.ZPoly}
  {x : Hex.SimpleRoot p}
  [p.CheckedIrreducible]
  (rep : Hex.RefinedIsolation p)
  (h : Hex.SimpleRoot.mk rep = x) :
  Hex.QAdjoin p x →+* ℂ

Evaluation at the selected root as an injective ring homomorphism.

theorem

Hex.AlgebraicRoot.exact_toComplex (a : Hex.AlgebraicRoot) :
  a.exact.toComplex = a.toComplex
Hex.AlgebraicRoot.exact_toComplex
  (a : Hex.AlgebraicRoot) :
  a.exact.toComplex = a.toComplex

The total canonicalization wrapper preserves the represented value.

theorem

Hex.AlgebraicPoly.contains_roots_iff (f : Hex.AlgebraicPoly) (z : ℂ) :
  f.roots.Contains z ↔ Polynomial.eval z f.toPolynomial = 0
Hex.AlgebraicPoly.contains_roots_iff
  (f : Hex.AlgebraicPoly) (z : ℂ) :
  f.roots.Contains z ↔
    Polynomial.eval z f.toPolynomial = 0

Semantic membership in the algebraic-coefficient output is exactly polynomial vanishing.

21.7.8. Cross-references🔗

HexPolyZ supplies the integer-polynomial presentation.
HexRoots supplies certified complex-root isolation and Hex.SimpleRoot.
HexResultant supplies the eliminants used by lazy arithmetic and fixed-field norm candidates.
HexMatrix and HexRowReduce supply exact span coordinates for fixed-field minimal polynomials.
HexNumberFieldTower builds successive extensions when one primitive presentation is not convenient.