theorem Hex.NumberTower.factorSquarefree_mem_sound (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (f : Array (Array ℚ)) {factors : Array (Array (Array ℚ))} : Factor.factorSquarefree? levels f = some factors → have hinv := ⋯; ∀ factor ∈ factors, Factor.polyCoords (Factor.rawPoly levels factor) = factor ∧ Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly levels factor))

Soundness of the squarefree-component factorizer at every tower height: each returned factor is a canonical coordinate array interpreting to an irreducible polynomial, by induction through the recursive one-level Trager step with the Berlekamp-Zassenhaus base case.