def Hex.NumberTower.Level.polynomial (level : Level) (lower : List Level) : Array (Array Rat)

The monic polynomial represented by a raw level, including its implicit leading coefficient.

Equations

• level.polynomial lower = level.defining.push (Hex.NumberTower.Arithmetic.fixedCoeffs (Hex.NumberTower.levelsDim lower) #[1])

def Hex.NumberTower.Level.RationalRelation (level : Level) (lower : List Level) : Prop

A rational-presentation level relation agrees with the monic rational associate of the stored absolute root's checked integer polynomial.

Equations

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

inductive Hex.NumberTower.Level.Certificate (level : Level) (lower : List Level) : Prop

Meaningful construction evidence for one level. The base constructor ties the relation directly to a checked irreducible integer presentation and its selected root. A relative constructor records successful execution of the recursive Trager irreducibility checker and the fixed-embedding zero check.

• rational {level : Level} {lower : List Level} (relation : level.RationalRelation lower) : level.Certificate lower
• relative {level : Level} {lower : List Level} (degree_gt_one : 1 < level.degree) (irreducible : Factor.isIrreducible lower (level.polynomial lower) = true) (embedding : RawEvaluation.vanishesAt? lower (level.polynomial lower) level.root = some true) : level.Certificate lower

def Hex.NumberTower.LevelsValid : List Level → Prop

Every top-first level has canonical coefficient widths relative to the tail beneath it and carries constructor-produced irreducibility and fixed- embedding evidence.

Equations

• Hex.NumberTower.LevelsValid [] = True
• Hex.NumberTower.LevelsValid (level :: lower) = (level.Structural (Hex.NumberTower.levelsDim lower) ∧ level.Certificate lower ∧ Hex.NumberTower.LevelsValid lower)

structure Hex.NumberTower : Type

A validated, fixed-embedding tower of successive algebraic extensions of Rat. Construction is sealed, and checked smart constructors are the only API for extending towers.

• levels : Array Level

  The extension levels, stored top-first.

• valid : LevelsValid self.levels.toList

  Every level passed its structural, irreducibility, and fixed-embedding checks at construction time.

def Hex.NumberTower.rat : NumberTower

The rational tower, with no algebraic extension levels.

Equations

• Hex.NumberTower.rat = { levels := #[], valid := True.intro }

@[simp]

theorem Hex.NumberTower.rat_levels : rat.levels.toList = []

The rational tower has no proper extension levels.

def Hex.NumberTower.dim (T : NumberTower) : Nat

Absolute dimension over Rat.

Equations

• T.dim = Hex.NumberTower.levelsDim T.levels.toList

def Hex.NumberTower.Internal.extend? (T : NumberTower) (level : Level) : Option NumberTower

Internal checked boundary for adjoining one proper extension level. Raw level arrays are accepted only after structural, recursive irreducibility, and fixed-embedding checks all succeed.

Equations

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

theorem Hex.NumberTower.Internal.extend?_isSome (T : NumberTower) (level : Level) (hdegree : 1 < level.degree) (hstruct : level.structuralCheck T.dim = true) (hirred : Factor.isIrreducible T.levels.toList (level.polynomial T.levels.toList) = true) (hembed : RawEvaluation.vanishesAt? T.levels.toList (level.polynomial T.levels.toList) level.root = some true) : (extend? T level).isSome = true

The internal extension constructor succeeds once all of its explicit checks have been discharged.

theorem Hex.NumberTower.Internal.extend?_levels (T : NumberTower) (level : Level) {U : NumberTower} (h : extend? T level = some U) : U.levels.toList = level :: T.levels.toList

A successful checked extension prepends exactly the admitted level.

theorem Hex.NumberTower.Internal.extend?_dim (T : NumberTower) (level : Level) {U : NumberTower} (h : extend? T level = some U) : U.dim = level.degree * T.dim

A successful checked extension multiplies the lower tower dimension by the admitted relative degree.

def Hex.NumberTower.height (T : NumberTower) : Nat

Number of proper algebraic extension levels.

Equations

• T.height = T.levels.size

structure Hex.NumberTower.Elem (T : NumberTower) : Type

Canonical mixed-radix rational coordinates in a fixed tower.

• data : Array Rat

  The flattened mixed-radix rational coordinates.

• size_eq : self.data.size = T.dim

  The coordinate array has exactly the tower's dimension.

def Hex.NumberTower.normalizeCoeffs (T : NumberTower) (coefficients : Array Rat) : Array Rat

Normalize an arbitrary coordinate array to the tower dimension by truncating excess coordinates and padding missing coordinates with zero.

Equations

• T.normalizeCoeffs coefficients = (Vector.ofFn fun (i : Fin T.dim) => coefficients.getD (↑i) 0).toArray

theorem Hex.NumberTower.normalizeCoeffs_eq_self (T : NumberTower) (coefficients : Array Rat) (hsize : coefficients.size = T.dim) : T.normalizeCoeffs coefficients = coefficients

Normalization fixes an array that already has the tower width.

def Hex.NumberTower.ofCoeffs (T : NumberTower) (coefficients : Array Rat) : T.Elem

Construct the unique fixed-width element represented by a raw coordinate array.

Equations

• T.ofCoeffs coefficients = { data := T.normalizeCoeffs coefficients, size_eq := ⋯ }

def Hex.NumberTower.Internal.ofCoeffs (T : NumberTower) (coefficients : Array Rat) (hsize : coefficients.size = T.dim) : T.Elem

Construct an element from coordinates whose exact tower width is already known. Arithmetic kernels use this internal boundary to avoid copying a fresh fixed-width result through normalizeCoeffs a second time.

Equations

• Hex.NumberTower.Internal.ofCoeffs T coefficients hsize = { data := coefficients, size_eq := hsize }

def Hex.NumberTower.coeffs {T : NumberTower} (a : T.Elem) : Array Rat

Canonical flattened rational coordinates.

Equations

• Hex.NumberTower.coeffs a = a.data

@[simp]

theorem Hex.NumberTower.Internal.coeffs_ofCoeffs (T : NumberTower) (coefficients : Array Rat) (hsize : coefficients.size = T.dim) : coeffs (ofCoeffs T coefficients hsize) = coefficients

Exact-width construction exposes its supplied coordinates unchanged.

@[simp]

theorem Hex.NumberTower.coeffs_size {T : NumberTower} (a : T.Elem) : (coeffs a).size = T.dim

Every element exposes exactly the tower's mixed-radix width.

@[simp]

theorem Hex.NumberTower.coeffs_ofCoeffs (T : NumberTower) (coefficients : Array Rat) : coeffs (T.ofCoeffs coefficients) = T.normalizeCoeffs coefficients

Reading a freshly normalized element returns its normalized coordinates.

theorem Hex.NumberTower.Elem.ext {T : NumberTower} {a b : T.Elem} (h : coeffs a = coeffs b) : a = b

Equality is exact coordinate equality inside a fixed tower.

theorem Hex.NumberTower.Elem.ext_iff {T : NumberTower} {a b : T.Elem} : a = b ↔ coeffs a = coeffs b

Equality is exact coordinate equality inside a fixed tower; the generated iff form of Hex.NumberTower.Elem.ext.

@[instance_reducible]

instance Hex.NumberTower.instDecidableEqElem {T : NumberTower} : DecidableEq T.Elem

Equations

• Hex.NumberTower.instDecidableEqElem a b = match decEq (Hex.NumberTower.coeffs a).toList (Hex.NumberTower.coeffs b).toList with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

def Hex.NumberTower.ofRat (T : NumberTower) (q : Rat) : T.Elem

Embed a rational number into the constant mixed-radix coordinate.

Equations

• T.ofRat q = T.ofCoeffs #[q]

theorem Hex.NumberTower.ofRat_eq_ofCoeffs (T : NumberTower) (q : Rat) : T.ofRat q = T.ofCoeffs #[q]

Rational embedding is the singleton-coordinate constructor.

structure Hex.NumberTower.Extension (T : NumberTower) : Type

A dependent extension result carries the canonical lower-field embedding, the new generator, and its selected absolute algebraic root.

• tower : NumberTower

  The extended tower.

• embed : T.Elem → self.tower.Elem

  The canonical embedding of the lower field.

• gen : self.tower.Elem

  The adjoined generator as an element of the extended tower.

• root : AlgebraicRoot

  The absolute algebraic root selected for the generator.

def Hex.NumberTower.positiveAssociate (p : ZPoly) : ZPoly

Primitive associate with positive leading coefficient. This leaves every complex root fixed and only normalizes a possible global sign.

Equations

• Hex.NumberTower.positiveAssociate p = p.normalizePrimitiveSign

theorem Hex.NumberTower.positiveAssociate_primitive (p : ZPoly) (checked : p.CheckedIrreducible) : (positiveAssociate p).Primitive

Checked integer irreducibility forces primitive content.

theorem Hex.NumberTower.positiveAssociate_lc_pos (p : ZPoly) (checked : p.CheckedIrreducible) : 0 < DensePoly.leadingCoeff (positiveAssociate p)

A checked positive-degree polynomial's positive associate has positive leading coefficient.

theorem Hex.NumberTower.positiveAssociate_degree_pos (p : ZPoly) (checked : p.CheckedIrreducible) : 0 < DensePoly.natDegree (positiveAssociate p)

Sign association preserves positive degree.

theorem Hex.NumberTower.positiveAssociate_simple (p : ZPoly) (hsf : HasOnlySimpleRoots p) : HasOnlySimpleRoots (positiveAssociate p)

Sign association preserves the executable simple-root certificate.

theorem Hex.NumberTower.mahlerPrec_positiveAssociate (p : ZPoly) : mahlerPrec (positiveAssociate p) = mahlerPrec p

Global sign normalization preserves the Mahler refinement precision.

def Hex.NumberTower.RefinedIsolation.positiveAssociate {p : ZPoly} (rep : RefinedIsolation p) : RefinedIsolation (NumberTower.positiveAssociate p)

Transport a refined isolation across global sign normalization.

Equations

• Hex.NumberTower.RefinedIsolation.positiveAssociate rep = ⟨{ square := rep.val.square, witness := rep.val.witness.normalize }, ⋯⟩

def Hex.NumberTower.ofQAdjoin {p : ZPoly} {x : SimpleRoot p} [checked : p.CheckedIrreducible] (hsf : HasOnlySimpleRoots p) (rep : RefinedIsolation p) (_h : SimpleRoot.mk rep = x) : 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.

Equations

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