theorem Hex.reassemblyExpansionComplete_constant_of_ne_zero (f : ZPoly) (hf : f ≠ 0) (hdeg : DensePoly.natDegree (normalizeForFactor f).squareFreeCore = 0) : reassemblyExpansionComplete (normalizeForFactor f) #[(normalizeForFactor f).squareFreeCore]

When the recorded primitive square-free part has degree zero (and f ≠ 0), the fast-path singleton-part reassembly is automatically expansion-complete: the primitive square-free part collapses to 1 via squareFreeCore_eq_one_of_constant_of_ne_zero, the singleton-1 expansion is the identity via expandRepeatedPartFactorArray_singleton_one, and the residual (normalizeForFactor f).repeatedPart is forced to 1 by normalizeForFactor_repeatedPart_eq_one_of_constant (the constant-branch specialisation of ZPoly.primitiveSquareFreeDecomposition_repeatedPart_eq_one_of_squareFreeCore_degree_zero). Used by the fast-path constant arm public wrapper factor_constant_branch_entry_irreducible_of_choosePrimeData so it can drop its explicit hcomplete hypothesis. The small-mod singleton, slow-quadratic, and fast-quadratic branches have analogous theorems.

theorem Hex.squareFreeCore_normalizeFactorSign_of_ne_zero (f : ZPoly) (hf : f ≠ 0) : normalizeFactorSign (normalizeForFactor f).squareFreeCore = (normalizeForFactor f).squareFreeCore

The normalized primitive square-free part has positive leading coefficient (squareFreeCore_leadingCoeff_pos_of_ne_zero), so its sign-normalisation is the identity. Exposed publicly for support-lemma callers in the Mathlib-side layer (notably the small-mod singleton arm specialisation of normalizeForFactor_repeatedPart_isFactorPower_polyProduct_of_irreducible_factors_cover, which discharges its hnorm precondition with this lemma).

theorem Hex.factorTrialFactorsWithBound_polyProduct (f : ZPoly) (B : Nat) : DensePoly.C (signedContentScalar f) * (factorTrialFactorsWithBound f B).polyProduct = f

The raw bounded trial-division factor array multiplies back to the input once the signed content scalar is restored.

theorem Hex.factorTrialWithBound_product (f : ZPoly) (B : Nat) : (factorTrialWithBound f B).product = f

Bounded trial division reconstructs its input exactly: the packed Factorization multiplies back to f for every bound.

theorem Hex.factorTrial_product (f : ZPoly) : (factorTrial f).product = f

The public trial-division entry point reconstructs its input.

theorem Hex.factorize_product (f : ZPoly) : f.factorize.product = f

The public total factorization reconstructs its input. This holds unconditionally: each non-backstop method's result is accepted only when it reconstructs f (the self-certifying guard in factorTraced), and every fallback is the proven factorTrial backstop.

theorem Hex.factorize_entries_primitive_of_ne_zero (f : ZPoly) (hf : f ≠ 0) (entry : ZPoly × Nat) : entry ∈ f.factorize.factors → entry.fst.Primitive

Every recorded entry of the default factorization of a nonzero f is primitive, with no raw-source hypothesis. The hybrid's factorizationOfFactors packing certifies the filtered product reconstructs f (factorize_product + factorizationOfFactors_product), so that product is primitive and hence so is every recorded (filtered) entry.

theorem Hex.factorize_entries_degree_pos (f : ZPoly) (hf : f ≠ 0) (entry : ZPoly × Nat) : entry ∈ f.factorize.factors → 0 < DensePoly.natDegree entry.fst

Every recorded entry of a nonzero default factorization has positive degree.

The recording filter alone does not exclude nonunit constants. Primitivity is the essential extra fact: a primitive constant is a unit, while recorded factors are nonunits.

theorem Hex.ZPoly.isIrreducible_X : X.isIrreducible = true

The factorization-backed executable irreducibility checker accepts the indeterminate X. This follows from product preservation: positive-degree factors with positive multiplicities can contribute total degree one only as one factor of multiplicity one.

