21.8. HexNumberFieldTower: successive algebraic extensions🔗

21.8.1. Introduction🔗

HexNumberFieldTower performs exact arithmetic, factorization, adjoining, and splitting in a sequence of relative algebraic extensions.

21.8.2. Validated towers and coordinates🔗

HexNumberFieldTower represents a fixed embedding of a successive extension ℚ(α₁,…,αₙ). Levels are stored newest first; element coordinates use the mixed-radix order in which the oldest generator varies fastest. Constructors validate coefficient widths, relative irreducibility, and vanishing at the chosen absolute root before a level enters a public tower.

def

Hex.NumberTower.ofQAdjoin {p : Hex.ZPoly} {x : Hex.SimpleRoot p}
  [checked : p.CheckedIrreducible] (hsf : Hex.HasOnlySimpleRoots p)
  (rep : Hex.RefinedIsolation p) (_h : Hex.SimpleRoot.mk rep = x) :
  Hex.NumberTower.rat.Extension
Hex.NumberTower.ofQAdjoin {p : Hex.ZPoly}
  {x : Hex.SimpleRoot p}
  [checked : p.CheckedIrreducible]
  (hsf : Hex.HasOnlySimpleRoots p)
  (rep : Hex.RefinedIsolation p)
  (_h : Hex.SimpleRoot.mk rep = x) :
  Hex.NumberTower.rat.Extension

Build a one-level tower for a checked rational presentation. The level relation is the monic rational associate of p; its absolute generator uses the supplied isolation, transported only across a possible global sign.

The rational base tower is useful on its own and illustrates the coordinate normalization and total arithmetic conventions:

open Hex Hex.NumberTower

#guard rat.dim = 1
#guard coeffs (ofRat rat 7 / ofRat rat 3) = #[7 / 3]
#guard coeffs ((0 : Elem rat)⁻¹) = #[0]

21.8.3. Factorization by relative norms🔗

Hex.NumberTower.factor? performs Yun decomposition and then recursively applies Trager's algorithm one level at a time. At K(α)/K, it searches a deterministic finite list of integer shifts for a squarefree relative norm, factors that norm over K, and recovers the factors over K(α) by gcd. It does not replace this step with an absolute norm, which would duplicate factors defined over an intermediate subfield. The rational base case delegates to the HexBerlekampZassenhaus integer factorizer.

def

Hex.NumberTower.Norm.oneLevel (level : Hex.NumberTower.Level)
  (lower : List Hex.NumberTower.Level) (f : Array (Array ℚ)) (c : ℤ) :
  Array (Array ℚ)
Hex.NumberTower.Norm.oneLevel
  (level : Hex.NumberTower.Level)
  (lower : List Hex.NumberTower.Level)
  (f : Array (Array ℚ)) (c : ℤ) :
  Array (Array ℚ)

One Trager norm step. Input coefficients are flattened over level :: lower; output coefficients are flattened over lower.

def

Hex.NumberTower.factor? (T : Hex.NumberTower) (f : T.Poly) :
  Option (T.Factorization f)
Hex.NumberTower.factor?
  (T : Hex.NumberTower) (f : T.Poly) :
  Option (T.Factorization f)

Complete irreducible factorization with multiplicity.

The returned payload keeps the scalar separate and records each distinct factor once with a positive multiplicity.

The following example constructs ℚ(√2) and factors X² - 2 there; the two linear factors correspond to the already-present roots ±√2.

open Hex Hex.NumberTower

namespace HexNumberFieldTowerChapter

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! 🐙⟩
    if hsimple : HasOnlySimpleRoots sqrtTwoPoly then
      let extension := ofQAdjoin (x := sqrtTwoRoot)
        hsimple sqrtTwoRep rfl
      let f : Poly extension.tower :=
        DensePoly.ofCoeffs
          #[ofRat extension.tower (-2), 0, 1]
      match factor? extension.tower f with
      | some result =>
          result.factors.size = 2 &&
            result.factors.all fun entry =>
              entry.1.degree? = some 1 && entry.2 = 1
      | none => false
    else
      false
  else
    false

end HexNumberFieldTowerChapter

21.8.4. Adjoining and splitting🔗

Adjoining selects the unique relative factor that contains the requested absolute algebraic root under the tower's fixed embedding. If that factor is linear, the root was already present and the result is an identity extension.

def

Hex.NumberTower.adjoin? (T : Hex.NumberTower)
  (candidate : Hex.AlgebraicRoot) : Option T.Extension
Hex.NumberTower.adjoin?
  (T : Hex.NumberTower)
  (candidate : Hex.AlgebraicRoot) :
  Option T.Extension

