theorem Hex.NumberTower.rawPoly_polyCoords (levels : List Level) (f : DensePoly (Arithmetic.Coeff levels)) : Factor.rawPoly levels (Factor.polyCoords f) = f

Rebuilding a raw dense polynomial from its flattened coordinate arrays is the identity: Factor.polyCoords is a section of Factor.rawPoly.

theorem Hex.NumberTower.rawPoly_shiftTop (level : Level) (lower : List Level) (f : Array (Array ℚ)) (c : ℤ) : Factor.rawPoly (level :: lower) (Factor.shiftTop level lower f c) = (Factor.rawPoly (level :: lower) f).compose (DensePoly.ofCoeffs #[-(Arithmetic.Coeff.ofData (level :: lower) #[↑c] * Factor.topGenerator level lower), 1])

The executable top-generator shift is composition with the affine polynomial X - c * α over the extended coefficient field.

theorem Hex.NumberTower.polyCoords_rawPoly_shiftTop (level : Level) (lower : List Level) (f : Array (Array ℚ)) (c : ℤ) : Factor.polyCoords (Factor.rawPoly (level :: lower) (Factor.shiftTop level lower f c)) = Factor.shiftTop level lower f c

Shifted coordinate arrays are already canonical: rebuilding and re-flattening a Factor.shiftTop output returns it unchanged.

theorem Hex.NumberTower.rawPoly_embedLower (level : Level) (lower : List Level) (f : Array (Array ℚ)) : Factor.rawPoly (level :: lower) (Factor.embedLower level lower f) = DensePoly.ofCoeffs (Array.map (fun (coefficient : Array ℚ) => Arithmetic.Coeff.ofData (level :: lower) coefficient) f)

Rebuilding an embedLower output reads its coefficients through the canonical coordinate injection into the extended tower.

theorem Hex.NumberTower.ofData_lower_eq_lowerHom (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (a : Arithmetic.Coeff lower) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Arithmetic.Coeff.ofData (level :: lower) a.data = (Norm.lowerHom level lower hvalid hinjectiveTop) a

Zero-padding lower-tower coordinate data into the extended tower agrees with the bundled lower-coefficient embedding Norm.lowerHom.

theorem Hex.NumberTower.rawPoly_embedLower_polyCoords (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (q : DensePoly (Arithmetic.Coeff lower)) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Factor.rawPoly (level :: lower) (Factor.embedLower level lower (Factor.polyCoords q)) = HexPolyMathlib.ofPolynomial (Polynomial.map (Norm.lowerHom level lower hvalid hinjectiveTop) (HexPolyMathlib.toPolynomial q))

Lifting a lower-tower polynomial by embedLower is, semantically, coefficientwise mapping through Norm.lowerHom.

theorem Hex.NumberTower.toPolynomial_affine {K : Type u_1} [Field K] [DecidableEq K] (delta : K) : HexPolyMathlib.toPolynomial (DensePoly.ofCoeffs #[-delta, 1]) = Polynomial.X - Polynomial.C delta

The two-coefficient array #[-delta, 1] interprets to the affine polynomial X - C delta.

theorem Hex.NumberTower.toPolynomial_shiftTop (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : Array (Array ℚ)) (c : ℤ) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; have delta := Arithmetic.Coeff.ofData (level :: lower) #[↑c] * Factor.topGenerator level lower; HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) (Factor.shiftTop level lower f c)) = (Polynomial.taylor (-delta)) (HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) f))

Semantic polynomial translation performed by the executable top-level shift.

theorem Hex.NumberTower.shiftDelta_neg (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (c : ℤ) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; have deltaNeg := Arithmetic.Coeff.ofData (level :: lower) #[-↑c] * Factor.topGenerator level lower; have delta := Arithmetic.Coeff.ofData (level :: lower) #[↑c] * Factor.topGenerator level lower; -deltaNeg = delta

Negating the integer shift negates the shift delta c * α, so opposite shifts translate by opposite amounts.

theorem Hex.NumberTower.irreducible_shiftTop_iff (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : Array (Array ℚ)) (c : ℤ) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) (Factor.shiftTop level lower f c))) ↔ Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) f))

Shifting by the top generator preserves irreducibility: translation by a fixed element is a ring automorphism of the polynomial ring.

