theorem Hex.factorize_entry_leadingCoeff_pos (f : ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ f.factorize.factors.toList) : 0 < DensePoly.leadingCoeff entry.fst

Every recorded entry of the default public factorization has positive leading coefficient.

theorem Hex.factorize_entry_shouldRecord (f : ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ f.factorize.factors.toList) : shouldRecordPolynomialFactor entry.fst = true

Every recorded entry of the default public factorization passes the shouldRecordPolynomialFactor filter.

theorem Hex.factorize_entry_mem_raw_source (f : ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ f.factorize.factors.toList) : ∃ (raw : ZPoly), raw ∈ (factorFactors f).toList ∧ entry.fst = normalizeFactorSign raw

Any recorded entry of the default public factorization comes from the hybrid's raw factor array factorFactors, up to sign normalization.

theorem Hex.factorize_entry_primitive_of_chosen_raw_primitive {f : ZPoly} {entry : ZPoly × Nat} (hmem : entry ∈ f.factorize.factors.toList) (h_raw : ∀ (raw : ZPoly), raw ∈ (factorFactors f).toList → raw.Primitive) : entry.fst.Primitive

Every recorded entry of the default public factorization is primitive once every raw factor in the hybrid's raw factor array is primitive.

theorem Hex.factorize_entries_primitive (f : ZPoly) (h_raw : ∀ (raw : ZPoly), raw ∈ (factorFactors f).toList → raw.Primitive) (entry : ZPoly × Nat) : entry ∈ f.factorize.factors → entry.fst.Primitive

Public-entry specialisation: every recorded entry is primitive once the hybrid's raw factor array is primitive entrywise.

theorem Hex.factorize_pairwise_first (f : ZPoly) : List.Pairwise (fun (a b : ZPoly × Nat) => a.fst ≠ b.fst) f.factorize.factors.toList

The default public factorization has no duplicate polynomial keys.

class Hex.ZPoly.Irreducible (f : ZPoly) : Prop

Mathlib-free irreducibility predicate for integer polynomials.

The class form lets downstream Mathlib-free APIs request irreducibility through typeclass inference. The predicate remains the usual nonzero, non-unit, no proper factorization condition.

• not_zero : f ≠ 0

  The zero polynomial is not irreducible.

• not_unit : ¬f.IsUnit

  Units are excluded from irreducibility.

• no_factors (a b : ZPoly) : f = a * b → a.IsUnit ∨ b.IsUnit

  Every product decomposition has a unit factor.

def Hex.ZPoly.Associated (a b : ZPoly) : Prop

Mathlib-free associatedness predicate for integer polynomials: a and b are associated when b = a * u for some ZPoly-unit u (i.e. u = ±1). Used by irreducibility dischargers to translate "Mathlib-side irreducible factor of the primitive square-free part" to the direct non-divisibility hypothesis required by the greedy expansion helper.

Equations

• a.Associated b = ∃ (u : Hex.ZPoly), u.IsUnit ∧ b = a * u

def Hex.ZPoly.isNatPrime (n : Nat) : Bool

Integer primality checker used by constant-polynomial irreducibility. This is the shared verified bounded checker from HexArith.

Equations

• Hex.ZPoly.isNatPrime n = Hex.Nat.isPrimeTrial n

def Hex.ZPoly.isIrreducible (f : ZPoly) : Bool

Computational irreducibility checker backed by the public factorization API.

Constants are checked by integer primality. Positive-degree polynomials are checked from the returned Factorization: the scalar must be a unit and there must be exactly one polynomial factor with multiplicity one.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.ZPoly.eq_C_of_size_eq_one (a : ZPoly) (hsize : DensePoly.size a = 1) : a = DensePoly.C (DensePoly.coeff a 0)

A polynomial of dense size 1 is the constant polynomial of its zeroth coefficient. The trimming invariant on DensePoly forces the single stored coefficient to be nonzero, so coeff 0 already names the unique stored entry.

theorem Hex.ZPoly.irreducible_C_of_isNatPrime {k : Int} (hp : isNatPrime k.natAbs = true) : Irreducible (DensePoly.C k)

A constant polynomial DensePoly.C k is ZPoly.Irreducible whenever k.natAbs is prime in the elementary isNatPrime sense.

theorem Hex.ZPoly.isNatPrime_natAbs_of_irreducible_C {k : Int} (hk_ne : k ≠ 0) (hirr : Irreducible (DensePoly.C k)) : isNatPrime k.natAbs = true

An irreducible constant polynomial DensePoly.C k (for k ≠ 0) has k.natAbs prime in the elementary isNatPrime sense.

theorem Hex.ZPoly.irreducible_X : X.Irreducible

The integer indeterminate X is irreducible.

theorem Hex.ZPoly.Irreducible_of_modP_irreducible_of_primitive_of_admissible (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hprime : Nat.Prime p) (hprim : f.Primitive) (hadm : leadingCoeffAdmissible f p) (hnotConstant : 1 < DensePoly.size f) (hirr : (modP p f).Irreducible) : f.Irreducible

Mathlib-free Gauss reduction-mod-p transfer: a primitive integer polynomial whose leading coefficient survives reduction modulo a prime p and whose modular image is FpPoly-irreducible is itself ZPoly.Irreducible.

