def Hex.NumberTower.Factor.rawPoly (levels : List Level) (f : Array (Array Rat)) : DensePoly (Arithmetic.Coeff levels)

Convert raw flattened coefficient arrays to a runtime-indexed tower polynomial.

Equations

• Hex.NumberTower.Factor.rawPoly levels f = Hex.DensePoly.ofCoeffs (Array.map (Hex.NumberTower.Arithmetic.Coeff.ofData levels) f)

def Hex.NumberTower.Factor.polyCoords {levels : List Level} (f : DensePoly (Arithmetic.Coeff levels)) : Array (Array Rat)

Extract flattened coefficient arrays from a runtime-indexed tower polynomial.

Equations

• Hex.NumberTower.Factor.polyCoords f = Array.map Hex.NumberTower.Arithmetic.Coeff.data f.toArray

def Hex.NumberTower.Factor.yunAux (levels : List Level) (w repeated : DensePoly (Arithmetic.Coeff levels)) (multiplicity fuel : Nat) (out : Array (Array (Array Rat) × Nat)) : Array (Array (Array Rat) × Nat)

Fuel-bounded Yun loop. Here w is the product of the factors whose multiplicity is still at least the current index, while repeated contains their remaining copies. Dividing w by their gcd emits the squarefree component of exactly that multiplicity.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Factor.yunAux levels w repeated multiplicity 0 out = out

def Hex.NumberTower.Factor.yunRaw (levels : List Level) (f : Array (Array Rat)) : Array (Array (Array Rat) × Nat)

Yun squarefree decomposition over raw tower coordinates. Zero and constants have no positive-degree components.

Equations

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

@[irreducible]

def Hex.NumberTower.Factor.polyPow {levels : List Level} (f : DensePoly (Arithmetic.Coeff levels)) (n : Nat) : DensePoly (Arithmetic.Coeff levels)

Polynomial power used by reconstruction checks, computed by repeated squaring so high multiplicities do not induce a linear multiplication chain.

Equations

• Hex.NumberTower.Factor.polyPow f n = if n = 0 then 1 else have half := Hex.NumberTower.Factor.polyPow f (n / 2); have square := half * half; if n % 2 = 0 then square else square * f

def Hex.NumberTower.Factor.yunProduct (levels : List Level) (components : Array (Array (Array Rat) × Nat)) : Array (Array Rat)

Reconstruct a monic polynomial from raw Yun components.

Equations

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

def Hex.NumberTower.Factor.yunMultiplicitiesIncrease (components : Array (Array (Array Rat) × Nat)) : Bool

Check that the emitted multiplicities are in strictly increasing order.

Equations

• Hex.NumberTower.Factor.yunMultiplicitiesIncrease components = decide (List.Pairwise (fun (a b : Array (Array Rat) × Nat) => a.snd < b.snd) components.toList)

def Hex.NumberTower.Factor.yunPairwiseCoprime (levels : List Level) (components : Array (Array (Array Rat) × Nat)) : Bool

Check that distinct Yun components are pairwise coprime.

Equations

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

def Hex.NumberTower.Factor.checkYun (levels : List Level) (f : Array (Array Rat)) (components : Array (Array (Array Rat) × Nat)) : Bool

Self-check a Yun decomposition: multiplicities are positive and strictly increasing, the monic squarefree components are pairwise coprime, and their powered product reconstructs the monic input. Polynomials of degree zero have the unique empty decomposition.

Equations

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

def Hex.NumberTower.Factor.toRatPoly (f : Array (Array Rat)) : DensePoly Rat

Recover the rational polynomial stored by base-tower raw coordinates.

Equations

• Hex.NumberTower.Factor.toRatPoly f = Hex.DensePoly.ofCoeffs (Array.map (fun (coefficient : Array Rat) => coefficient.getD 0 0) f)

def Hex.NumberTower.Factor.ofRatPoly (f : DensePoly Rat) : Array (Array Rat)

Convert a rational polynomial back to raw base-tower coordinates.

Equations

