theorem Hex.NumberTower.polynomial_map_list_prod {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (ps : List (Polynomial R)) : Polynomial.map f ps.prod = (List.map (fun (p : Polynomial R) => Polynomial.map f p) ps).prod

Mapping a ring homomorphism across a list of polynomials commutes with taking the product.

theorem Hex.NumberTower.rawPoly_nil_eq_zero_iff (f : Array (Array ℚ)) : Factor.rawPoly [] f = 0 ↔ Factor.toRatPoly f = 0

Over the empty tower the raw coordinate polynomial vanishes exactly when its rational reading does: Factor.rawPoly [] and Factor.toRatPoly present the same polynomial through the coefficient identification with ℚ.

theorem Hex.NumberTower.map_monic_rawPoly_nil (f : Array (Array ℚ)) : Polynomial.map LevelSemantics.coeffRatEquiv.toRingHom (HexPolyMathlib.toPolynomial (Norm.monic (Factor.rawPoly [] f))) = HexPolyMathlib.toPolynomial (have p := Factor.toRatPoly f; if p.isZero = true then 0 else DensePoly.scale p.leadingCoeff⁻¹ p)

Over the empty tower, monic normalisation commutes with the coefficient identification with ℚ: normalising Factor.rawPoly [] f and then reading coefficients rationally gives the leading-coefficient rescaling of Factor.toRatPoly f.

theorem Hex.NumberTower.rawFactorFoldl (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (factors : List (Array (Array ℚ))) (init : DensePoly (Arithmetic.Coeff levels)) : HexPolyMathlib.toPolynomial (List.foldl (fun (product : DensePoly (Arithmetic.Coeff levels)) (factor : Array (Array ℚ)) => product * Factor.rawPoly levels factor) init factors) = HexPolyMathlib.toPolynomial init * (List.map (fun (factor : Array (Array ℚ)) => HexPolyMathlib.toPolynomial (Factor.rawPoly levels factor)) factors).prod

The executable left fold multiplying raw tower factors interprets to the initial value times the product of the interpreted factors.

theorem Hex.NumberTower.ratFactorFoldl (factors : List (Array (Array ℚ))) (init : DensePoly ℚ) : HexPolyMathlib.toPolynomial (List.foldl (fun (product : DensePoly ℚ) (factor : Array (Array ℚ)) => product * Factor.toRatPoly factor) init factors) = HexPolyMathlib.toPolynomial init * (List.map (fun (factor : Array (Array ℚ)) => HexPolyMathlib.toPolynomial (Factor.toRatPoly factor)) factors).prod

Rational analogue of rawFactorFoldl: the executable left fold multiplying rational readings of factors interprets to the initial value times the product of the interpreted factors.

theorem Hex.NumberTower.factorSquarefree_product (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (f : Array (Array ℚ)) {factors : Array (Array (Array ℚ))} (hf : Factor.rawPoly levels f ≠ 0) (hresult : Factor.factorSquarefree? levels f = some factors) : have hinv := ⋯; (List.map (fun (factor : Array (Array ℚ)) => HexPolyMathlib.toPolynomial (Factor.rawPoly levels factor)) factors.toList).prod = HexPolyMathlib.toPolynomial (Norm.monic (Factor.rawPoly levels f))

Reconstruction for one squarefree component: the factors returned by Factor.factorSquarefree? multiply to the monic normalisation of the input, after interpretation over the tower coefficient field.

theorem Hex.NumberTower.gcd_prod_associated {K : Type u_1} [Field K] [DecidableEq K] (P : Polynomial K) (qs : List (Polynomial K)) : Squarefree qs.prod → Associated (gcd P qs.prod) (List.map (fun (q : Polynomial K) => gcd P q) qs).prod

The gcd of P with a squarefree product is associated to the product of the gcds with the individual factors: pairwise coprimality of the squarefree factors lets the gcd distribute over the product.

theorem Hex.NumberTower.prod_gcd_associated {K : Type u_1} [Field K] [DecidableEq K] (P : Polynomial K) (qs : List (Polynomial K)) (hsquarefree : Squarefree qs.prod) (hdiv : P ∣ qs.prod) : Associated (List.map (fun (q : Polynomial K) => gcd P q) qs).prod P

Trager's gcd recovery is complete: if P divides a squarefree product, the product of the gcds of P with the factors recovers P up to a unit.

theorem Hex.NumberTower.euclidean_gcd_associated_gcd {K : Type u_1} [Field K] [DecidableEq K] (a b : Polynomial K) : Associated (EuclideanDomain.gcd a b) (gcd a b)

The Euclidean-algorithm gcd and the normalised GCDMonoid gcd of two polynomials agree up to a unit.

theorem Hex.NumberTower.recover_product_associated (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (component : Array (Array ℚ)) (shift : ℤ) (lowerFactors : Array (Array (Array ℚ))) (hcomponentNe : Factor.rawPoly (level :: lower) component ≠ 0) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; have delta := Arithmetic.Coeff.ofData (level :: lower) #[↑shift] * Factor.topGenerator level lower; have shifted := Factor.rawPoly (level :: lower) (Factor.shiftTop level lower component shift); have lifted := fun (lowerFactor : Array (Array ℚ)) => Factor.rawPoly (level :: lower) (Factor.embedLower level lower lowerFactor); Associated ((Polynomial.taylor (-delta)) (List.map (fun (factor : Array (Array ℚ)) => HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) factor)) (Factor.recover level lower shift component lowerFactors).toList).prod) (List.map (fun (lowerFactor : Array (Array ℚ)) => EuclideanDomain.gcd (HexPolyMathlib.toPolynomial shifted) (HexPolyMathlib.toPolynomial (lifted lowerFactor))) lowerFactors.toList).prod

Shifting the product of the factors recovered by Factor.recover back by the shift delta gives, up to a unit, the product of the gcds of the shifted component with the lifted lower-tower factors. Lower factors whose gcd is constant contribute a unit and are exactly the ones the recovery loop discards.

theorem Hex.NumberTower.recover_product_monic (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (component : Array (Array ℚ)) (shift : ℤ) (lowerFactors : Array (Array (Array ℚ))) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; (∀ factor ∈ Factor.recover level lower shift component lowerFactors, Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) factor))) → (List.map (fun (factor : Array (Array ℚ)) => HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) factor)) (Factor.recover level lower shift component lowerFactors).toList).prod.Monic