theorem Hex.NumberTower.ofData_zero_eq_zero (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) : Arithmetic.Coeff.ofData levels #[0] = 0

The canonical coordinate representative of rational zero is the coefficient-field zero.

theorem Hex.NumberTower.rawPoly_shiftTop_zero (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : DensePoly (Arithmetic.Coeff (level :: lower))) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Factor.rawPoly (level :: lower) (Factor.shiftTop level lower (Factor.polyCoords f) 0) = f

The zero shift is the identity on rebuilt polynomials.

theorem Hex.NumberTower.toPolynomial_shiftTop_zero (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : Array (Array ℚ)) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) (Factor.shiftTop level lower f 0)) = HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) f)

The zero shift leaves the represented polynomial unchanged.

def Hex.NumberTower.tragerNorm (level : Level) (lower : List Level) (f : DensePoly (Arithmetic.Coeff (level :: lower))) : DensePoly (Arithmetic.Coeff lower)

The lower-field polynomial produced by one unshifted Trager elimination.

Equations

• Hex.NumberTower.tragerNorm level lower f = Hex.NumberTower.Factor.rawPoly lower (Hex.NumberTower.Norm.oneLevel level lower (Hex.NumberTower.Factor.polyCoords f) 0)

theorem Hex.NumberTower.tragerNorm_shiftTop (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : Array (Array ℚ)) (c : ℤ) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; tragerNorm level lower (Factor.rawPoly (level :: lower) (Factor.shiftTop level lower f c)) = Factor.rawPoly lower (Norm.oneLevel level lower f c)

Norming after an executable shift agrees with the shifted one-level resultant Norm.oneLevel … c, identifying the two routes to the shifted Trager norm.

