def Hex.NumberTower.Norm.liftCoefficient (level : Level) (lower : List Level) (a : Array Rat) : DensePoly (DensePoly (Arithmetic.Coeff lower))

Interpret flattened current-tower coordinates as a polynomial in the top generator, with coefficients that are constant polynomials in X over the lower tower.

Equations

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

def Hex.NumberTower.Norm.definingOuter (level : Level) (lower : List Level) : DensePoly (DensePoly (Arithmetic.Coeff lower))

The newest level's monic defining polynomial in the elimination variable, with coefficients regarded as constant polynomials in X.

Equations

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

def Hex.NumberTower.Norm.shiftedOuter (level : Level) (lower : List Level) (f : Array (Array Rat)) (c : Int) : DensePoly (DensePoly (Arithmetic.Coeff lower))

Substitute X - cY into a polynomial over the current tower, presenting the result as a polynomial in Y over lower[X].

Equations

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

def Hex.NumberTower.Norm.quadratic (level : Level) (lower : List Level) (f : Array (Array Rat)) (c : Int) : Array (Array Rat)

Shift modulo a quadratic relation, keeping only the constant and linear generator coefficients. For Y² + bY + a, the norm is A² - bAB + aB².

Equations

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

def Hex.NumberTower.Norm.oneLevel (level : Level) (lower : List Level) (f : Array (Array Rat)) (c : Int) : Array (Array Rat)

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

Equations

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

def Hex.NumberTower.Norm.iterated (levels : List Level) : Array (Array Rat) → Array (Array Rat)

Eliminate every tower generator without shifting. This absolute norm is used to obtain root candidates for splitting; recursive Trager factorization continues to use oneLevel independently at each level.

Equations

• Hex.NumberTower.Norm.iterated [] x✝ = x✝
• Hex.NumberTower.Norm.iterated (level :: lower) x✝ = Hex.NumberTower.Norm.iterated lower (Hex.NumberTower.Norm.oneLevel level lower x✝ 0)

def Hex.NumberTower.Norm.derivative (lower : List Level) (f : DensePoly (Arithmetic.Coeff lower)) : DensePoly (Arithmetic.Coeff lower)

Formal derivative over a runtime-indexed lower tower.

Equations

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

def Hex.NumberTower.Norm.monic {lower : List Level} (f : DensePoly (Arithmetic.Coeff lower)) : DensePoly (Arithmetic.Coeff lower)

Monic normalization over the runtime-indexed lower tower.

Equations

• Hex.NumberTower.Norm.monic f = if f.isZero = true then 0 else Hex.DensePoly.scale f.leadingCoeff⁻¹ f

def Hex.NumberTower.Norm.isSquarefree (lower : List Level) (f : Array (Array Rat)) : Bool

Executable squarefreeness test over a checked lower tower. The rational base uses the certified modular trial before exact gcd fallback.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Norm.isSquarefree [] f = Hex.ZPoly.ratSquarefree (Hex.DensePoly.ofCoeffs (Array.map (fun (a : Array Rat) => a.getD 0 0) f))

def Hex.NumberTower.Norm.tragerShiftCount (d m : Nat) : Nat

Number of deterministic Trager shifts required for a top degree d and component degree m.

Equations

• Hex.NumberTower.Norm.tragerShiftCount d m = Hex.Nat.choose (d * m) 2 + 1

def Hex.NumberTower.Norm.signedShift (i : Nat) : Int

Deterministic signed enumeration 0, 1, -1, 2, -2, ....

Equations

• Hex.NumberTower.Norm.signedShift i = Hex.AlgebraicPoly.Common.signedShift i

def Hex.NumberTower.Norm.findSquarefreeShiftAux (level : Level) (lower : List Level) (f : Array (Array Rat)) (i : Nat) : Nat → Option (Int × Array (Array Rat))

Search successive signed shifts without materializing the remaining range.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Norm.findSquarefreeShiftAux level lower f i 0 = none

def Hex.NumberTower.Norm.findSquarefreeShift (level : Level) (lower : List Level) (f : Array (Array Rat)) : Option (Int × Array (Array Rat))

Search exactly the finite Trager collision bound and return the first shift whose one-level norm is squarefree over the lower tower.

Equations

• Hex.NumberTower.Norm.findSquarefreeShift level lower f = Hex.NumberTower.Norm.findSquarefreeShiftAux level lower f 0 (Hex.NumberTower.Norm.tragerShiftCount level.degree (f.size - 1))