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 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.