theorem Hex.NumberTower.tragerNorm_mul (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (a b : DensePoly (Arithmetic.Coeff (level :: lower))) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; tragerNorm level lower (a * b) = tragerNorm level lower a * tragerNorm level lower b

The one-level Trager norm is multiplicative.

theorem Hex.NumberTower.tragerNorm_lift (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (q : DensePoly (Arithmetic.Coeff lower)) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; have lifted := HexPolyMathlib.ofPolynomial (Polynomial.map (Norm.lowerHom level lower hvalid hinjectiveTop) (HexPolyMathlib.toPolynomial q)); HexPolyMathlib.toPolynomial (tragerNorm level lower lifted) = HexPolyMathlib.toPolynomial q ^ level.degree

The norm of a polynomial lifted from the lower tower is its level.degree-th power: every conjugate of the top generator contributes the same factor.

theorem Hex.NumberTower.tragerNorm_dvd (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) {a b : DensePoly (Arithmetic.Coeff (level :: lower))} : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; HexPolyMathlib.toPolynomial a ∣ HexPolyMathlib.toPolynomial b → HexPolyMathlib.toPolynomial (tragerNorm level lower a) ∣ HexPolyMathlib.toPolynomial (tragerNorm level lower b)

The one-level Trager norm preserves divisibility of interpreted polynomials.

theorem Hex.NumberTower.tragerNorm_not_isUnit (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : DensePoly (Arithmetic.Coeff (level :: lower))) (hdegree : 0 < f.natDegree) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; ¬IsUnit (HexPolyMathlib.toPolynomial (tragerNorm level lower f))

The Trager norm of a nonconstant polynomial is nonconstant: a unit norm would force the input itself to be a unit.

theorem Hex.NumberTower.toPolynomial_monic_associated (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f : DensePoly (Arithmetic.Coeff levels)) (hf : f ≠ 0) : Associated (HexPolyMathlib.toPolynomial (Norm.monic f)) (HexPolyMathlib.toPolynomial f)

Monic normalisation only rescales by a unit: the interpretation of Norm.monic f is associated to the interpretation of f.

theorem Hex.NumberTower.natDegree_monic (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f : DensePoly (Arithmetic.Coeff levels)) : (Norm.monic f).natDegree = f.natDegree

Monic normalisation preserves the degree, including at zero.

theorem Hex.NumberTower.toPolynomial_monic_monic (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f : DensePoly (Arithmetic.Coeff levels)) (hf : f ≠ 0) : (HexPolyMathlib.toPolynomial (Norm.monic f)).Monic

The monic normalisation of a nonzero executable polynomial interprets to a monic polynomial.

theorem Hex.NumberTower.monic_eq_self (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f : DensePoly (Arithmetic.Coeff levels)) : (HexPolyMathlib.toPolynomial f).Monic → Norm.monic f = f

Monic normalisation fixes polynomials that already interpret to monic polynomials.

theorem Hex.NumberTower.not_two_nonunits_of_squarefree_primePower {K : Type u_1} [Field K] {N q a b : Polynomial K} {d : ℕ} (hN : Squarefree N) (hq : Irreducible q) (hNdiv : a * b ∣ N) (hqdiv : a * b ∣ q ^ d) (haUnit : ¬IsUnit a) (hbUnit : ¬IsUnit b) : False

Core counting argument for gcd recovery: a product of two nonunits cannot simultaneously divide a squarefree polynomial and a power of one irreducible, since both its irreducible factors would collapse onto that irreducible and square it inside the squarefree divisor.

theorem Hex.NumberTower.recoveredCommon_irreducible (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (P : DensePoly (Arithmetic.Coeff (level :: lower))) (q : DensePoly (Arithmetic.Coeff lower)) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; have lifted := Factor.rawPoly (level :: lower) (Factor.embedLower level lower (Factor.polyCoords q)); have common := Norm.monic (P.gcd lifted); Squarefree (HexPolyMathlib.toPolynomial (tragerNorm level lower P)) → Irreducible (HexPolyMathlib.toPolynomial q) → 0 < common.natDegree → Irreducible (HexPolyMathlib.toPolynomial common)

Irreducibility of one recovered gcd: when the Trager norm of P is squarefree and q is an irreducible lower factor, any nonconstant monic gcd of P with the lift of q is irreducible, because its norm divides both the squarefree norm of P and the prime power q ^ level.degree.

theorem Hex.NumberTower.recoveredFactor_irreducible (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (component lowerFactor : Array (Array ℚ)) (shift : ℤ) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; have shifted := Factor.rawPoly (level :: lower) (Factor.shiftTop level lower component shift); have q := Factor.rawPoly lower lowerFactor; have lifted := Factor.rawPoly (level :: lower) (Factor.embedLower level lower lowerFactor); have common := Norm.monic (shifted.gcd lifted); have unshifted := Factor.rawPoly (level :: lower) (Factor.shiftTop level lower (Factor.polyCoords common) (-shift)); have result := Norm.monic unshifted; Squarefree (HexPolyMathlib.toPolynomial (tragerNorm level lower shifted)) → Irreducible (HexPolyMathlib.toPolynomial q) → Factor.polyCoords q = lowerFactor → 0 < common.natDegree → Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) (Factor.polyCoords result)))

Irreducibility survives un-shifting and renormalising: the recovered factor produced from one accepted lower factor interprets to an irreducible polynomial over the extended tower.

theorem Hex.NumberTower.findSquarefreeShiftAux_squarefree (level : Level) (lower : List Level) (f : Array (Array ℚ)) (start fuel : ℕ) {shift : ℤ} {norm : Array (Array ℚ)} (h : Norm.findSquarefreeShiftAux level lower f start fuel = some (shift, norm)) : Norm.isSquarefree lower norm = true

Any shift accepted by the bounded search passes the executable squarefreeness check on its one-level norm.

theorem Hex.NumberTower.findSquarefreeShiftAux_norm (level : Level) (lower : List Level) (f : Array (Array ℚ)) (start fuel : ℕ) {shift : ℤ} {norm : Array (Array ℚ)} (h : Norm.findSquarefreeShiftAux level lower f start fuel = some (shift, norm)) : norm = Norm.oneLevel level lower f shift

The norm returned by the bounded search is the one-level resultant at the returned shift.

theorem Hex.NumberTower.findSquarefreeShift_squarefree (level : Level) (lower : List Level) (f : Array (Array ℚ)) {shift : ℤ} {norm : Array (Array ℚ)} (h : Norm.findSquarefreeShift level lower f = some (shift, norm)) : Norm.isSquarefree lower norm = true

A successful Norm.findSquarefreeShift returns a norm passing the executable squarefreeness check.

theorem Hex.NumberTower.findSquarefreeShift_norm (level : Level) (lower : List Level) (f : Array (Array ℚ)) {shift : ℤ} {norm : Array (Array ℚ)} (h : Norm.findSquarefreeShift level lower f = some (shift, norm)) : norm = Norm.oneLevel level lower f shift

A successful Norm.findSquarefreeShift returns the one-level resultant at the returned shift.

theorem Hex.NumberTower.array_degree_pos_of_raw_degree_pos (levels : List Level) (f : Array (Array ℚ)) (hdegree : 0 < (Factor.rawPoly levels f).natDegree) : 0 < f.size - 1

Positive rebuilt degree forces the flattened coefficient array to have at least two entries.

theorem Hex.NumberTower.oneLevel_degree_pos (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : Array (Array ℚ)) (shift : ℤ) (hdegree : 0 < (Factor.rawPoly (level :: lower) f).natDegree) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Squarefree (HexPolyMathlib.toPolynomial (Factor.rawPoly lower (Norm.oneLevel level lower f shift))) → 0 < (Factor.rawPoly lower (Norm.oneLevel level lower f shift)).natDegree

A squarefree one-level norm of a nonconstant input is itself nonconstant, so the recursion below the top level receives a genuine factorization problem.

theorem Hex.NumberTower.squarefree_toPolynomial_of_check (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f : Array (Array ℚ)) (hcheck : Norm.isSquarefree levels f = true) : Squarefree (HexPolyMathlib.toPolynomial (Factor.rawPoly levels f))

The executable squarefreeness certificate is semantically sound: a polynomial passing Norm.isSquarefree interprets to a squarefree polynomial over the tower coefficient field.

theorem Hex.NumberTower.mem_foldl_push_if {α : Type u_1} {β : Type u_2} (p : α → Prop) [DecidablePred p] (g : α → β) (items : List α) (init : Array β) (x : β) : x ∈ List.foldl (fun (out : Array β) (item : α) => if p item then out.push (g item) else out) init items → x ∈ init ∨ ∃ item ∈ items, p item ∧ g item = x

Membership inversion for a filtered push fold: an element of the result is either in the initial accumulator or the image of a passing input.

theorem Hex.NumberTower.foldl_push_if_toList {α : Type u_1} {β : Type u_2} (p : α → Prop) [DecidablePred p] (g : α → β) (items : List α) (init : Array β) : (List.foldl (fun (out : Array β) (item : α) => if p item then out.push (g item) else out) init items).toList = init.toList ++ List.filterMap (fun (item : α) => if p item then some (g item) else none) items

A filtered push fold materialises as the initial accumulator followed by a filterMap over the inputs.

theorem Hex.NumberTower.filterMap_prod_associated {K : Type u_1} {α : Type u_2} [Field K] (p : α → Prop) [DecidablePred p] (result common : α → Polynomial K) (hpass : ∀ (item : α), p item → Associated (result item) (common item)) (hskip : ∀ (item : α), ¬p item → IsUnit (common item)) (items : List α) : Associated (List.filterMap (fun (item : α) => if p item then some (result item) else none) items).prod (List.map common items).prod

Dropping unit contributions preserves the product up to a unit: if passing items have associated images and failing items map to units, the filtered product is associated to the full product.

theorem Hex.NumberTower.taylor_list_prod {K : Type u_1} [CommRing K] (c : K) (ps : List (Polynomial K)) : (Polynomial.taylor c) ps.prod = (List.map (⇑(Polynomial.taylor c)) ps).prod

Taylor translation distributes over a list product.

theorem Hex.NumberTower.polynomial_squarefree_map {K : Type u_1} {L : Type u_2} [Field K] [Field L] [CharZero K] [CharZero L] (f : K →+* L) {p : Polynomial K} (hp : Squarefree p) : Squarefree (Polynomial.map f p)

Squarefreeness transfers along field embeddings in characteristic zero, via separability.

theorem Hex.NumberTower.recoveryGcd_eq (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (p q : DensePoly (Arithmetic.Coeff levels)) : Factor.recoveryGcd p q = p.gcd q

Monic recovery division preserves the exact unnormalised gcd.

theorem Hex.NumberTower.recover_mem (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : LevelSemantics.DenoteInjective (level :: lower)) (shift : ℤ) (component : Array (Array ℚ)) (lowerFactors : Array (Array (Array ℚ))) {factor : Array (Array ℚ)} (hfactor : factor ∈ Factor.recover level lower shift component lowerFactors) : ∃ lowerFactor ∈ lowerFactors, have shifted := Factor.rawPoly (level :: lower) (Factor.shiftTop level lower component shift); have lifted := Factor.rawPoly (level :: lower) (Factor.embedLower level lower lowerFactor); have common := Norm.monic (shifted.gcd lifted); 0 < common.natDegree ∧ Factor.polyCoords (Norm.monic (Factor.rawPoly (level :: lower) (Factor.shiftTop level lower (Factor.polyCoords common) (-shift)))) = factor

Membership inversion for Factor.recover: every recovered factor arises from some lower factor whose lifted gcd with the shifted component is nonconstant, by un-shifting and renormalising that gcd.

theorem Hex.NumberTower.recover_mem_sound (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 := ⋯; have shifted := Factor.rawPoly (level :: lower) (Factor.shiftTop level lower component shift); Squarefree (HexPolyMathlib.toPolynomial (tragerNorm level lower shifted)) → (∀ lowerFactor ∈ lowerFactors, Factor.polyCoords (Factor.rawPoly lower lowerFactor) = lowerFactor ∧ Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly lower lowerFactor))) → ∀ factor ∈ Factor.recover level lower shift component lowerFactors, Factor.polyCoords (Factor.rawPoly (level :: lower) factor) = factor ∧ Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) factor))

