theorem HexPolyFpMathlib.hexPrime_of_fact (p : ℕ) [Fact (Nat.Prime p)] : Hex.Nat.Prime p

Mathlib's Nat.Prime fact yields the executable prime predicate, so the executable square-free decomposition (which consumes Hex.Nat.Prime p) can be invoked in a context carrying only the Mathlib-side hypothesis.

theorem HexPolyFpMathlib.pow_eq_pow {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) (n : ℕ) : f.pow n = f ^ n

The executable square-and-multiply power is Mathlib's monoid power, the sibling of linearPow_eq_pow for the exponentiation the compiled square-free path actually runs.

theorem HexPolyFpMathlib.weightedProduct_eq_prod {p : ℕ} [Hex.ZMod64.Bounds p] (factors : List (Hex.FpPoly.SquareFreeFactor p)) : Hex.FpPoly.weightedProduct factors = (List.map (fun (sf : Hex.FpPoly.SquareFreeFactor p) => sf.factor ^ sf.multiplicity) factors).prod

The executable weighted factor product is the Mathlib list product of the factors raised to their multiplicities, still on the executable side of the correspondence.

theorem HexPolyFpMathlib.toMathlibPolynomial_weightedProduct {p : ℕ} [Hex.ZMod64.Bounds p] (factors : List (Hex.FpPoly.SquareFreeFactor p)) : toMathlibPolynomial (Hex.FpPoly.weightedProduct factors) = (List.map (fun (sf : Hex.FpPoly.SquareFreeFactor p) => toMathlibPolynomial sf.factor ^ sf.multiplicity) factors).prod

The weighted factor product transports to the Mathlib list product of the transported factors raised to their multiplicities.

theorem HexPolyFpMathlib.isCoprime_toMathlibPolynomial_of_normalizeMonic_gcd_eq_one {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] {a b : Hex.FpPoly p} (h : (Hex.FpPoly.normalizeMonic (Hex.DensePoly.gcd a b)).2 = 1) : IsCoprime (toMathlibPolynomial a) (toMathlibPolynomial b)

The executable square-free layer's coprimality certificate — the monic normalization of the executable gcd reducing to 1 — transports to Mathlib coprimality, via the executable Bezout identity. This is the hex-poly-fp counterpart of hex-berlekamp-mathlib's isCoprime_toMathlibPolynomial_of_isUnitPolynomial_gcd, keyed on the gcd-unit phrasing the Yun theorems emit rather than Berlekamp's isUnitPolynomial.

theorem HexPolyFpMathlib.squarefree_toMathlibPolynomial_of_normalizeMonic_gcd_eq_one {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] {g : Hex.FpPoly p} (h : (Hex.FpPoly.normalizeMonic (Hex.DensePoly.gcd g (Hex.DensePoly.derivative g))).2 = 1) : Squarefree (toMathlibPolynomial g)

The executable square-freeness certificate — the monic normalization of gcd g (derivative g) reducing to 1 — transports to Mathlib Squarefree: coprimality with the formal derivative is Polynomial.Separable, and separable polynomials are square-free.

theorem HexPolyFpMathlib.squareFreeDecomposition_correct {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] (hp : Hex.Nat.Prime p) (f : Hex.FpPoly p) : have d := Hex.FpPoly.squareFreeDecomposition hp f; Polynomial.C (HexModArithMathlib.ZMod64.toZMod d.unit) * (List.map (fun (sf : Hex.FpPoly.SquareFreeFactor p) => toMathlibPolynomial sf.factor ^ sf.multiplicity) d.factors).prod = toMathlibPolynomial f ∧ (∀ sf ∈ d.factors, Squarefree (toMathlibPolynomial sf.factor)) ∧ List.Pairwise (fun (a b : Hex.FpPoly.SquareFreeFactor p) => IsCoprime (toMathlibPolynomial a.factor) (toMathlibPolynomial b.factor)) d.factors ∧ ∀ sf ∈ d.factors, 0 < sf.multiplicity

Headline correctness theorem for hex-poly-fp: the executable Yun square-free decomposition is a genuine square-free decomposition in Polynomial (ZMod p).

For a prime modulus and any input f, writing d for the decomposition:

• reconstruction — the constant C d.unit times the product of the transported factors, each raised to its recorded multiplicity, is the transport of f;

• square-freeness — every transported factor is Squarefree;

• pairwise coprimality — the transported factors are pairwise IsCoprime;

• positive multiplicities — every recorded multiplicity is positive.

No nonzeroness or degree hypothesis on f is required: the executable theorems cover the degenerate cases (for f = 0 the emitted unit is 0), and the statement transports them unchanged. Built from the Mathlib-free post-conditions squareFreeDecomposition_weightedProduct, squareFreeDecomposition_factors_squareFree, squareFreeDecomposition_pairwise_coprime, and squareFreeDecomposition_multiplicity_pos, with the gcd-unit certificates converted through the executable Bezout identity.