def HexBerlekampZassenhausMathlib.irreducibleByFactorization (f : Polynomial ℤ) : Bool

Executable irreducibility predicate for transported integer polynomials.

The checker delegates to the Mathlib-free Hex.ZPoly executable predicate after transporting the Mathlib polynomial into the project representation.

Equations

• HexBerlekampZassenhausMathlib.irreducibleByFactorization f = (HexPolyZMathlib.ofPolynomial f).isIrreducible

@[simp]

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

The default executable factorization multiplies back to the input.

theorem Hex.ZPoly.Irreducible_iff_polynomialIrreducible (f : ZPoly) : f.Irreducible ↔ _root_.Irreducible (HexPolyZMathlib.toPolynomial f)

The Mathlib-free executable irreducibility predicate agrees with Mathlib's irreducibility predicate after transport to Polynomial ℤ.

theorem Hex.ZPoly.polynomialIrreducible_iff_irreducible (f : ZPoly) : _root_.Irreducible (HexPolyZMathlib.toPolynomial f) ↔ f.Irreducible

Mathlib irreducibility of the transported polynomial is equivalent to the Mathlib-free executable irreducibility predicate.

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

Hex.ZPoly.Irreducible is preserved by Hex.normalizeFactorSign.

Exposed publicly so the assembled per-branch output theorem can lift raw factor irreducibility to entry irreducibility (entries pass through collectFactorMultiplicities, which normalises each raw factor's sign).

theorem HexBerlekampZassenhausMathlib.factorize_entries_primitive_of_chosen_raw_primitive (f : Hex.ZPoly) (hf : f ≠ 0) (entry : Hex.ZPoly × ℕ) : entry ∈ f.factorize.factors → entry.1.Primitive

Every polynomial factor emitted by the default executable factorization of a nonzero input is primitive. The public factorization verifies its own output, so primitivity is discharged from f ≠ 0 alone (the filtered product reconstructs f); no raw-source hypothesis is needed.

theorem HexBerlekampZassenhausMathlib.toPolynomial_foldl_mul (lst : List Hex.ZPoly) (init : Hex.ZPoly) : HexPolyZMathlib.toPolynomial (List.foldl (fun (x1 x2 : Hex.ZPoly) => x1 * x2) init lst) = List.foldl (fun (x1 x2 : Polynomial ℤ) => x1 * x2) (HexPolyZMathlib.toPolynomial init) (List.map HexPolyZMathlib.toPolynomial lst)

Conversion to Mathlib polynomials preserves a left-associated product.

theorem HexBerlekampZassenhausMathlib.toPolynomial_one_zpoly : HexPolyZMathlib.toPolynomial 1 = 1

The executable Array.polyProduct agrees with Mathlib's List.prod after pushing each factor through the toPolynomial map. This is the algorithm-to-Mathlib translation needed to feed Hex.ZPoly factor lists into UFD arguments over Polynomial ℤ.

theorem HexBerlekampZassenhausMathlib.polyProduct_toPolynomial (factors : Array Hex.ZPoly) : HexPolyZMathlib.toPolynomial factors.polyProduct = (List.map HexPolyZMathlib.toPolynomial factors.toList).prod

Converting an executable factor product gives the corresponding Mathlib list product.

def HexBerlekampZassenhausMathlib.flattenedFactorEntries (entries : List (Hex.ZPoly × ℕ)) : List Hex.ZPoly

Expand factorization entries by multiplicity, forgetting their packed array shape.

Equations

• HexBerlekampZassenhausMathlib.flattenedFactorEntries entries = List.flatMap (fun (entry : Hex.ZPoly × ℕ) => List.replicate entry.2 entry.1) entries

def HexBerlekampZassenhausMathlib.factorizationFlattenedFactors (φ : Hex.Factorization) : List Hex.ZPoly

Expand the polynomial entries of a Hex.Factorization by multiplicity.

Equations

• HexBerlekampZassenhausMathlib.factorizationFlattenedFactors φ = HexBerlekampZassenhausMathlib.flattenedFactorEntries φ.factors.toList

theorem HexBerlekampZassenhausMathlib.factorPower_toPolynomial (f : Hex.ZPoly) (k : ℕ) : HexPolyZMathlib.toPolynomial (Hex.Factorization.factorPower f k) = HexPolyZMathlib.toPolynomial f ^ k

Conversion to Mathlib polynomials preserves the executable factor power.

theorem HexBerlekampZassenhausMathlib.factorizationProduct_toPolynomial (φ : Hex.Factorization) : HexPolyZMathlib.toPolynomial φ.product = Polynomial.C φ.scalar * (List.map HexPolyZMathlib.toPolynomial (factorizationFlattenedFactors φ)).prod

Transport Hex.Factorization.product to Mathlib as the scalar times the product of the multiplicity-flattened transported factors.

theorem HexBerlekampZassenhausMathlib.normalize_toPolynomial_of_normalizeFactorSign_id {f : Hex.ZPoly} (hne : f ≠ 0) (h : Hex.normalizeFactorSign f = f) : normalize (HexPolyZMathlib.toPolynomial f) = HexPolyZMathlib.toPolynomial f

A nonzero executable integer polynomial fixed by Hex.normalizeFactorSign transports to a normalize-fixed polynomial over ℤ.

This is the reusable sign-normalization lemma for Mathlib-side factorization arguments over Hex.ZPoly factors.

theorem HexBerlekampZassenhausMathlib.zpoly_eq_of_toPolynomial_associated_of_primitive_pos_leading {p q : Hex.ZPoly} (hp_primitive : p.Primitive) (hq_primitive : q.Primitive) (hp_lc : 0 < Hex.DensePoly.leadingCoeff p) (hq_lc : 0 < Hex.DensePoly.leadingCoeff q) (hassoc : Associated (HexPolyZMathlib.toPolynomial p) (HexPolyZMathlib.toPolynomial q)) : p = q

Primitive executable integer polynomials with positive leading coefficient are the canonical representatives of their Mathlib Associated class after transport to Polynomial ℤ.

theorem HexBerlekampZassenhausMathlib.zpoly_not_associated_of_ne_of_primitive_pos_leading {p q : Hex.ZPoly} (hp_primitive : p.Primitive) (hq_primitive : q.Primitive) (hp_lc : 0 < Hex.DensePoly.leadingCoeff p) (hq_lc : 0 < Hex.DensePoly.leadingCoeff q) (hpq : p ≠ q) : ¬Associated (HexPolyZMathlib.toPolynomial p) (HexPolyZMathlib.toPolynomial q)

Distinct primitive executable integer polynomials with positive leading coefficient are not associated after transport to Polynomial ℤ.

theorem HexBerlekampZassenhausMathlib.factorize_entries_not_associated (f : Hex.ZPoly) (hf : f ≠ 0) : List.Pairwise (fun (a b : Hex.ZPoly × ℕ) => ¬Associated (HexPolyZMathlib.toPolynomial a.1) (HexPolyZMathlib.toPolynomial b.1)) f.factorize.factors.toList

Recorded entries of the default executable factorization of a nonzero input are pairwise non-associated after transport to Polynomial ℤ. Primitivity is discharged from f ≠ 0 by the self-certifying path.

theorem HexBerlekampZassenhausMathlib.factorize_entry_dvd (f : Hex.ZPoly) {entry : Hex.ZPoly × ℕ} (hentry : entry ∈ f.factorize.factors) : HexPolyZMathlib.toPolynomial entry.1 ∣ HexPolyZMathlib.toPolynomial f

Every recorded factor divides the transported input polynomial.

theorem HexBerlekampZassenhausMathlib.factorize_exists_root (f : Hex.ZPoly) (hf : f ≠ 0) {z : ℂ} (hz : (Polynomial.map (Int.castRingHom ℂ) (HexPolyZMathlib.toPolynomial f)).IsRoot z) : ∃ entry ∈ f.factorize.factors, (Polynomial.map (Int.castRingHom ℂ) (HexPolyZMathlib.toPolynomial entry.1)).IsRoot z

Every complex root of a nonzero input is a root of one of the recorded irreducible factors.

theorem HexBerlekampZassenhausMathlib.factorize_unique (φ ψ : Hex.Factorization) (hφ_norm : ∀ entry ∈ φ.factors, Hex.normalizeFactorSign entry.1 = entry.1) (hψ_norm : ∀ entry ∈ ψ.factors, Hex.normalizeFactorSign entry.1 = entry.1) (hφ_nonconst : ∀ entry ∈ φ.factors, 0 < Hex.DensePoly.natDegree entry.1) (hψ_nonconst : ∀ entry ∈ ψ.factors, 0 < Hex.DensePoly.natDegree entry.1) (hφ_irr : ∀ entry ∈ φ.factors, entry.1.Irreducible) (hψ_irr : ∀ entry ∈ ψ.factors, entry.1.Irreducible) (hφ_prod_ne : φ.product ≠ 0) (hprod : φ.product = ψ.product) : φ.scalar = ψ.scalar ∧ (List.map (fun (e : Hex.ZPoly × ℕ) => Multiset.replicate e.2 e.1) φ.factors.toList).sum = (List.map (fun (e : Hex.ZPoly × ℕ) => Multiset.replicate e.2 e.1) ψ.factors.toList).sum

Two irreducible executable factorizations of the same nonzero polynomial have the same signed scalar and the same multiplicity-flattened multiset of polynomial factors. The corrected statement compares flattened normalized factors rather than raw List.Perm, since Hex.Factorization does not constrain factor sign, multiplicity packing, or constant factors. The normalizeFactorSign and nonconst hypotheses rule out the corresponding counterexamples.

theorem HexBerlekampZassenhausMathlib.leadingCoeff_normalizeFactorSign_nonneg (f : Hex.ZPoly) : 0 ≤ Hex.DensePoly.leadingCoeff (Hex.normalizeFactorSign f)

Sign normalization produces a nonnegative leading coefficient.