Every factor produced by Factor.recover from canonical irreducible lower factors is canonical and interprets to an irreducible polynomial over the extended tower.

theorem Hex.NumberTower.toRatPoly_ofRatPoly (f : DensePoly ℚ) : Factor.toRatPoly (Factor.ofRatPoly f) = f

Wrapping rational coefficients as singleton coordinate arrays and reading them back is the identity.

theorem Hex.NumberTower.polyCoords_rawPoly_ofRatPoly (f : DensePoly ℚ) (hf : f ≠ 0) : Factor.polyCoords (Factor.rawPoly [] (Factor.ofRatPoly f)) = Factor.ofRatPoly f

Over the empty tower, ofRatPoly outputs canonical coordinate arrays: rebuilding and re-flattening them is the identity for nonzero inputs.

theorem Hex.NumberTower.toPolynomial_scale_inv_monic (f : DensePoly ℚ) (hf : f ≠ 0) : (HexPolyMathlib.toPolynomial (DensePoly.scale f.leadingCoeff⁻¹ f)).Monic

Rescaling a nonzero rational polynomial by the inverse of its leading coefficient interprets to a monic polynomial.

theorem Hex.NumberTower.scale_inv_associated (f : DensePoly ℚ) (hf : f ≠ 0) : Associated (HexPolyMathlib.toPolynomial (DensePoly.scale f.leadingCoeff⁻¹ f)) (HexPolyMathlib.toPolynomial f)