When every recovered factor interprets to an irreducible polynomial, the product of the interpreted recovered factors is monic: each factor is a monic normalisation by construction.

theorem Hex.NumberTower.recover_product (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (component norm : Array (Array ℚ)) (shift : ℤ) (lowerFactors : Array (Array (Array ℚ))) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Factor.rawPoly (level :: lower) component ≠ 0 → Squarefree (HexPolyMathlib.toPolynomial (Factor.rawPoly lower norm)) → norm = Norm.oneLevel level lower component shift → (∀ lowerFactor ∈ lowerFactors, Factor.polyCoords (Factor.rawPoly lower lowerFactor) = lowerFactor) → (List.map (fun (lowerFactor : Array (Array ℚ)) => HexPolyMathlib.toPolynomial (Factor.rawPoly lower lowerFactor)) lowerFactors.toList).prod = HexPolyMathlib.toPolynomial (Norm.monic (Factor.rawPoly lower norm)) → (∀ factor ∈ Factor.recover level lower shift component lowerFactors, Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) factor))) → (List.map (fun (factor : Array (Array ℚ)) => HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) factor)) (Factor.recover level lower shift component lowerFactors).toList).prod = HexPolyMathlib.toPolynomial (Norm.monic (Factor.rawPoly (level :: lower) component))

Reconstruction across one Trager recovery step: given a squarefree one-level norm at the accepted shift and lower-tower factors that multiply to its monic normalisation, the recovered top-level factors multiply to the monic normalisation of the squarefree component itself.

theorem Hex.NumberTower.recover_singleton (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : LevelSemantics.DenoteInjective (level :: lower)) (component : Array (Array ℚ)) (shift : ℤ) (lowerFactors : Array (Array (Array ℚ))) : have hinv := ⋯; lowerFactors.size = 1 → 0 < (Norm.monic (Factor.rawPoly (level :: lower) component)).natDegree → (List.map (fun (factor : Array (Array ℚ)) => HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) factor)) (Factor.recover level lower shift component lowerFactors).toList).prod = HexPolyMathlib.toPolynomial (Norm.monic (Factor.rawPoly (level :: lower) component)) → Factor.recover level lower shift component lowerFactors = #[Factor.polyCoords (Norm.monic (Factor.rawPoly (level :: lower) component))]

With a singleton lower factor list, recovery either returns one canonical factor or nothing. A positive-degree reconstruction product rules out the empty result and identifies that factor exactly.

theorem Hex.NumberTower.normalizedRatFactorFoldl (factors : List ZPoly) (init : DensePoly ℚ) : HexPolyMathlib.toPolynomial (List.foldl (fun (product : DensePoly ℚ) (factor : ZPoly) => product * DensePoly.scale factor.toRatPoly.leadingCoeff⁻¹ factor.toRatPoly) init factors) = HexPolyMathlib.toPolynomial init * (List.map normalizedRatFactor factors).prod

The executable left fold multiplying monically rescaled rational readings of integer factors interprets to the initial value times the product of the corresponding normalizedRatFactors.

theorem Hex.NumberTower.factorRat_product (p : DensePoly ℚ) (hp : p ≠ 0) (hpMonic : (HexPolyMathlib.toPolynomial p).Monic) : have integer := ZPoly.ratPolyPrimitivePart p; have rawFactors := Array.flatMap (fun (entry : ZPoly × ℕ) => Array.replicate entry.2 entry.1) integer.factorize.factors; have factors := Array.map (fun (factor : ZPoly) => have q := factor.toRatPoly; have q := DensePoly.scale q.leadingCoeff⁻¹ q; Factor.ofRatPoly q) rawFactors; Array.foldl (fun (product : DensePoly ℚ) (factor : Array (Array ℚ)) => product * Factor.toRatPoly factor) 1 factors = p

Rational base case of reconstruction: the monically rescaled Berlekamp-Zassenhaus factors of the primitive part of a monic rational polynomial multiply back to the polynomial itself.

theorem Hex.NumberTower.gcd_derivative_size_le_one_of_separable (p : DensePoly ℚ) (hseparable : (HexPolyMathlib.toPolynomial p).Separable) : (p.gcd p.derivative).size ≤ 1

For a separable input the executable gcd with the derivative is constant, so the squarefreeness guard in the rational factorizer passes.

theorem Hex.NumberTower.factorRat_isSome (input : DensePoly ℚ) (hseparable : (HexPolyMathlib.toPolynomial input).Separable) : (Factor.factorRat? input).isSome = true

The rational base factorizer is total on the separable inputs supplied by Yun decomposition.