theorem Hex.checkIrreducibleCert_prime_data (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (hcert : checkIrreducibleCert f cert = true) (primeData : PrimeFactorData) : primeData ∈ cert.perPrime.toList → PrimeFactorData.checkForPolynomial f primeData = true

A successful integer certificate exposes the per-prime polynomial check fact: every recorded PrimeFactorData block satisfies checkForPolynomial f; admissible prime, positive recorded factor degrees, modular degree-sum and factor-product alignment, and aligned nested Rabin certificates. Callers extract individual conjuncts via the dedicated helpers below.

theorem Hex.checkIrreducibleCert_isGoodPrime (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (hcert : checkIrreducibleCert f cert = true) (primeData : PrimeFactorData) : primeData ∈ cert.perPrime.toList → isGoodPrime f primeData.p = true

A successful integer certificate exposes the per-prime good-prime fact: every recorded PrimeFactorData uses an admissible prime for f (size, leading coefficient, and modular square-freeness all satisfied).

theorem Hex.checkIrreducibleCert_factorDegrees_positive (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (hcert : checkIrreducibleCert f cert = true) (primeData : PrimeFactorData) : primeData ∈ cert.perPrime.toList → ∀ (i : Nat) (hi : i < primeData.factorDegrees.size), 0 < primeData.factorDegrees[i]

A successful integer certificate exposes positivity of every recorded modular factor degree: each per-prime block's factorDegrees array contains only positive entries.

theorem Hex.checkIrreducibleCert_degreeSum_eq (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (hcert : checkIrreducibleCert f cert = true) (primeData : PrimeFactorData) : primeData ∈ cert.perPrime.toList → primeData.degreeSum = DensePoly.natDegree (ZPoly.modP primeData.p f)

A successful integer certificate exposes the per-prime modular degree-sum alignment: each block's recorded degreeSum equals the degree of the polynomial's modular image.

theorem Hex.checkIrreducibleCert_factorProduct_eq (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (hcert : checkIrreducibleCert f cert = true) (primeData : PrimeFactorData) : primeData ∈ cert.perPrime.toList → primeData.factorProduct = ZPoly.modP primeData.p f

A successful integer certificate exposes the per-prime modular factor product alignment: each block's recorded factorProduct equals the polynomial's modular image.

theorem Hex.checkIrreducibleCert_certificate_alignment (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (hcert : checkIrreducibleCert f cert = true) (primeData : PrimeFactorData) : primeData ∈ cert.perPrime.toList → primeData.checkFactorCerts = true

A successful integer certificate exposes the per-prime nested Rabin checks: checkFactorCerts validates the concrete modular factor array, the recorded degrees, and the upstream Berlekamp.checkIrreducibilityCertificate result for each aligned entry.

theorem Hex.checkIrreducibleCert_degree_obstructions (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (hcert : checkIrreducibleCert f cert = true) : ZPolyIrreducibilityCertificate.checkDegreeObstructions f cert = true

A successful integer certificate satisfies the top-level degree-obstruction check: every recorded DegreeObstruction is valid for the certificate, and every nontrivial candidate factor degree of f has at least one obstruction.

theorem Hex.checkIrreducibleCert_obstructs_candidate_degrees (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (hcert : checkIrreducibleCert f cert = true) (targetDegree : Nat) : targetDegree ∈ ZPolyIrreducibilityCertificate.candidateFactorDegrees f → ZPolyIrreducibilityCertificate.hasObstructionFor f cert targetDegree = true

A successful integer certificate provides a valid obstruction for every nontrivial candidate factor degree of f (the degrees 1, …, (deg f) / 2), ruling out an integer factorization at any of those degrees.

theorem Hex.degreeObstruction_no_subset_degree (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (obs : DegreeObstruction) (primeData : PrimeFactorData) (hobs : DegreeObstruction.checkForCertificate f cert obs = true) (hprime : cert.primeDataAt? obs.primeIndex = some primeData) : primeData.hasSubsetDegree obs.targetDegree = false

A valid DegreeObstruction exposes the underlying no-subset-sum fact: the referenced per-prime block has no subset of its modular factor degrees summing to the obstruction's targetDegree.