Rescaling by the inverse leading coefficient changes the interpretation only by a unit.

noncomputable def Hex.NumberTower.normalizedRatFactor (f : ZPoly) : Polynomial ℚ

The monic rational polynomial obtained from an integer factor by reading it rationally and dividing by its leading coefficient.

Equations

• Hex.NumberTower.normalizedRatFactor f = HexPolyMathlib.toPolynomial (Hex.DensePoly.scale f.toRatPoly.leadingCoeff⁻¹ f.toRatPoly)

theorem Hex.NumberTower.toRatPoly_ne_zero {f : ZPoly} (hf : f ≠ 0) : f.toRatPoly ≠ 0

The rational reading of a nonzero integer polynomial is nonzero.

theorem Hex.NumberTower.normalizedRatFactors_monic_associated (factors : List ZPoly) (hne : ∀ f ∈ factors, f ≠ 0) : (List.map normalizedRatFactor factors).prod.Monic ∧ Associated (List.map normalizedRatFactor factors).prod (List.map HexPolyZMathlib.toPolyℚ factors).prod

The product of monically rescaled integer factors is monic and associated to the product of their plain rational readings.

theorem Hex.NumberTower.factorPower_toPolyℚ (f : ZPoly) (n : ℕ) : HexPolyZMathlib.toPolyℚ (Factorization.factorPower f n) = HexPolyZMathlib.toPolyℚ f ^ n