The hnotConstant : 1 < f.size precondition rules out the size-one constant case explicitly: the executable FpPoly.Irreducible predicate only asserts the factorization disjunction (it does not internally exclude constants the way Mathlib's _root_.Irreducible does via not_isUnit), so the non-unit clause for f is supplied at the ZPoly level. A primitive ZPoly of size > 1 is automatically not a ZPoly unit (units have size 1).

Mathlib analog: HexBerlekampZassenhausMathlib.irreducible_of_isPrimitive_of_irreducible_map_intCast_zmod (HexBerlekampZassenhausMathlib/IntReductionMod.lean:106).

theorem Hex.ZPoly.irreducible_of_linear (f : ZPoly) (hsize : decide (DensePoly.size f = 2) = true) (hcontent : decide (f.content = 1) = true) : f.Irreducible

Kernel-decidable irreducibility for a linear (dense size two) primitive integer polynomial: both hypotheses are Boolean checks on literal data, so a reified application discharges them with Eq.refl true. Public decide-slot form of irreducible_of_size_two_primitive for the irreducibility/factor_poly elaborators.

theorem Hex.zpolyIrreducible_normalizeFactorSign_of_zpolyIrreducible {f : ZPoly} (hirr : f.Irreducible) : (normalizeFactorSign f).Irreducible

Hex.normalizeFactorSign preserves Hex.ZPoly.Irreducible: the sign-normalised polynomial equals either the original or its -1 scaling, and -1 is a ZPoly unit, so the no-proper-factorization predicate transfers. Mathlib-free counterpart of the Mathlib-side zpolyIrreducible_normalizeFactorSign_of_zpolyIrreducible (HexBerlekampZassenhausMathlib). Consumed by the Mathlib-free factor_factors_irreducible assembly.

theorem Hex.xPowerFactorArray_irreducible (power : Nat) (factor : ZPoly) (h : factor ∈ (xPowerFactorArray power).toList) : factor.Irreducible

Every factor emitted by the extracted X-power normalization array is irreducible.

theorem Hex.reassemblePolynomialFactors_xPower_irreducible (d : FactorNormalizationData) (coreFactors : Array ZPoly) (factor : ZPoly) (_hmem : factor ∈ (reassemblePolynomialFactors d coreFactors).toList) (hx : factor ∈ (xPowerFactorArray d.xPower).toList) : factor.Irreducible

Reassembly preserves the irreducibility proof for normalization factors coming specifically from the extracted power of X.

theorem Hex.reassemblePolynomialFactors_factor_irreducible_of_complete_and_core_irreducible (d : FactorNormalizationData) (coreFactors : Array ZPoly) (hcomplete : reassemblyExpansionComplete d coreFactors) (h_core : ∀ (factor : ZPoly), factor ∈ coreFactors.toList → factor.Irreducible) {factor : ZPoly} (hmem : factor ∈ (reassemblePolynomialFactors d coreFactors).toList) : factor.Irreducible

Lift square-free-factor irreducibility through the reassembly. When the repeated-part expansion fully consumes its residual (so the reassembly emits only X powers and the supplied factors of the square-free part), every emitted raw factor is irreducible. This is the Mathlib-free "reassemble lift" consumed by the assembled per-branch output theorem to discharge the xPower half of each branch automatically.

theorem Hex.reassemblePolynomialFactors_constant_irreducible_or_repeated_or_one (d : FactorNormalizationData) {factor : ZPoly} (hcore : d.squareFreeCore = 1) (hmem : factor ∈ (reassemblePolynomialFactors d #[d.squareFreeCore]).toList) : factor.Irreducible ∨ factor ∈ (repeatedPartFactorArray d.repeatedPart).toList ∨ factor = 1

Membership classifier for the constant primitive square-free part branch. The only raw factors requiring irreducibility content are extracted powers of X; the singleton square-free factor is 1, and any repeated-part fallback is identified separately for later expansion through actual factors of the square-free part.

theorem Hex.normalizeForFactor_reassembles (f : ZPoly) : have normalized := normalizeForFactor f; ∃ (unit : Rat), normalized.xFreePrimitive.toRatPoly = DensePoly.scale unit (normalized.squareFreeCore * normalized.repeatedPart).toRatPoly

The primitive square-free layer in normalization reassembles the extracted X-free primitive polynomial up to the rational unit introduced by clearing denominators.

theorem Hex.reassembleNormalizedFactors_product (f : ZPoly) (normalized : FactorNormalizationData) (coreFactors : Array ZPoly) (hnormalized : normalizeForFactor f = normalized) (hcore : coreFactors.polyProduct = normalized.squareFreeCore) : ∃ (unit : Rat), normalized.xFreePrimitive.toRatPoly = DensePoly.scale unit (coreFactors.polyProduct * normalized.repeatedPart).toRatPoly

Replacing the primitive square-free part by a product-equivalent factor array preserves the rational-associate normalization invariant for the extracted primitive polynomial.

theorem Hex.normalizedConstantFactors_product (f : ZPoly) (normalized : FactorNormalizationData) (hnormalized : normalizeForFactor f = normalized) (hconst : DensePoly.natDegree normalized.squareFreeCore = 0) : ∃ (unit : Rat), normalized.xFreePrimitive.toRatPoly = DensePoly.scale unit (normalized.squareFreeCore * normalized.repeatedPart).toRatPoly

For constant square-free parts, the normalization-only factor array preserves the rational-associate normalization invariant for the extracted primitive polynomial.

theorem Hex.extractXPower_core_primitive_of_ne_zero (f : ZPoly) (hf : f ≠ 0) : f.primitivePart.extractXPower.core.Primitive

The X-free part of the primitive part of a nonzero integer polynomial is itself primitive. Stripping initial zero coefficients does not introduce a common factor because the original primitive part already has unit content.