noncomputable def HexBerlekampZassenhausMathlib.cZ (m : UInt64) (f : Hex.ZPoly) : Polynomial (ZMod m.toNat)

Coefficient cast of an executable integer polynomial into ZMod m.toNat[X].

Equations

• HexBerlekampZassenhausMathlib.cZ m f = Polynomial.map (Int.castRingHom (ZMod m.toNat)) (HexPolyMathlib.toPolynomial f)

noncomputable def HexBerlekampZassenhausMathlib.cW {m : UInt64} (ctx : MontCtx m) (a : Hex.DensePoly (Hex.WordMod ctx)) : Polynomial (ZMod m.toNat)

Coefficient cast of an executable WordMod polynomial into ZMod m.toNat[X].

Equations

• HexBerlekampZassenhausMathlib.cW ctx a = Polynomial.map HexModArithMathlib.WordMod.toZModRingHom (HexPolyMathlib.toPolynomial a)

@[simp]

theorem HexBerlekampZassenhausMathlib.cZ_coeff (m : UInt64) (f : Hex.ZPoly) (j : ℕ) : (cZ m f).coeff j = ↑(Hex.DensePoly.coeff f j)

Coefficient rule for the integer-polynomial cast cZ.

@[simp]

theorem HexBerlekampZassenhausMathlib.cW_coeff {m : UInt64} (ctx : MontCtx m) (a : Hex.DensePoly (Hex.WordMod ctx)) (j : ℕ) : (cW ctx a).coeff j = HexModArithMathlib.WordMod.toZMod (a.coeff j)

Coefficient rule for the WordMod-polynomial cast cW.

theorem HexBerlekampZassenhausMathlib.cZ_mul (m : UInt64) (f g : Hex.ZPoly) : cZ m (f * g) = cZ m f * cZ m g

cZ is multiplicative.

theorem HexBerlekampZassenhausMathlib.cZ_add (m : UInt64) (f g : Hex.ZPoly) : cZ m (f + g) = cZ m f + cZ m g

cZ is additive.

theorem HexBerlekampZassenhausMathlib.cW_mul {m : UInt64} (ctx : MontCtx m) (a b : Hex.DensePoly (Hex.WordMod ctx)) : cW ctx (a * b) = cW ctx a * cW ctx b

cW is multiplicative.

theorem HexBerlekampZassenhausMathlib.cW_add {m : UInt64} (ctx : MontCtx m) (a b : Hex.DensePoly (Hex.WordMod ctx)) : cW ctx (a + b) = cW ctx a + cW ctx b

cW is additive.

theorem HexBerlekampZassenhausMathlib.eq_of_cZ_eq {m : UInt64} (x y : Hex.ZPoly) (hx : ∀ (i : ℕ), 0 ≤ Hex.DensePoly.coeff x i ∧ Hex.DensePoly.coeff x i < ↑m.toNat) (hy : ∀ (i : ℕ), 0 ≤ Hex.DensePoly.coeff y i ∧ Hex.DensePoly.coeff y i < ↑m.toNat) (h : cZ m x = cZ m y) : x = y

Canonical-representative uniqueness: two integer polynomials with all coefficients in [0, m) that are congruent mod m coefficientwise are equal.

theorem HexBerlekampZassenhausMathlib.map_divMod_monic {S : Type u_1} [CommRing S] [DecidableEq S] [Div S] {T : Type u_2} [CommRing T] (φ : S →+* T) (num g : Hex.DensePoly S) (hcancel : ∀ (a : S), a - a / g.leadingCoeff * g.leadingCoeff = 0) (hgmonic : (Polynomial.map φ (HexPolyMathlib.toPolynomial g)).Monic) (hdegmap : (Polynomial.map φ (HexPolyMathlib.toPolynomial g)).degree = (HexPolyMathlib.toPolynomial g).degree) (hdeg : (HexPolyMathlib.toPolynomial (num.divMod g).2).degree < (HexPolyMathlib.toPolynomial g).degree) : Polynomial.map φ (HexPolyMathlib.toPolynomial (num.divMod g).1) = Polynomial.map φ (HexPolyMathlib.toPolynomial num) /ₘ Polynomial.map φ (HexPolyMathlib.toPolynomial g)

Monic division commutes with a coefficient ring hom, in the target T[X]: the mapped executable quotient is the Mathlib monic-division quotient of the mapped inputs. Uniqueness (div_modByMonic_unique) does the work; the caller supplies the transported monic/degree facts.

theorem HexBerlekampZassenhausMathlib.intCast_intModNat (c : ℤ) (M : ℕ) (hM : 0 < M) : ↑(Hex.ZPoly.intModNat c M) = ↑c

The canonical natural representative intModNat casts back to the original residue in ZMod M.