Adjoin the specified absolute algebraic root. A selected linear factor produces the identity extension; a nonlinear factor is admitted only through Hex.NumberTower.Internal.extend?, which reruns structural, relative-irreducibility, and fixed- embedding checks before constructing the new carrier index.

Splitting alternates factorization and genuine adjoining steps until every factor is linear. The zero polynomial uses .all; a nonzero constant returns an empty finite root array.

def

Hex.NumberTower.split? (T : Hex.NumberTower) (f : T.Poly) :
  Option (T.Splitting f)
Hex.NumberTower.split?
  (T : Hex.NumberTower) (f : T.Poly) :
  Option (T.Splitting f)

Construct an extension in which the input polynomial splits into linear factors, retaining multiplicities from checked factorization.

21.8.5. Flattening to one primitive element🔗

Hex.NumberTower.flatten? replaces a tower by one canonical Hex.QAdjoin presentation. It combines the fixed generators in deterministic signed-shift order. A direct full-degree search and validated linear-gcd recovery form the fast path. The total fallback retains a bounded maximum-degree primitive candidate and recovers the old generators by exact trace pairing. It then checks direct-evaluation coordinate maps, a tower-basis round trip, and the primitive polynomial relation before returning maps. The Mathlib companion proves that this checked operation returns some for every valid tower.

def

Hex.NumberTower.flatten? (T : Hex.NumberTower) : Option T.Flattening
Hex.NumberTower.flatten?
  (T : Hex.NumberTower) :
  Option T.Flattening

Replace a checked tower by one canonical primitive-element presentation. The result is returned only after exact generator recovery, a tower-basis round trip, and the primitive polynomial relation succeed.

21.8.6. Companion contracts🔗

HexNumberFieldTowerMathlib interprets mixed-radix coordinates in the stored complex embedding, states the arithmetic and relative-resultant correspondence, and characterizes complete factorization, adjoining, splitting, and flattening.

def

Hex.NumberTower.toComplex (T : Hex.NumberTower) (a : T.Elem) : ℂ
Hex.NumberTower.toComplex
  (T : Hex.NumberTower) (a : T.Elem) : ℂ

The complex value of a tower element. The fallback is unreachable by Hex.NumberTower.eval?_isSome.

theorem

Hex.NumberTower.factor?_sound (T : Hex.NumberTower) (f : T.Poly)
  {r : T.Factorization f} (h : T.factor? f = some r) : r.Sound
Hex.NumberTower.factor?_sound
  (T : Hex.NumberTower) (f : T.Poly)
  {r : T.Factorization f}
  (h : T.factor? f = some r) : r.Sound

Every returned Trager factorization satisfies reconstruction, multiplicity, irreducibility, uniqueness, and ordering.

theorem

Hex.NumberTower.adjoin?_sound (T : Hex.NumberTower)
  (candidate : Hex.AlgebraicRoot) {E : T.Extension}
  (h : T.adjoin? candidate = some E) :
  Hex.NumberTower.Extension.Sound candidate E
Hex.NumberTower.adjoin?_sound
  (T : Hex.NumberTower)
  (candidate : Hex.AlgebraicRoot)
  {E : T.Extension}
  (h : T.adjoin? candidate = some E) :
  Hex.NumberTower.Extension.Sound
    candidate E

Every returned adjoining payload satisfies the fixed-embedding, generation, and identity-extension contracts.

theorem

Hex.NumberTower.split?_sound (T : Hex.NumberTower) (f : T.Poly)
  {S : T.Splitting f} (h : T.split? f = some S) : S.Sound
Hex.NumberTower.split?_sound
  (T : Hex.NumberTower) (f : T.Poly)
  {S : T.Splitting f}
  (h : T.split? f = some S) : S.Sound

Every returned split payload reconstructs the input and generates the result extension from the listed roots.

theorem

Hex.NumberTower.flatten?_sound (T : Hex.NumberTower) {F : T.Flattening}
  (h : T.flatten? = some F) : F.Sound
Hex.NumberTower.flatten?_sound
  (T : Hex.NumberTower) {F : T.Flattening}
  (h : T.flatten? = some F) : F.Sound

Every returned primitive presentation has inverse coordinate maps, preserves arithmetic, and commutes with the fixed complex embeddings.

21.8.7. Cross-references🔗

HexNumberField supplies selected algebraic roots, canonical exactification, and the one-generator target of flattening.
HexResultant supplies one-level relative elimination.
Factor tactics describes the HexBerlekampZassenhaus integer factorizer used at the rational base case.