theorem HexBerlekampZassenhausMathlib.factorize_irreducible_of_nonUnit (f : Hex.ZPoly) (entry : Hex.ZPoly × ℕ) : entry ∈ f.factorize.factors → entry.1.Irreducible

Every polynomial factor emitted by the default executable factorization is irreducible in the executable Hex.ZPoly sense.

theorem HexBerlekampZassenhausMathlib.factorize_polynomialIrreducible_of_nonUnit (f : Hex.ZPoly) (entry : Hex.ZPoly × ℕ) : entry ∈ f.factorize.factors → Irreducible (HexPolyZMathlib.toPolynomial entry.1)

Every polynomial factor emitted by the default executable factorization is irreducible after transport to Polynomial ℤ.

theorem HexBerlekampZassenhausMathlib.factorize_entries_leadingCoeff_pos (f : Hex.ZPoly) (entry : Hex.ZPoly × ℕ) : entry ∈ f.factorize.factors → 0 < Hex.DensePoly.leadingCoeff entry.1

Every polynomial factor emitted by the default executable factorization has positive leading coefficient.

theorem HexBerlekampZassenhausMathlib.factorize_normalized (f : Hex.ZPoly) (hf : f ≠ 0) : f.factorize.product = f ∧ (∀ entry ∈ f.factorize.factors, entry.1.Primitive ∧ Irreducible (HexPolyZMathlib.toPolynomial entry.1) ∧ 0 < Hex.DensePoly.leadingCoeff entry.1) ∧ (∀ entry ∈ f.factorize.factors, 0 < entry.2) ∧ List.Pairwise (fun (a b : Hex.ZPoly × ℕ) => ¬Associated (HexPolyZMathlib.toPolynomial a.1) (HexPolyZMathlib.toPolynomial b.1)) f.factorize.factors.toList ∧ f.factorize.scalar = if f = 0 then 0 else if Hex.DensePoly.leadingCoeff f < 0 then -f.content else f.content

The normalized irreducible factorization produced for a nonzero polynomial.

The product reconstructs the input. Every recorded factor is primitive, has positive leading coefficient, and is irreducible after transport to Polynomial ℤ; multiplicities are positive; distinct entries are not associates; and the scalar is the signed content of the input.

The hypothesis f ≠ 0 is necessary because the factorization of zero is degenerate: its scalar and product are zero, while zero is not primitive.

theorem HexBerlekampZassenhausMathlib.factorize_entries_normalizeFactorSign (f : Hex.ZPoly) (entry : Hex.ZPoly × ℕ) : entry ∈ f.factorize.factors → Hex.normalizeFactorSign entry.1 = entry.1

The sign-normalization side condition for the default executable factorization: every recorded polynomial factor is fixed by normalizeFactorSign. This is the hψ_norm clause that uniqueness/checker callers would otherwise reconstruct from the executable Hex.factorize_entry_normalizeFactorSign_id.

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

The nonconstant side condition for the default executable factorization: every recorded polynomial factor has positive degree. This is the hψ_nonconst clause uniqueness/checker callers would otherwise reconstruct.

Positive degree is not derivable from shouldRecordPolynomialFactor alone; a constant like Hex.DensePoly.C 2 passes the recording filter, has positive leading coefficient, and is sign-normalized. The constant case is excluded by primitivity (content 1 forces a constant to be ±1), so this carries the f ≠ 0 side condition that Hex.factorize_entries_primitive_of_ne_zero needs (the self-certifying path). The constant-exclusion argument itself is Hex.degree_pos_of_primitive_norm_record.

theorem HexBerlekampZassenhausMathlib.factorize_unique_of_product (f : Hex.ZPoly) (φ : Hex.Factorization) (hf_ne : f ≠ 0) (hproduct : φ.product = f) (hφ_norm : ∀ entry ∈ φ.factors, Hex.normalizeFactorSign entry.1 = entry.1) (hψ_norm : ∀ entry ∈ f.factorize.factors, Hex.normalizeFactorSign entry.1 = entry.1) (hφ_nonconst : ∀ entry ∈ φ.factors, 0 < Hex.DensePoly.natDegree entry.1) (hψ_nonconst : ∀ entry ∈ f.factorize.factors, 0 < Hex.DensePoly.natDegree entry.1) (hirr : ∀ entry ∈ φ.factors, entry.1.Irreducible) : φ.scalar = f.factorize.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) f.factorize.factors.toList).sum

Uniqueness specialised against the default executable factorization, so callers only provide the competing product, irreducibility, sign-normalization, and nonconstant-factor facts, plus that the input is nonzero. The default factorization's own well-formedness is supplied by factorize_irreducible_of_nonUnit and its sibling lemmas.

theorem HexBerlekampZassenhausMathlib.factorize_unique_of_product_default (f : Hex.ZPoly) (φ : Hex.Factorization) (hf_ne : f ≠ 0) (hproduct : φ.product = f) (hφ_norm : ∀ entry ∈ φ.factors, Hex.normalizeFactorSign entry.1 = entry.1) (hφ_nonconst : ∀ entry ∈ φ.factors, 0 < Hex.DensePoly.natDegree entry.1) (hirr : ∀ entry ∈ φ.factors, entry.1.Irreducible) : φ.scalar = f.factorize.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) f.factorize.factors.toList).sum

Default-specialised sibling of factorize_unique_of_product that discharges the default factorization's own sign-normalization and nonconstant side conditions internally, so callers no longer supply hψ_norm or hψ_nonconst. The nonconstant clause needs only f ≠ 0 (the same hf_ne already supplied), via factorize_entries_degree_pos; hψ_norm is discharged unconditionally.

theorem Hex.ZPoly.isIrreducible_iff (f : ZPoly) : f.isIrreducible = true ↔ f.Irreducible

The executable irreducibility checker Hex.ZPoly.isIrreducible agrees with the Hex.ZPoly.Irreducible class.

isIrreducible runs factorize and checks the result is a single primitive factor of multiplicity 1 (with a ±1 scalar), so this is exactly the statement that the default factorization is a correct irreducible factorization. The degree-0 (constant) arm is the elementary-primality characterisation (irreducible_C_of_isNatPrime / isNatPrime_natAbs_of_irreducible_C); the positive-degree arm composes factorize_irreducible_of_nonUnit (forward) with factorize_unique_of_product_default (backward, which pins the factor count to the normalizedFactors cardinality).

@[instance_reducible]

instance Hex.ZPoly.instDecidableIrreducible (f : ZPoly) : Decidable f.Irreducible

Equations

• f.instDecidableIrreducible = decidable_of_iff (f.isIrreducible = true) ⋯

@[simp]

theorem HexBerlekampZassenhausMathlib.irreducibleByFactorization_iff (f : Polynomial ℤ) : irreducibleByFactorization f = true ↔ Irreducible f

The executable factorization predicate agrees with Mathlib irreducibility over Polynomial ℤ.

@[instance_reducible]

instance HexBerlekampZassenhausMathlib.irreducibleDecidablePred : DecidablePred fun (f : Polynomial ℤ) => Irreducible f

Mathlib irreducibility over Polynomial ℤ is decidable through the executable Berlekamp-Zassenhaus factorization surface.

Equations

• HexBerlekampZassenhausMathlib.irreducibleDecidablePred f = if h : HexBerlekampZassenhausMathlib.irreducibleByFactorization f = true then isTrue ⋯ else isFalse ⋯