theorem Hex.NumberTower.factorSquarefree_isSome (levels : List Level) (_hvalid : LevelsValid levels) (_hinjective : LevelSemantics.DenoteInjective levels) (f : Array (Array ℚ)) : Norm.isSquarefree levels f = true → 0 < (Factor.rawPoly levels f).natDegree → (Factor.factorSquarefree? levels f).isSome = true

Totality of the squarefree-component factorizer: on a certified squarefree nonconstant input the bounded shift search and every recursive call succeed, so Factor.factorSquarefree? returns a result.

theorem Hex.NumberTower.factorRaw_isSome (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (f : Array (Array ℚ)) : (Factor.factorRaw? levels f).isSome = true

The complete raw Yun/Trager factorization pipeline cannot fail when coefficient denotation is injective.

theorem Hex.NumberTower.isIrreducible_nil_iff (f : Array (Array ℚ)) : Factor.isIrreducible [] f = true ↔ (Factor.rawPoly [] f).leadingCoeff = 1 ∧ Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly [] f))

Over the empty tower the executable irreducibility checker accepts exactly the monic inputs whose interpretation is irreducible.

theorem Hex.NumberTower.isIrreducible_iff_of_injective (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (f : Array (Array ℚ)) : have hinv := ⋯; Factor.isIrreducible levels f = true ↔ (Factor.rawPoly levels f).leadingCoeff = 1 ∧ Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly levels f))

With coefficient-denotation injectivity supplied explicitly, the recursive Boolean checker is exactly monic polynomial irreducibility. This generic form breaks the logical cycle used when validating the tower itself.

theorem Hex.NumberTower.factorRaw_check (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (f : Array (Array ℚ)) (hcanonical : Factor.polyCoords (Factor.rawPoly levels f) = f) {raw : Factor.RawFactorization} (hresult : Factor.factorRaw? levels f = some raw) : Factor.check levels f raw.scalar raw.factors = true

Every raw candidate produced by the complete Yun/Trager pipeline passes the executable certificate replay, provided the input coordinate array is in the canonical image of rawPoly.

theorem Hex.NumberTower.denoteInjective_of_valid (levels : List Level) : LevelsValid levels → LevelSemantics.DenoteInjective levels

Structural validity plus the recursive checker certificates imply injectivity of raw coefficient denotation at every tower depth.