• Hex.NumberTower.Factor.ofRatPoly f = Array.map (fun (coefficient : Rat) => #[coefficient]) f.toArray

def Hex.NumberTower.Factor.factorRat? (input : DensePoly Rat) : Option (Array (Array (Array Rat)))

Complete factorization of a monic squarefree rational polynomial. The Berlekamp–Zassenhaus entries are expanded by multiplicity before their monic normalizations are checked against the input. The recursive caller admits only squarefree inputs, so the companion proves that this expansion contains one copy of each irreducible factor; expanding here also makes reconstruction independent of that semantic fact.

Equations

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

def Hex.NumberTower.Factor.topGenerator (level : Level) (lower : List Level) : Arithmetic.Coeff (level :: lower)

The newest generator as a runtime-indexed element. A linear level already lies in the lower field, so its generator is the negative constant term of its monic relation.

Equations

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

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

Substitute X - c*alpha in a current-level polynomial.

Equations

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

def Hex.NumberTower.Factor.embedLower (level : Level) (lower : List Level) (f : Array (Array Rat)) : Array (Array Rat)

Embed a lower-tail polynomial into the current level. Mixed-radix order places lower coordinates in the first top-generator block.

Equations

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

def Hex.NumberTower.Factor.recoveryGcd {levels : List Level} (p q : DensePoly (Arithmetic.Coeff levels)) : DensePoly (Arithmetic.Coeff levels)

Start recovery division with the monic shifted component when it has smaller degree than the lifted norm factor. The remaining Euclidean chain uses exactly the reference gcd's remaining fuel and remainder representative.

Equations

• Hex.NumberTower.Factor.recoveryGcd p q = if p.isZero = false ∧ p.size < q.size ∧ p.leadingCoeff = 1 then p.gcdAux (q.modArray p id) (p.size + q.size - 1) else p.gcd q

def Hex.NumberTower.Factor.recover (level : Level) (lower : List Level) (shift : Int) (component : Array (Array Rat)) (lowerFactors : Array (Array (Array Rat))) : Array (Array (Array Rat))

Recover current-level factors from irreducible lower factors of a squarefree Trager norm, then undo the selected generator shift.

Equations

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

def Hex.NumberTower.Factor.factorSquarefree? (levels : List Level) : Array (Array Rat) → Option (Array (Array (Array Rat)))

Recursive Trager factorization of one monic squarefree component. The recursion is structural in the tower height; every proper level performs one bounded one-level norm search and recurses only on the lower tail.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Factor.factorSquarefree? [] x✝ = Hex.NumberTower.Factor.factorRat? (Hex.NumberTower.Factor.toRatPoly x✝)

structure Hex.NumberTower.Factor.RawFactorization : Type

Runtime factorization payload before re-indexing coefficients by a public NumberTower.

• scalar : Array Rat

  The leading scalar's raw coordinates.

• factors : Array (Array (Array Rat) × Nat)

  Raw monic factors, canonically sorted, each with its multiplicity.

def Hex.NumberTower.Factor.ratListLess : List Rat → List Rat → Bool

Lexicographic order on rational lists.

Equations

• Hex.NumberTower.Factor.ratListLess [] [] = false
• Hex.NumberTower.Factor.ratListLess [] (head :: tail) = true
• Hex.NumberTower.Factor.ratListLess (head :: tail) [] = false
• Hex.NumberTower.Factor.ratListLess (a :: as) (b :: bs) = if a < b then true else if b < a then false else Hex.NumberTower.Factor.ratListLess as bs

def Hex.NumberTower.Factor.flattenPoly (f : Array (Array Rat)) : List Rat

Flatten polynomial coefficient coordinates for canonical sorting. Each coefficient carries its length, so the key remains injective even for malformed raw inputs whose coordinate blocks do not have the tower width.

Equations

• Hex.NumberTower.Factor.flattenPoly f = List.flatMap (fun (coefficient : Array Rat) => ↑coefficient.size :: coefficient.toList) f.toList

def Hex.NumberTower.Factor.factorLess (a b : Array (Array Rat)) : Bool

Canonical lexicographic factor order.

Equations

• Hex.NumberTower.Factor.factorLess a b = Hex.NumberTower.Factor.ratListLess (Hex.NumberTower.Factor.flattenPoly a) (Hex.NumberTower.Factor.flattenPoly b)

def Hex.NumberTower.Factor.insertFactor (factor : Array (Array Rat) × Nat) : List (Array (Array Rat) × Nat) → List (Array (Array Rat) × Nat)

Insert one factor into a canonically ordered factor list. Equal coordinate keys are combined by adding multiplicities.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Factor.insertFactor factor [] = [factor]

def Hex.NumberTower.Factor.canonicalFactors (factors : Array (Array (Array Rat) × Nat)) : Array (Array (Array Rat) × Nat)

Sort factors canonically and combine duplicate coordinate keys.

Equations

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

def Hex.NumberTower.Factor.factorsSorted (factors : Array (Array (Array Rat) × Nat)) : Bool

Check that every pair of factors is in strict canonical order. Strictness ensures each irreducible occurs once, with its multiplicity stored in the paired natural number.

Equations

• Hex.NumberTower.Factor.factorsSorted factors = decide (List.Pairwise (fun (a b : Array (Array Rat) × Nat) => Hex.NumberTower.Factor.factorLess a.fst b.fst = true) factors.toList)

def Hex.NumberTower.Factor.factorProduct (levels : List Level) (scalar : Array Rat) (factors : Array (Array (Array Rat) × Nat)) : Array (Array Rat)

Multiply a scalar and powered raw factor list.

Equations

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

def Hex.NumberTower.Factor.isIrreducible (levels : List Level) (f : Array (Array Rat)) : Bool

Executable recursive irreducibility checker for a monic squarefree raw tower polynomial. The rational base delegates to the integer-polynomial checker shared by rational factorization; proper towers accept exactly a singleton Trager reconstruction.

Equations

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

def Hex.NumberTower.Factor.appendComponent? (levels : List Level) (out : Array (Array (Array Rat) × Nat)) (component : Array (Array Rat) × Nat) : Option (Array (Array (Array Rat) × Nat))

Append all irreducible factors of one Yun component, carrying the Yun multiplicity into the accumulated factor list.

Equations

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

def Hex.NumberTower.Factor.check (levels : List Level) (f : Array (Array Rat)) (scalar : Array Rat) (factors : Array (Array (Array Rat) × Nat)) : Bool

Full executable raw factorization certificate check. At proper tower levels, “irreducible” means a piece the recursive Trager checker cannot split; the Mathlib companion supplies the semantic irreducibility theorem. Cheap reconstruction and canonical-order checks precede recursive replay.

Equations

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

def Hex.NumberTower.Factor.factorRaw? (levels : List Level) (f : Array (Array Rat)) : Option RawFactorization

Produce a canonical factorization candidate with checked Yun multiplicities and recursive Trager recovery. The public dependent constructor performs the one full executable certificate replay.

Equations

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