theorem HexBerlekampZassenhausMathlib.zpoly_size_pos_of_monic {f : Hex.ZPoly} (h : Hex.DensePoly.Monic f) : 0 < Hex.DensePoly.size f

Monic integer polynomials have positive stored size.

theorem HexBerlekampZassenhausMathlib.zpoly_primitive_of_monic {f : Hex.ZPoly} (h : Hex.DensePoly.Monic f) : f.Primitive

Monic integer polynomials are primitive (content 1).

theorem HexBerlekampZassenhausMathlib.zpoly_normalize_factor_sign_of_monic {f : Hex.ZPoly} (h : Hex.DensePoly.Monic f) : Hex.normalizeFactorSign f = f

Monic integer polynomials are fixed by Hex.normalizeFactorSign.

theorem HexBerlekampZassenhausMathlib.monic_primitive_sign_normalized_of_monic {factor : Hex.ZPoly} (hfactor_monic : Hex.DensePoly.Monic factor) : Hex.DensePoly.Monic factor ∧ factor.content = 1 ∧ Hex.normalizeFactorSign factor = factor

A monic integer polynomial automatically has primitive content and is its own sign-normalisation. This packages the two normalisation hypotheses required by recombinationCandidate_eq_factor_of_recovery (content factor = 1 and normalizeFactorSign factor = factor) into one consequence of Monic factor, together with restating the monic hypothesis itself.

The recursive coverage proof for Hex.recombinationSearchModAux uses this after obtaining a monic integer divisor of the current target. Together with the Hensel-lift partition, this helper discharges the primitive and sign-normalised hypotheses of recombinationCandidate_eq_factor_of_recovery for that factor. Monicness itself is taken as a hypothesis here because the LiftedFactorSubsetPartition.cover field does not constrain the integer factor's leading-coefficient sign; the recursive coverage proof supplies it from a separate Hensel-lift normalisation argument.

theorem HexBerlekampZassenhausMathlib.henselLiftData_liftedFactors_size_eq (core : Hex.ZPoly) (B : ℕ) (primeData : Hex.PrimeChoiceData) : (Hex.henselLiftData core B primeData).liftedFactors.size = primeData.factorsModP.size

Size of the lifted-factor array equals the size of the modular-factor array.

This is the factor_count_eq field that HenselSubsetLiftHypotheses (line 1425 above) requires for the executable Hex.choosePrimeData / Hex.henselLiftData surface. The lifted-factor array is Hex.ZPoly.multifactorLiftQuadratic primeData.p B core (primeData.factorsModP.map Hex.FpPoly.liftToZ), whose size equals the input map's size by Hex.ZPoly.multifactorLiftQuadratic_size_eq_input; the map preserves size by Array.size_map.

theorem HexBerlekampZassenhausMathlib.MonicLift.factorCount_eq (core : Hex.ZPoly) (B : ℕ) (primeData : Hex.PrimeChoiceData) : (core.toMonicLiftData B primeData).liftedFactors.size = primeData.factorsModP.size

Multifactor Hensel lifting preserves the number of selected modular factors.

theorem HexBerlekampZassenhausMathlib.henselLiftData_liftedFactor_monic (core : Hex.ZPoly) (B : ℕ) (primeData : Hex.PrimeChoiceData) (hcore_monic : Hex.DensePoly.Monic core) (hprime_invariant : Hex.ZPoly.QuadraticMultifactorLiftInvariant primeData.p B core (Array.map Hex.FpPoly.liftToZ primeData.factorsModP).toList) (hp : 1 < primeData.p) (hB : 1 ≤ B) (i : Fin (Hex.henselLiftData core B primeData).liftedFactors.size) : Hex.DensePoly.Monic (Hex.henselLiftData core B primeData).liftedFactors[i]

Thin umbrella wrapper exposing per-output monicness of Hex.henselLiftData in the Mathlib-facing surface.