The executable integer factor power reads rationally as the polynomial power.

theorem Hex.NumberTower.toPolyℚ_mul (f g : ZPoly) : HexPolyZMathlib.toPolyℚ (f * g) = HexPolyZMathlib.toPolyℚ f * HexPolyZMathlib.toPolyℚ g

Rational reading of integer polynomials is multiplicative.

theorem Hex.NumberTower.factorizationProduct_toPolyℚ_foldl (entries : List (ZPoly × ℕ)) (init : ZPoly) : HexPolyZMathlib.toPolyℚ (List.foldl (fun (product : ZPoly) (entry : ZPoly × ℕ) => product * Factorization.factorPower entry.1 entry.2) init entries) = HexPolyZMathlib.toPolyℚ init * (List.flatMap (fun (entry : ZPoly × ℕ) => List.replicate entry.2 (HexPolyZMathlib.toPolyℚ entry.1)) entries).prod

The executable fold multiplying labelled integer factor powers reads rationally as the initial value times the multiplicity-expanded product of the factors.

theorem Hex.NumberTower.factorizationProduct_toPolyℚ (factorization : Hex.Factorization) : HexPolyZMathlib.toPolyℚ factorization.product = Polynomial.C ↑factorization.scalar * (List.flatMap (fun (entry : ZPoly × ℕ) => List.replicate entry.2 (HexPolyZMathlib.toPolyℚ entry.1)) factorization.factors.toList).prod

A Hex.Factorization reads rationally as its scalar times the multiplicity-expanded product of its factors.

theorem Hex.NumberTower.factorize_normalized_product (f : ZPoly) (hf : f ≠ 0) : have factors := List.flatMap (fun (entry : ZPoly × ℕ) => List.replicate entry.2 entry.1) f.factorize.factors.toList; (List.map normalizedRatFactor factors).prod.Monic ∧ Associated (List.map normalizedRatFactor factors).prod (HexPolyZMathlib.toPolyℚ f)

Monically rescaling the multiplicity-expanded Berlekamp-Zassenhaus factors of a nonzero integer polynomial yields a monic product associated to its rational reading.

theorem Hex.NumberTower.normalizedRatFactor_irreducible (integer : ZPoly) (hinteger : integer ≠ 0) (entry : ZPoly × ℕ) (hentry : entry ∈ integer.factorize.factors) : Irreducible (normalizedRatFactor entry.1)

Each Berlekamp-Zassenhaus factor stays irreducible after monic rational rescaling: primitivity transfers integer irreducibility to ℚ by Gauss's lemma, and rescaling is associated.

theorem Hex.NumberTower.rawRatFactor_irreducible (integer : ZPoly) (hinteger : integer ≠ 0) (entry : ZPoly × ℕ) (hentry : entry ∈ integer.factorize.factors) : have q := DensePoly.scale entry.1.toRatPoly.leadingCoeff⁻¹ entry.1.toRatPoly; Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly [] (Factor.ofRatPoly q)))

The empty-tower coordinate encoding of a monically rescaled Berlekamp-Zassenhaus factor interprets to an irreducible polynomial.

theorem Hex.NumberTower.generatedRatFactors_sound (integer : ZPoly) (hinteger : integer ≠ 0) : 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 := DensePoly.scale factor.toRatPoly.leadingCoeff⁻¹ factor.toRatPoly; Factor.ofRatPoly q) rawFactors; ∀ factor ∈ factors, Factor.polyCoords (Factor.rawPoly [] factor) = factor ∧ Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly [] factor))

Every multiplicity-expanded, monically rescaled Berlekamp-Zassenhaus factor is a canonical coordinate array interpreting to an irreducible polynomial over the empty tower.

theorem Hex.NumberTower.factorRat_mem_sound (input : DensePoly ℚ) {factors : Array (Array (Array ℚ))} (hresult : Factor.factorRat? input = some factors) (factor : Array (Array ℚ)) : factor ∈ factors → Factor.polyCoords (Factor.rawPoly [] factor) = factor ∧ Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly [] factor))

Base-case soundness of the rational factorizer: every factor returned by Factor.factorRat? is canonical and interprets to an irreducible polynomial.