theorem Hex.latticeCoreFactorsWithBound_polyProduct (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) {cf : Array ZPoly} (h : latticeCoreFactorsWithBound core B primeData = some cf) : cf.polyProduct = core

PolyProduct identity for the van Hoeij lattice factorization: every emitted factor array multiplies back to core. The singleton arms are immediate and the CLD-split arm reuses bhksRecoveryCoreWithBound_product.

theorem Hex.latticeCoreFactorsWithBound_normalizeFactorSign (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) (hcore_pos : 0 < DensePoly.leadingCoeff core) {cf : Array ZPoly} (h : latticeCoreFactorsWithBound core B primeData = some cf) (factor : ZPoly) : factor ∈ cf.toList → normalizeFactorSign factor = factor

Each factor emitted by the van Hoeij lattice factorization is fixed by normalizeFactorSign, provided core has positive leading coefficient. The CLD-split factors are sign-normalized by construction, and the singleton arms are core, fixed by its positive leading coefficient.

theorem Hex.latticeCoreFactorsWithBound_degree_pos (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) (hcore_deg : 0 < DensePoly.natDegree core) {cf : Array ZPoly} (h : latticeCoreFactorsWithBound core B primeData = some cf) (factor : ZPoly) : factor ∈ cf.toList → 0 < DensePoly.natDegree factor

Each factor emitted by the van Hoeij lattice factorization has positive degree?, provided core itself has positive degree. The CLD-split factors have positive degree by construction, and the singleton arms are core, whose positive degree is the sole hypothesis.

theorem Hex.splitIntegerRootFactorsAux_factor_irreducible {target : ZPoly} {roots : List Int} {fuel : Nat} {factors : Array ZPoly} {residual factor : ZPoly} (hsplit : splitIntegerRootFactorsAux target roots fuel = (factors, residual)) (hmem : factor ∈ factors.toList) : factor.Irreducible

Factors emitted by the integer-root splitter are monic linear root factors, and hence irreducible. This is the theorem-level wrapper used by the quadratic-root branch before any optional residual factor is appended.

theorem Hex.splitIntegerRootFactorsAux_factors_form {target : ZPoly} {roots : List Int} {fuel : Nat} {factors : Array ZPoly} {residual : ZPoly} (hsplit : splitIntegerRootFactorsAux target roots fuel = (factors, residual)) : ∃ (rs : List Int), rs.Sublist roots ∧ factors.toList = List.map linearFactorForRoot rs

Public wrapper of the splitter distinct-roots invariant: factors emitted by splitIntegerRootFactorsAux are linearFactorForRoot rᵢ for some sublist rs of the input roots. Composed with roots.Nodup (e.g. via integerRootCandidates_nodup) to read off pairwise distinctness of the factor roots, used by the linear-vs-linear pairwise non-association case.

theorem Hex.exhaustiveIntegerTrialCoreFactorsWithBound_polyProduct (core : ZPoly) (B : Nat) : (exhaustiveIntegerTrialCoreFactorsWithBound core B).polyProduct = core

PolyProduct identity for the standalone integer trial-division algorithm.

theorem Hex.exhaustiveIntegerTrialCoreFactorsWithBound_normalizeFactorSign (core : ZPoly) (B : Nat) (hcore_pos : 0 < DensePoly.leadingCoeff core) (factor : ZPoly) : factor ∈ (exhaustiveIntegerTrialCoreFactorsWithBound core B).toList → normalizeFactorSign factor = factor

Each factor emitted by the standalone integer trial-division algorithm is fixed by normalizeFactorSign, provided core has positive leading coefficient.

theorem Hex.exhaustiveIntegerTrialCoreFactorsWithBound_shouldRecord (core : ZPoly) (B : Nat) (hcore_pos : 0 < DensePoly.leadingCoeff core) (factor : ZPoly) : factor ∈ (exhaustiveIntegerTrialCoreFactorsWithBound core B).toList → shouldRecordPolynomialFactor factor = true

Each factor emitted by the standalone integer trial-division algorithm satisfies shouldRecordPolynomialFactor, provided core has positive leading coefficient.

theorem Hex.scale_neg_one_neg_one (p : ZPoly) : DensePoly.scale (-1) (DensePoly.scale (-1) p) = p

scale (-1) is an involution on ZPoly: applying it twice returns the original polynomial.

theorem Hex.squareFreeCore_dvd_self (f : ZPoly) (hf : f ≠ 0) : (normalizeForFactor f).squareFreeCore ∣ f

The normalized primitive square-free part divides the original polynomial.

Chains squareFreeCore ∣ squareFreeCore * repeatedPart through the signed reassembly scale ε (squareFreeCore * repeatedPart) = primitivePart core (the X-free part is primitive, so its primitive part is itself), then core ∣ primitivePart f (the X-power extraction product) and primitivePart f ∣ f (content_mul_primitivePart). Lifts a coefficient bound on divisors of f to a bound on divisors of the primitive square-free part.

theorem Hex.exhaustiveIntegerTrialCoreFactorsWithBound_degree_pos (core : ZPoly) (B : Nat) (hcore_prim : core.Primitive) (hcore_pos : 0 < DensePoly.leadingCoeff core) (factor : ZPoly) : factor ∈ (exhaustiveIntegerTrialCoreFactorsWithBound core B).toList → 0 < DensePoly.natDegree factor

Every factor emitted by the standalone integer trial-division algorithm has positive degree, when core is primitive with positive leading coefficient.

The three factor families are handled separately: integer-root split factors are linearFactorForRoot images (degree one); peeled candidates carry the positive-degree invariant of trialDivisionCandidatesUpTo; and the final residual, when retained, cannot be a constant, because a size-one divisor of a primitive polynomial is a unit, which a ≠ 1 residual with positive leading coefficient is not.