theorem HexBerlekampZassenhausMathlib.toPolynomial_X : HexPolyZMathlib.toPolynomial (Hex.DensePoly.ofCoeffs #[0, 1]) = Polynomial.X

toPolynomial sends the executable X (the dense coefficient array #[0, 1]) to Mathlib's Polynomial.X.

theorem HexBerlekampZassenhausMathlib.toPolynomial_listProd (l : List Hex.ZPoly) : HexPolyZMathlib.toPolynomial l.prod = (List.map HexPolyZMathlib.toPolynomial l).prod

List products commute with the integer polynomial transport.

theorem HexBerlekampZassenhausMathlib.zpolyIrreducible_of_checkIrreducibleCertLinear (f : Hex.ZPoly) (cert : Hex.ZPolyIrreducibilityCertificate) (hprime : (cert.perPrime.all fun (primeData : Hex.PrimeFactorData) => decide (Nat.Prime primeData.p)) = true) (hcontent : decide (f.content = 1) = true) (hpos : decide (0 < Hex.DensePoly.natDegree f) = true) (hcert : Hex.checkIrreducibleCertLinear f cert = true) : f.Irreducible

The decide-slot form of checkIrreducibleCertLinear soundness concluding in the free layer: the same four Boolean hypotheses as irreducible_of_checkIrreducibleCertLinear, with the Mathlib-free Hex.ZPoly.Irreducible conclusion transported back through the unconditional Irreducible_iff_polynomialIrreducible.

def HexBerlekampZassenhausMathlib.checkMultiPrimeCert (f : Hex.ZPoly) (cert : Hex.ZPolyIrreducibilityCertificate) : Bool

Kernel-decidable check that a multi-prime certificate witnesses irreducibility of f: primality of the recorded block primes, content one, positive executable degree, and the incremental pow-chain replay checkIrreducibleCertLinear; the four hypothesis slots of zpolyIrreducible_of_checkIrreducibleCertLinear as one Boolean.

Equations

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

theorem HexBerlekampZassenhausMathlib.zpolyIrreducible_of_checkMultiPrimeCert (f : Hex.ZPoly) (cert : Hex.ZPolyIrreducibilityCertificate) (hcheck : checkMultiPrimeCert f cert = true) : f.Irreducible

A passing checkMultiPrimeCert forces free-layer irreducibility.

def HexBerlekampZassenhausMathlib.checkMultiPrimeCover (factors : List Hex.ZPoly) (certified : List (Hex.ZPoly × Hex.ZPoly.IrredWitness)) (multiPrime : List (Hex.ZPoly × Hex.ZPolyIrreducibilityCertificate)) : Bool

Bulk kernel-decidable irreducibility for a ZPoly factor list with repetition, mixing witness kinds: certified carries free-layer IrredWitness entries, multiPrime carries multi-prime degree-obstruction certificates for balanced factors, and every factor must match one of the two lists by beqCoeffs.

Equations

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

theorem HexBerlekampZassenhausMathlib.irreducible_of_checkMultiPrimeCover (factors : List Hex.ZPoly) (certified : List (Hex.ZPoly × Hex.ZPoly.IrredWitness)) (multiPrime : List (Hex.ZPoly × Hex.ZPolyIrreducibilityCertificate)) (hcheck : checkMultiPrimeCover factors certified multiPrime = true) (q : Hex.ZPoly) : q ∈ factors → q.Irreducible

A passing checkMultiPrimeCover forces free-layer irreducibility of every listed factor.

theorem Hex.ZPoly.irreducible_of_decide (f : ZPoly) (h : decide f.Irreducible = true) : f.Irreducible

Decide-slot endpoint for the irreducibility! kernel fallback on Hex.ZPoly: the kernel replays the full factorizer through Hex.ZPoly.instDecidableIrreducible. Emitted only by the bang forms; see their docstrings for the cost and import all closure caveats.

theorem Hex.ZPoly.forall_irreducible_of_decide (l : List ZPoly) (h : decide (∀ q ∈ l, q.Irreducible) = true) (q : ZPoly) : q ∈ l → q.Irreducible

Bulk decide-slot endpoint for the factor_poly! kernel fallback on Hex.ZPoly: one kernel factorizer replay per listed factor.

theorem HexBerlekampZassenhausMathlib.irreducible_ofZ_decide (P : Polynomial ℤ) (f : Hex.ZPoly) (h : decide f.Irreducible = true) (hP : HexPolyZMathlib.toPolynomial f = P) : Irreducible P

Decide-slot endpoint for the irreducibility! kernel fallback on Polynomial ℤ: the free-layer kernel replay transported through the unconditional iff and the parser-built translation equality.

theorem HexBerlekampZassenhausMathlib.irreducible_ofZ (P : Polynomial ℤ) (f : Hex.ZPoly) (certified : List (Hex.ZPoly × Hex.ZPoly.IrredWitness)) (multiPrime : List (Hex.ZPoly × Hex.ZPolyIrreducibilityCertificate)) (hcover : checkMultiPrimeCover [f] certified multiPrime = true) (hP : HexPolyZMathlib.toPolynomial f = P) : Irreducible P

Single-polynomial endpoint for the irreducibility extension on Polynomial ℤ: the cover check on the singleton factor list accepts either witness kind, and hP is the parser-built translation equality.

noncomputable def Hex.FactoredPoly.ofZ (P : Polynomial ℤ) (f : ZPoly) (s : ℤ) (factors : List ZPoly) (certified : List (ZPoly × ZPoly.IrredWitness)) (multiPrime : List (ZPoly × ZPolyIrreducibilityCertificate)) (hmul : (DensePoly.C s * factors.prod).beqCoeffs f = true) (hcover : HexBerlekampZassenhausMathlib.checkMultiPrimeCover factors certified multiPrime = true) (hP : HexPolyZMathlib.toPolynomial f = P) : FactoredPoly P

One-shot assembler for the factor_poly extension on Polynomial ℤ: every certification slot is a Boolean check on reified literal data (filled by Eq.refl true in emitted terms), and hP is the parser-built translation equality tying the reified executable polynomial to the user's Mathlib polynomial.

Equations

• Hex.FactoredPoly.ofZ P f s factors certified multiPrime hmul hcover hP = { scalar := s, factors := List.map HexPolyZMathlib.toPolynomial factors, factors_mul := ⋯, factors_irred := ⋯ }

noncomputable def Hex.FactoredPoly.ofZDecide (P : Polynomial ℤ) (f : ZPoly) (s : ℤ) (factors : List ZPoly) (hmul : (DensePoly.C s * factors.prod).beqCoeffs f = true) (hirr : decide (∀ q ∈ factors, q.Irreducible) = true) (hP : HexPolyZMathlib.toPolynomial f = P) : FactoredPoly P

Decide-slot assembler for the factor_poly! kernel fallback on Polynomial ℤ: the factors_irred slot replays the full factorizer in the kernel once per factor. Emitted only by the bang forms.

Equations

• Hex.FactoredPoly.ofZDecide P f s factors hmul hirr hP = { scalar := s, factors := List.map HexPolyZMathlib.toPolynomial factors, factors_mul := ⋯, factors_irred := ⋯ }