hex

17.5. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexBerlekampMathlib is the companion that transports it: toMathlibPolynomial maps a Hex.FpPoly to Polynomial (ZMod p), and the executable checks become statements about Mathlib's Irreducible predicate on the transported polynomial.

The headline equivalence takes an arbitrary input. The computable test HexBerlekampMathlib.fpIsIrreducible normalizes to a monic polynomial, runs Rabin's test on it, and agrees exactly with Mathlib irreducibility:

🔗theorem
HexBerlekampMathlib.fpIsIrreducible_iff {p : ℕ} [Hex.ZMod64.Bounds p]
  [Fact (Nat.Prime p)] (f : Hex.FpPoly p) :
  HexBerlekampMathlib.fpIsIrreducible f = true ↔
    Irreducible (HexPolyFpMathlib.toMathlibPolynomial f)
HexBerlekampMathlib.fpIsIrreducible_iff
  {p : ℕ} [Hex.ZMod64.Bounds p]
  [Fact (Nat.Prime p)]
  (f : Hex.FpPoly p) :
  HexBerlekampMathlib.fpIsIrreducible f =
      true ↔
    Irreducible
      (HexPolyFpMathlib.toMathlibPolynomial
        f)

The computable Rabin-backed test agrees with Mathlib irreducibility of the transported polynomial over ZMod p.

For nonzero f the monic normalization m = (normalizeMonic f).2 is a unit multiple of f (f = leadingCoeff f • m up to C), so irreducibility of toMathlibPolynomial m and of toMathlibPolynomial f coincide; rabin_irreducible supplies the former for the monic m (also in the constant case, where both the Rabin test and Mathlib irreducibility are false).

For a monic input the equivalence is Rabin's criterion itself, in both directions: the test succeeds exactly on the irreducible polynomials. The forward direction is what certificate checking uses; the reverse direction says the test never misses.

🔗theorem
HexBerlekampMathlib.rabin_irreducible {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) (hmonic : Hex.DensePoly.Monic f)
  [Fact (Nat.Prime p)] (n : ℕ)
  (hdegree : Hex.Berlekamp.basisSize f = n) :
  Hex.Berlekamp.rabinTest f hmonic = true ↔
    Irreducible (HexPolyFpMathlib.toMathlibPolynomial f)
HexBerlekampMathlib.rabin_irreducible
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic f)
  [Fact (Nat.Prime p)] (n : ℕ)
  (hdegree :
    Hex.Berlekamp.basisSize f = n) :
  Hex.Berlekamp.rabinTest f hmonic =
      true ↔
    Irreducible
      (HexPolyFpMathlib.toMathlibPolynomial
        f)

Rabin's executable test is equivalent to Mathlib irreducibility for the transported polynomial.

Factorization transports factor by factor. On a monic square-free input of positive degree, every entry of the list returned by Hex.Berlekamp.berlekampFactor is irreducible in Mathlib's sense. Together with the Mathlib-free product theorem Hex.Berlekamp.prod_berlekampFactor above, the returned list is a complete factorization into Mathlib irreducibles.

🔗theorem
HexBerlekampMathlib.irreducible_of_mem_berlekampFactor {p : ℕ}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic f) [Hex.ZMod64.PrimeModulus p]
  [Fact (Nat.Prime p)] (hf_pos : 0 < Hex.DensePoly.natDegree f)
  (hsquareFree :
    ∀ (d : Hex.FpPoly p),
      d ∣ f →
        d ∣ Hex.DensePoly.derivative f →
          Hex.Berlekamp.isUnitPolynomial d = true)
  (g : Hex.FpPoly p) :
  g ∈ (Hex.Berlekamp.berlekampFactor f hmonic).factors →
    Irreducible (HexPolyFpMathlib.toMathlibPolynomial g)
HexBerlekampMathlib.irreducible_of_mem_berlekampFactor
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic f)
  [Hex.ZMod64.PrimeModulus p]
  [Fact (Nat.Prime p)]
  (hf_pos : 0 < Hex.DensePoly.natDegree f)
  (hsquareFree :
    ∀ (d : Hex.FpPoly p),
      d ∣ f →
        d ∣ Hex.DensePoly.derivative f →
          Hex.Berlekamp.isUnitPolynomial
              d =
            true)
  (g : Hex.FpPoly p) :
  g ∈
      (Hex.Berlekamp.berlekampFactor f
          hmonic).factors →
    Irreducible
      (HexPolyFpMathlib.toMathlibPolynomial
        g)

Every factor emitted by executable Berlekamp factorization on a positive-degree input is irreducible after transport to Mathlib's polynomial model, assuming the square-free input in the common-divisor form used by the executable soundness chain. The positive-degree input hypothesis is essential: emitted factors of a constant input are themselves constant, transporting to Mathlib units rather than irreducibles.

The proof boundary follows the import boundary. The executable library proves what is statable without Mathlib: the product identity, degree accounting, and the loop invariants of the factor loop. The companion supplies the finite-field theory, such as the existence and subfield structure of 𝔽_(p^n) behind Rabin's criterion, that reads those checks as irreducibility.