theorem HexBerlekampMathlib.natDegree_toMathlibPolynomial_eq_basisSize {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : (toMathlibPolynomial f).natDegree = Hex.Berlekamp.basisSize f

The executable Berlekamp basis size is the Mathlib natural degree after transport. This is the algorithm-facing specialization of the representation theorem natDegree_toMathlibPolynomial.

theorem HexBerlekampMathlib.isUnit_toMathlibPolynomial_of_isUnitPolynomial {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] {g : Hex.FpPoly p} (h : Hex.Berlekamp.isUnitPolynomial g = true) : IsUnit (toMathlibPolynomial g)

An executable unit polynomial (a nonzero constant) transports to a Mathlib unit.

theorem HexBerlekampMathlib.irreducible_toMathlibPolynomial_of_fpPolyIrreducible {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] {f : Hex.FpPoly p} (hpos : 0 < (toMathlibPolynomial f).natDegree) (hirr : f.Irreducible) : Irreducible (toMathlibPolynomial f)

Transport executable FpPoly.Irreducible to Mathlib Irreducible over ZMod p.

The positive Mathlib-degree hypothesis is essential: FpPoly.Irreducible holds vacuously for any nonzero constant (every factorization has a degree-0 factor), whereas such a constant transports to a Mathlib unit, not an irreducible. At the Berlekamp use site the emitted factors are nonconstant, so the hypothesis is available.

theorem HexBerlekampMathlib.isCoprime_toMathlibPolynomial_of_isUnitPolynomial_gcd {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] {a b : Hex.FpPoly p} (h : Hex.Berlekamp.isUnitPolynomial (Hex.DensePoly.gcd a b) = true) : IsCoprime (toMathlibPolynomial a) (toMathlibPolynomial b)

A passing executable gcd-unit check transports to Mathlib coprimality of the transported polynomials, via the executable Bezout identity.

@[reducible, inline]

noncomputable abbrev HexBerlekampMathlib.Rabin.frobeniusPolynomial (p n : ℕ) : Polynomial (ZMod p)

The Mathlib polynomial X^(p^n) - X used by Rabin's divisibility leg.

Equations

• HexBerlekampMathlib.Rabin.frobeniusPolynomial p n = Polynomial.X ^ p ^ n - Polynomial.X

theorem HexBerlekampMathlib.Rabin.toMathlibPolynomial_xPowSubX {p : ℕ} [Hex.ZMod64.Bounds p] (k : ℕ) : toMathlibPolynomial (Hex.Berlekamp.xPowSubX k) = frobeniusPolynomial p k

The executable absolute polynomial X^(p^k) - X transports to frobeniusPolynomial p k.

theorem HexBerlekampMathlib.Rabin.natDegree_dvd_of_irreducible_dvd_frobeniusPolynomial {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] {n : ℕ} {g : Polynomial (ZMod p)} (hg_irreducible : Irreducible g) (hg_dvd : g ∣ frobeniusPolynomial p n) : g.natDegree ∣ n

The Rabin finite-field degree lemma in the local ZMod p form used by the contrapositive proof.

theorem HexBerlekampMathlib.Rabin.irreducible_dvd_of_not_isCoprime {p : ℕ} [Fact (Nat.Prime p)] {g P : Polynomial (ZMod p)} (hg_irreducible : Irreducible g) (hnot_coprime : ¬IsCoprime g P) : g ∣ P

For an irreducible polynomial, any nontrivial gcd/coprimality failure with P forces divisibility by P.

theorem HexBerlekampMathlib.Rabin.irreducible_dvd_frobeniusPolynomial_of_natDegree_dvd {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] {g : Polynomial (ZMod p)} (hg_irreducible : Irreducible g) {N : ℕ} (hdvd : g.natDegree ∣ N) : g ∣ frobeniusPolynomial p N

The Rabin backward direction in the local ZMod p form: every irreducible polynomial of degree dividing N divides X^(p^N) - X.

Used by the contrapositive direction of rabinTest_true_irreducible to lift divisibility of an irreducible factor g from the basis-size Frobenius polynomial down to the Frobenius polynomial at a maximal proper divisor.

theorem HexBerlekampMathlib.Rabin.maximalProperDivisors_pos {n d : ℕ} (hmem : d ∈ Hex.Berlekamp.maximalProperDivisors n) : 0 < d

Maximal proper divisors are positive.

theorem HexBerlekampMathlib.Rabin.maximalProperDivisors_lt {n d : ℕ} (hmem : d ∈ Hex.Berlekamp.maximalProperDivisors n) : d < n

Maximal proper divisors are strictly below the ambient degree.

theorem HexBerlekampMathlib.Rabin.rabinTest_true_to_mathlib_checks {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) (htest : Hex.Berlekamp.rabinTest f hmonic = true) : 0 < n ∧ toMathlibPolynomial f ∣ frobeniusPolynomial p n ∧ ∀ d ∈ Hex.Berlekamp.maximalProperDivisors n, IsCoprime (toMathlibPolynomial f) (frobeniusPolynomial p d)

The executable Rabin test passing entails the exact Mathlib divisibility and coprimality checks appearing in Rabin's criterion.

theorem HexBerlekampMathlib.Rabin.rabinTest_true_of_mathlib_checks {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) (hchecks : 0 < n ∧ toMathlibPolynomial f ∣ frobeniusPolynomial p n ∧ ∀ d ∈ Hex.Berlekamp.maximalProperDivisors n, IsCoprime (toMathlibPolynomial f) (frobeniusPolynomial p d)) : Hex.Berlekamp.rabinTest f hmonic = true

The Mathlib Rabin checks imply the executable test surface once the transport lemmas connect executable remainders and gcds to Polynomial (ZMod p).

theorem HexBerlekampMathlib.toMathlibPolynomial_gcd_associated {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] (f g : Hex.FpPoly p) : Associated (toMathlibPolynomial (Hex.DensePoly.gcd f g)) (gcd (toMathlibPolynomial f) (toMathlibPolynomial g))

Executable gcd is associated to Mathlib's gcd after coefficient transport.

toMathlibPolynomial = fpPolyEquiv is a ring iso, so executable divisibility transports both ways; feeding the executable GcdLaws through it shows the transported gcd satisfies Mathlib's gcd universal property. The two are only associated, not equal, because the executable gcd is the last nonzero xgcd remainder with no monic rescale while Mathlib's gcd is normalize-canonical.

theorem HexBerlekampMathlib.toMathlibPolynomial_squareFree_coprime {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] (f : Hex.FpPoly p) (hsquareFree : Hex.Berlekamp.isUnitPolynomial (Hex.DensePoly.gcd f (Hex.DensePoly.derivative f)) = true) : IsCoprime (toMathlibPolynomial f) (Polynomial.derivative (toMathlibPolynomial f))

The executable square-free hypothesis used by Berlekamp is the corresponding Mathlib coprimality condition between the transported polynomial and its formal derivative.

theorem HexBerlekampMathlib.natDegree_toMathlibPolynomial_pos_of_degree?_pos {p : ℕ} [Hex.ZMod64.Bounds p] {g : Hex.FpPoly p} (hg : 0 < Hex.DensePoly.natDegree g) : 0 < (toMathlibPolynomial g).natDegree

A factor with positive executable degree transports to a Mathlib polynomial of positive natDegree: its leading coefficient is nonzero and the (injective) coefficient transport preserves that, so the top coefficient survives.

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 (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.

theorem HexBerlekampMathlib.irreducible_of_mem_berlekampFactor_of_gcd_eq_one {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 : Hex.DensePoly.gcd f (Hex.DensePoly.derivative f) = 1) (g : Hex.FpPoly p) : g ∈ (Hex.Berlekamp.berlekampFactor f hmonic).factors → Irreducible (toMathlibPolynomial g)

Every factor emitted by executable Berlekamp factorization is irreducible after transport to Mathlib's polynomial model.

theorem HexBerlekampMathlib.irreducible_of_berlekampFactor_factors_length_le_one {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 : Hex.Berlekamp.isUnitPolynomial (Hex.DensePoly.gcd f (Hex.DensePoly.derivative f)) = true) (hsmall : (Hex.Berlekamp.berlekampFactor f hmonic).factors.length ≤ 1) : Irreducible (toMathlibPolynomial f)

If executable Berlekamp factorization cannot split a monic square-free input, then the input itself is irreducible after transport to Mathlib.

The executable factor list is never empty; with length at most one, its head is therefore a member of the Berlekamp output, so the existing per-emitted-factor irreducibility theorem applies directly.

theorem HexBerlekampMathlib.rabinTest_true_irreducible {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) (hmonic : Hex.DensePoly.Monic f) [Fact (Nat.Prime p)] : Hex.Berlekamp.rabinTest f hmonic = true → Irreducible (toMathlibPolynomial f)

Forward Rabin soundness: when the executable Rabin test accepts, the transported Mathlib polynomial is irreducible.

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 (toMathlibPolynomial f)

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

@[instance_reducible]

instance HexBerlekampMathlib.instDecidableMonic {p : ℕ} [Hex.ZMod64.Bounds p] (m : Hex.FpPoly p) : Decidable (Hex.DensePoly.Monic m)

Monicity of an executable finite-field polynomial is decidable: Monic m is the equality leadingCoeff m = 1, and ZMod64 p has decidable equality. This is the instance that lets the Bool-valued fpIsIrreducible branch on monicity and still reduce in the kernel.

Equations

• HexBerlekampMathlib.instDecidableMonic m = HexBerlekampMathlib.instDecidableMonic._aux_1 m

def HexBerlekampMathlib.fpIsIrreducible {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : Bool

Computable, kernel-reducible irreducibility test for finite-field polynomials, backed by Berlekamp.rabinTest on the monic normalization.

Zero inputs are rejected; every nonzero f normalizes to a monic polynomial (normalizeMonic f).2 whose Rabin test decides irreducibility. decide +kernel reduces this test in the kernel, so via fpIsIrreducible_iff and instDecidableIrreducibleToMathlibPolynomial it certifies Irreducible (toMathlibPolynomial f) using only the kernel.

Equations

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

theorem HexBerlekampMathlib.fpIsIrreducible_iff {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] (f : Hex.FpPoly p) : fpIsIrreducible f = true ↔ Irreducible (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).

@[instance_reducible]

instance HexBerlekampMathlib.instDecidableIrreducibleToMathlibPolynomial {p : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] (f : Hex.FpPoly p) : Decidable (Irreducible (toMathlibPolynomial f))

Mathlib irreducibility of a transported finite-field polynomial is decidable by a kernel-reducible computation: decide +kernel runs fpIsIrreducible (hence Berlekamp.rabinTest) in the kernel and reads off the verdict.

Equations

• HexBerlekampMathlib.instDecidableIrreducibleToMathlibPolynomial f = decidable_of_iff (HexBerlekampMathlib.fpIsIrreducible f = true) ⋯