30.3. Factoring over ℚ(√2)🔗

X⁴ − 10X² + 1 is irreducible over ℚ: it is the minimal polynomial of √2 + √3. Over ℚ(√2) it splits into two quadratics, because (X² − 1)² − 8X² = X⁴ − 10X² + 1 and 8 = (2√2)². The tower's factorization finds exactly those two factors, with the scalar 1 kept separate:

def quartic : Poly T2 :=
  liftZPoly T2 #p[1, 0, -10, 0, 1]
def gPlus : Poly T2 := #p[-1, (2 : Rat) • r2, 1]
def gMinus : Poly T2 := #p[-1, (-2 : Rat) • r2, 1]

#guard gPlus * gMinus = quartic

-- A factorization pairs each factor with its multiplicity.
#guard
  let F := factor T2 quartic
  coeffs F.scalar = #[1, 0] &&
    F.factors.all (fun (_, m) => m = 1) &&
    F.factors.map (fun (g, _) => g) = #[gMinus, gPlus]

At each level K(α)/K the method searches a fixed list of integer shifts for a squarefree relative norm, factors that norm over K, and recovers the factors over K(α) by gcd; the base case over ℚ is the integer factorizer.

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.