theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_mul {p : ℕ} [Hex.ZMod64.Bounds p] (a b : Hex.FpPoly p) : HexPolyFpMathlib.toMathlibPolynomial (a * b) = HexPolyFpMathlib.toMathlibPolynomial a * HexPolyFpMathlib.toMathlibPolynomial b

Executable FpPoly p multiplication transports to Mathlib multiplication through HexBerlekampMathlib.fpPolyEquiv.

theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_one {p : ℕ} [Hex.ZMod64.Bounds p] : HexPolyFpMathlib.toMathlibPolynomial 1 = 1

The executable 1 : FpPoly p transports to Mathlib's 1.

theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_C {p : ℕ} [Hex.ZMod64.Bounds p] (c : Hex.ZMod64 p) : HexPolyFpMathlib.toMathlibPolynomial (Hex.DensePoly.C c) = Polynomial.C (HexModArithMathlib.ZMod64.toZMod c)

The executable constant polynomial DensePoly.C c transports to Mathlib's Polynomial.C of the ZMod p cast of c.

theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_scale {p : ℕ} [Hex.ZMod64.Bounds p] (c : Hex.ZMod64 p) (f : Hex.FpPoly p) : HexPolyFpMathlib.toMathlibPolynomial (Hex.DensePoly.scale c f) = Polynomial.C (HexModArithMathlib.ZMod64.toZMod c) * HexPolyFpMathlib.toMathlibPolynomial f

Coefficientwise scaling on FpPoly p transports across HexBerlekampMathlib.toMathlibPolynomial to multiplication by the corresponding Polynomial.C of the ZMod p cast.

theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_listFoldlMul_one {p : ℕ} [Hex.ZMod64.Bounds p] (xs : List (Hex.FpPoly p)) : HexPolyFpMathlib.toMathlibPolynomial (List.foldl (fun (x1 x2 : Hex.FpPoly p) => x1 * x2) 1 xs) = (List.map HexPolyFpMathlib.toMathlibPolynomial xs).prod

List foldl (· * ·) of executable FpPoly p factors transports across HexBerlekampMathlib.toMathlibPolynomial to the explicit Mathlib List.prod of the per-factor transports.

theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_factorProduct (primeData : Hex.PrimeFactorData) : HexPolyFpMathlib.toMathlibPolynomial primeData.factorProduct = (List.map HexPolyFpMathlib.toMathlibPolynomial primeData.factorPolys.toList).prod

The Mathlib transport of Hex.PrimeFactorData.factorProduct is the Mathlib List.prod of the recorded factor transports.

theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_modP_eq_map_intCast_zmod {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.ZPoly) : HexPolyFpMathlib.toMathlibPolynomial (Hex.ZPoly.modP p f) = Polynomial.map (Int.castRingHom (ZMod p)) (HexPolyZMathlib.toPolynomial f)

Coefficientwise reduction Hex.ZPoly.modP transports to Mathlib's coefficient map from ℤ[X] to (ZMod p)[X]. This keeps certificate soundness independent of the integer-reduction branch proofs.

theorem HexBerlekampZassenhausMathlib.toMathlibPolynomial_factorProduct_eq_map_intCast_zmod (f : Hex.ZPoly) (primeData : Hex.PrimeFactorData) (hcheck : Hex.PrimeFactorData.checkForPolynomial f primeData = true) : HexPolyFpMathlib.toMathlibPolynomial primeData.factorProduct = Polynomial.map (Int.castRingHom (ZMod primeData.p)) (HexPolyZMathlib.toPolynomial f)

A successful PrimeFactorData.checkForPolynomial block exposes the Mathlib factor-product / modular-image alignment: the Mathlib transport of the recorded factorProduct equals the Mathlib Polynomial.map (Int.castRingHom (ZMod p)) image of the underlying integer polynomial.

theorem HexBerlekampZassenhausMathlib.map_intCast_zmod_toPolynomial_eq_factorPolys_product (f : Hex.ZPoly) (primeData : Hex.PrimeFactorData) (hcheck : Hex.PrimeFactorData.checkForPolynomial f primeData = true) : Polynomial.map (Int.castRingHom (ZMod primeData.p)) (HexPolyZMathlib.toPolynomial f) = (List.map HexPolyFpMathlib.toMathlibPolynomial primeData.factorPolys.toList).prod

A successful PrimeFactorData.checkForPolynomial block exposes the Mathlib modular image of the underlying integer polynomial as the explicit product of recorded factor transports.

This is the shape used by the integer irreducibility certificate soundness composition: the Mathlib (toPolynomial f).map (Int.castRingHom (ZMod p)) factors through the explicit Mathlib List.prod of executable monic factor transports, enabling UFD-level identification of factor degrees against factorDegrees.