Hex.henselLiftData produces its liftedFactors by invoking Hex.ZPoly.multifactorLiftQuadratic, and the executable proof Hex.ZPoly.multifactorLiftQuadratic_each_monic already supplies monicness of every output index given monicness of the input polynomial and the quadratic multifactor lift invariant. This wrapper simply re-exposes that conclusion at the henselLiftData umbrella for downstream callers (notably monic_primitive_sign_normalized_of_monic above, which discharges the primitivity and sign-normalisation hypotheses required by recombinationCandidate_eq_factor_of_recovery once monicness is in hand).

theorem HexBerlekampZassenhausMathlib.henselLiftData_liftedFactor_monic_of_choosePrimeData (core : Hex.ZPoly) (B : ℕ) (primeData : Hex.PrimeChoiceData) (hcore_monic : Hex.DensePoly.Monic core) (hp_prime : Hex.Nat.Prime primeData.p) (hp : 1 < primeData.p) (hB : 1 ≤ B) (hfactors_monic : ∀ g ∈ primeData.factorsModP, Hex.DensePoly.Monic g) (hproduct_mod_p : (Array.map Hex.FpPoly.liftToZ primeData.factorsModP).polyProduct.congr core primeData.p) (hcoprime : Hex.ZPoly.QuadraticMultifactorCoprimeSplits primeData.p primeData.factorsModP.toList) (hnonempty : primeData.factorsModP.toList ≠ []) (i : Fin (Hex.henselLiftData core B primeData).liftedFactors.size) : Hex.DensePoly.Monic (Hex.henselLiftData core B primeData).liftedFactors[i]

Composed convenience wrapper: combines Hex.ZPoly.QuadraticMultifactorLiftInvariant_of_choosePrimeData with henselLiftData_liftedFactor_monic so that a Mathlib-side caller can discharge per-output monicness of Hex.henselLiftData from the choosePrimeData boundary facts directly, without having to construct the internal QuadraticMultifactorLiftInvariant themselves.

The upstream wrapper Hex.ZPoly.QuadraticMultifactorLiftInvariant_of_choosePrimeData (in HexBerlekampZassenhaus) packages the per-factor monicness, mod-p product congruence, sequential split coprimality, and nonempty witness into the abstract invariant; this wrapper then feeds it into the abstract- invariant version henselLiftData_liftedFactor_monic above.

theorem HexBerlekampZassenhausMathlib.henselLiftData_liftedFactor_injective (core : Hex.ZPoly) (B : ℕ) (primeData : Hex.PrimeChoiceData) (hcore_monic : Hex.DensePoly.Monic core) (hprime_invariant : Hex.ZPoly.QuadraticMultifactorLiftInvariant primeData.p B core (Array.map Hex.FpPoly.liftToZ primeData.factorsModP).toList) (hp : 1 < primeData.p) (hB : 1 ≤ B) (hfactors_monic : ∀ g ∈ primeData.factorsModP, Hex.DensePoly.Monic g) (hproduct_mod_p : (Array.map Hex.FpPoly.liftToZ primeData.factorsModP).polyProduct.congr core primeData.p) (hfactorsModP_nodup : primeData.factorsModP.toList.Nodup) : Function.Injective (liftedFactor (Hex.henselLiftData core B primeData))

Abstract-invariant injectivity umbrella for Hex.henselLiftData outputs.

Mirrors the structure of henselLiftData_liftedFactor_monic: takes the recursive QuadraticMultifactorLiftInvariant package plus mod-p product congruence and Nodup of the original modular factor list, and produces Function.Injective (liftedFactor d) directly.

The proof uses Hex.ZPoly.multifactorLiftQuadratic_each_congr_mod_base: each lifted factor reduces modulo p to the corresponding original modular factor (after FpPoly.liftToZ). Equal lifted factors therefore force equal modular factors, and Nodup of factorsModP collapses to equal indices.

This bypasses pairwise coprimality entirely; degenerate "unit lifted factor" cases are excluded by Nodup rather than by positive natDegree.