def HexBerlekampZassenhausMathlib.toWMap {m : UInt64} (ctx : MontCtx m) (x : Hex.ZPoly) : Hex.DensePoly (Hex.WordMod ctx)

The word-mapped executable image toW = ofNat ∘ intModNat.

Equations

• HexBerlekampZassenhausMathlib.toWMap ctx x = Hex.DensePoly.ofCoeffs (Array.map (fun (c : ℤ) => Hex.WordMod.ofNat (Hex.ZPoly.intModNat c m.toNat)) (Hex.DensePoly.toArray x))

theorem HexBerlekampZassenhausMathlib.coeff_toWMap {m : UInt64} (ctx : MontCtx m) (x : Hex.ZPoly) (j : ℕ) : (toWMap ctx x).coeff j = Hex.WordMod.ofNat (Hex.ZPoly.intModNat (Hex.DensePoly.coeff x j) m.toNat)

Coefficient rule for toWMap.

theorem HexBerlekampZassenhausMathlib.cW_toWMap_eq_cZ {m : UInt64} (ctx : MontCtx m) (x : Hex.ZPoly) : cW ctx (toWMap ctx x) = cZ m x

cW of the toW-mapped image of an integer polynomial equals cZ of the original.

theorem HexBerlekampZassenhausMathlib.cZ_reduceModPow {m : UInt64} {p a : ℕ} (hpos : 0 < m.toNat) (hm : m.toNat = p ^ a) (x : Hex.ZPoly) : cZ m (x.reduceModPow p a) = cZ m x

Reduction mod p^a vanishes under the ZMod (p^a) cast.

theorem HexBerlekampZassenhausMathlib.cZ_derivative (m : UInt64) (x : Hex.ZPoly) : cZ m (Hex.DensePoly.derivative x) = Polynomial.derivative (cZ m x)

The ZMod cast commutes with the executable derivative.

theorem HexBerlekampZassenhausMathlib.cW_derivative {m : UInt64} (ctx : MontCtx m) (a : Hex.DensePoly (Hex.WordMod ctx)) : cW ctx a.derivative = Polynomial.derivative (cW ctx a)

The ZMod cast of a word-modular polynomial commutes with the executable derivative.

theorem HexBerlekampZassenhausMathlib.powLtWordAux_eq (p n acc r : ℕ) : Hex.powLtWordAux p n acc = some r → r = acc * p ^ n

A successful powLtWordAux run computes acc * p ^ n.

theorem HexBerlekampZassenhausMathlib.powLtWordAux_lt (p n acc r : ℕ) : acc < UInt64.word → Hex.powLtWordAux p n acc = some r → r < UInt64.word

A successful powLtWordAux run stays below the word bound.

theorem HexBerlekampZassenhausMathlib.powLtWord?_eq {p a mval : ℕ} (h : Hex.powLtWord? p a = some mval) : mval = p ^ a ∧ mval < UInt64.word

A successful powLtWord? guard certifies both the power value and the word bound.

theorem HexBerlekampZassenhausMathlib.toPoly_degree_lt {S : Type u_1} [CommRing S] [DecidableEq S] {r g : Hex.DensePoly S} (hg0 : HexPolyMathlib.toPolynomial g ≠ 0) (hlt : r.natDegree < g.natDegree) : (HexPolyMathlib.toPolynomial r).degree < (HexPolyMathlib.toPolynomial g).degree

Executable degree comparison transports to Mathlib degree comparison.

theorem HexBerlekampZassenhausMathlib.intModNat_lt (y : ℤ) (M : ℕ) (hM : 0 < M) : Hex.ZPoly.intModNat y M < M

The natural representative of an integer residue is below a positive modulus.

theorem HexBerlekampZassenhausMathlib.cldQuotientModWord?_eq (f g : Hex.ZPoly) (p a : ℕ) (hg : Hex.DensePoly.Monic g) (hgdeg : 0 < Hex.DensePoly.natDegree g) {mval : ℕ} (hpow : Hex.powLtWord? p a = some mval) (hodd : UInt64.ofNat mval % 2 = 1) (hm1 : 1 < mval) : Hex.cldQuotientModWord? f g p a = some (Hex.cldQuotientModBignum f g p a)

Word-sized and arbitrary-precision logarithmic-derivative quotients agree when the modulus fits.

theorem HexBerlekampZassenhausMathlib.cldQuotientMod_eq_spec (f g : Hex.ZPoly) (p a : ℕ) : Hex.cldQuotientMod f g p a = Hex.cldQuotientModBignum f g p a

The word-sized selection in cldQuotientMod agrees with the bignum reference cldQuotientModBignum for every input: the guard exactly matches the hypotheses of cldQuotientModWord?_eq, so on the fast path the word quotient is byte-identical and Option.getD returns it; off the fast path the bignum branch is taken.