def Hex.ZPoly.intModNat (z : Int) (m : Nat) : Nat

Canonical nonnegative representative of z modulo m.

Computes Int.toNat (z % m); for 0 < m this is the unique value in [0, m) congruent to z. Used coefficientwise by modP and reduceModPow to land integer coefficients in the standard representative window before transport to FpPoly or back into ZPoly.

Equations

• Hex.ZPoly.intModNat z m = (z % Int.ofNat m).toNat

def Hex.ZPoly.intModNatImpl (z : Int) (m : Nat) : Nat

Windowed implementation of intModNat.

Modular addition of canonical operands lands in [0, 2m) and modular subtraction in (-m, m), so on the modular hot path almost every coefficient is within one modulus of its canonical representative. Testing for that costs a bignum comparison and at most one bignum addition, where Int.emod costs a full division; a value already in [0, m) is returned without allocating at all. Only genuinely wide values -- products, and the descent from a doubled precision -- pay for the division.

Proved equal to intModNat in intModNat_eq_impl.

Equations

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

theorem Hex.ZPoly.intModNat_eq_impl_value (z : Int) (m : Nat) : intModNat z m = intModNatImpl z m

@[csimp]

theorem Hex.ZPoly.intModNat_eq_impl : intModNat = intModNatImpl

Proof-backed compiled implementation of the canonical representative.

def Hex.ZPoly.intEmod (z : Int) (m : Nat) : Int

Canonical nonnegative representative of z modulo m, as an Int.

The Int-valued sibling of intModNat, for the coefficient arrays that are Int-valued on both sides of a reduction.

Equations

• Hex.ZPoly.intEmod z m = Int.ofNat (Hex.ZPoly.intModNat z m)

def Hex.ZPoly.intEmodImpl (z : Int) (m : Nat) : Int

Windowed implementation of intEmod.

Routing through intModNat would cost a multi-limb copy on every coefficient, in both directions: Int.toNat copies a big nonnegative Int into a Nat, and the value is then immediately coerced back. Since Int.emod is already nonnegative at a nonzero modulus, that round trip is pure allocation, and allocation -- not division width -- is what the modular hot path is made of.

The two near-canonical windows are kept: modular addition of canonical operands lands in [0, 2m) and modular subtraction in (-m, m), so a coefficient already canonical is returned as itself, allocating nothing at all, and one within a modulus below costs a single addition. A genuinely wide value -- the long division's window, or the descent from a doubled precision -- pays for one Int.emod and nothing else.

Proved equal to intEmod in intEmod_eq_impl.

Equations

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

theorem Hex.ZPoly.intEmod_eq_impl_value (z : Int) (m : Nat) : intEmod z m = intEmodImpl z m

@[csimp]

theorem Hex.ZPoly.intEmod_eq_impl : intEmod = intEmodImpl

Proof-backed compiled implementation of the Int-valued canonical representative.

theorem Hex.ZPoly.intEmod_eq_emod (z : Int) {m : Nat} (hm : 0 < m) : intEmod z m = z % ↑m

At a positive modulus intEmod is the ordinary integer remainder.

theorem Hex.ZPoly.intEmod_mem (z : Int) {m : Nat} (hm : 0 < m) : 0 ≤ intEmod z m ∧ intEmod z m < ↑m

intEmod lands in the canonical window.

theorem Hex.ZPoly.intEmod_eq_self {z : Int} {m : Nat} (h0 : 0 ≤ z) (h1 : z < ↑m) : intEmod z m = z

A value already in the canonical window is returned unchanged.

theorem Hex.ZPoly.intEmod_congr {a b : Int} {m : Nat} (h : a % ↑m = b % ↑m) : intEmod a m = intEmod b m

Congruent integers have the same canonical representative.

theorem Hex.ZPoly.intEmod_sub_intEmod (a b : Int) {m : Nat} (hm : 0 < m) : intEmod (a - intEmod b m) m = intEmod (a - b) m

Reducing one summand first does not change the canonical representative of a difference: the windowed elimination may subtract the raw product where the specification subtracts its reduction.

def Hex.ZPoly.modP (p : Nat) [ZMod64.Bounds p] (f : ZPoly) : FpPoly p

Reduce the coefficients of an integer polynomial modulo p.

Equations

• Hex.ZPoly.modP p f = Hex.DensePoly.ofList (List.map (fun (i : Nat) => Hex.ZMod64.ofNat p (Hex.ZPoly.intModNat (Hex.DensePoly.coeff f i) p)) (List.range (Hex.DensePoly.size f)))

def Hex.ZPoly.modPImpl (p : Nat) [ZMod64.Bounds p] (f : ZPoly) : FpPoly p

Array-map implementation of coefficient reduction modulo p.

Equations

• Hex.ZPoly.modPImpl p f = Hex.FpPoly.ofCoeffs (Array.map (fun (coeff : Int) => Hex.ZMod64.ofNat p (Hex.ZPoly.intModNat coeff p)) (Hex.DensePoly.toArray f))

theorem Hex.ZPoly.modP_eq_impl_value (p : Nat) [ZMod64.Bounds p] (f : ZPoly) : modP p f = modPImpl p f

The direct array map computes the reference modular image.

theorem Hex.ZPoly.modP_eq_impl : modP = modPImpl

Exact direct-array implementation of reduction modulo p.

This equality is intentionally not a csimp rule: on the large reduction ladder the compiler's implementation of the list/range specification is materially faster than Array.map.

def Hex.ZPoly.reduceModPow (f : ZPoly) (p k : Nat) : ZPoly

Reduce each coefficient to its canonical representative modulo p^k.

Equations

• f.reduceModPow p k = Hex.DensePoly.ofList (List.map (fun (i : Nat) => Int.ofNat (Hex.ZPoly.intModNat (Hex.DensePoly.coeff f i) (p ^ k))) (List.range (Hex.DensePoly.size f)))

def Hex.ZPoly.reduceModPowImpl (f : ZPoly) (p k : Nat) : ZPoly

Array-map implementation of coefficient reduction modulo p^k.

Equations

• f.reduceModPowImpl p k = Hex.DensePoly.ofCoeffs (Array.map (fun (coeff : Int) => Hex.ZPoly.intEmod coeff (p ^ k)) (Hex.DensePoly.toArray f))

theorem Hex.ZPoly.reduceModPow_eq_impl_value (f : ZPoly) (p k : Nat) : f.reduceModPow p k = f.reduceModPowImpl p k

The direct array map computes the reference prime-power reduction.

@[csimp]

theorem Hex.ZPoly.reduceModPow_eq_impl : reduceModPow = reduceModPowImpl

Proof-backed compiled implementation of prime-power coefficient reduction.

@[simp]

theorem Hex.ZPoly.coeff_modP (p : Nat) [ZMod64.Bounds p] (f : ZPoly) (i : Nat) : DensePoly.coeff (modP p f) i = ZMod64.ofNat p (intModNat (DensePoly.coeff f i) p)

Coefficientwise characterisation of modP: the i-th coefficient of the reduction is the ZMod64 image of the canonical representative of the original coefficient.

@[simp]

theorem Hex.ZPoly.modP_zero (p : Nat) [ZMod64.Bounds p] : modP p 0 = 0

Reducing the zero polynomial modulo p preserves zero.

@[simp]

theorem Hex.ZPoly.coeff_reduceModPow (f : ZPoly) (p k i : Nat) : DensePoly.coeff (f.reduceModPow p k) i = Int.ofNat (intModNat (DensePoly.coeff f i) (p ^ k))

Coefficientwise characterisation of reduceModPow: each coefficient is replaced by its canonical nonnegative representative in [0, p^k).

@[simp]

theorem Hex.ZPoly.reduceModPow_zero (p k : Nat) : reduceModPow 0 p k = 0

Reducing the zero polynomial modulo p^k preserves zero.

@[simp]

theorem Hex.ZPoly.reduceModPow_one_of_nontrivial (p k : Nat) (hpk : 1 < p ^ k) : reduceModPow 1 p k = 1

Reducing the integer one polynomial modulo a nontrivial power preserves one.

theorem Hex.ZPoly.coeff_reduceModPow_eq_zero_of_emod (f : ZPoly) (p k i : Nat) (hzero : DensePoly.coeff f i % Int.ofNat (p ^ k) = 0) : DensePoly.coeff (f.reduceModPow p k) i = 0

If a coefficient is already divisible by p^k, its reduceModPow image vanishes.

theorem Hex.ZPoly.coeff_reduceModPow_eq_emod_of_pos (f : ZPoly) (p k i : Nat) (hpk : 0 < p ^ k) : DensePoly.coeff (f.reduceModPow p k) i = DensePoly.coeff f i % Int.ofNat (p ^ k)

For positive modulus p^k, the reduced coefficient equals the integer remainder f.coeff i % p^k. Identifies the Nat-valued executable representative with Int.emod.

theorem Hex.ZPoly.congr_reduceModPow (f : ZPoly) (p k : Nat) (hpk : 0 < p ^ k) : (f.reduceModPow p k).congr f (p ^ k)

Coefficientwise reduction modulo p^k is congruent to the original polynomial.

theorem Hex.ZPoly.congr_reduceModPow_of_congr (f g : ZPoly) (p k : Nat) (hfg : f.congr g (p ^ k)) : f.reduceModPow p k = g.reduceModPow p k

Congruence is preserved by coefficientwise canonical reduction modulo p^k.

theorem Hex.ZPoly.congr_of_dvd_modulus (f g : ZPoly) {m n : Nat} (hmn : m ∣ n) (hfg : f.congr g n) : f.congr g m

Congruence modulo a larger modulus descends along divisibility of moduli.

theorem Hex.ZPoly.congr_pow_of_le (p a b : Nat) (f g : ZPoly) (hab : a ≤ b) (hfg : f.congr g (p ^ b)) : f.congr g (p ^ a)

Congruence modulo p^b descends to congruence modulo p^a for a ≤ b.

theorem Hex.ZPoly.reduceModPow_eq_of_congr (f g : ZPoly) (p k : Nat) (hfg : f.congr g (p ^ k)) : f.reduceModPow p k = g.reduceModPow p k

Alias oriented toward canonical reduction: congruent inputs have the same reduction.

theorem Hex.ZPoly.reduceModPow_idempotent (f : ZPoly) (p k : Nat) (hpk : 0 < p ^ k) : (f.reduceModPow p k).reduceModPow p k = f.reduceModPow p k

Reducing twice to the same positive modulus is idempotent.

@[simp]

theorem Hex.ZPoly.reduceModPow_reduceModPow (p k : Nat) [ZMod64.Bounds p] (f : ZPoly) : (f.reduceModPow p k).reduceModPow p k = f.reduceModPow p k

Canonical reduction modulo a positive power is idempotent.

def Hex.ZPoly.Canonical (f : ZPoly) (m : Nat) : Prop

The coefficient-range invariant of the modular kernels: every coefficient of f is the canonical residue in [0, m).

This is the invariant a lift must carry in order to drop a canonicalisation: reduceModPow_eq_self_of_canonical says it is exactly the hypothesis under which reduceModPow is the identity.

Equations

• f.Canonical m = ∀ (i : Nat), 0 ≤ Hex.DensePoly.coeff f i ∧ Hex.DensePoly.coeff f i < ↑m

theorem Hex.ZPoly.canonical_reduceModPow (f : ZPoly) (p k : Nat) (hpk : 0 < p ^ k) : (f.reduceModPow p k).Canonical (p ^ k)

Canonical reduction at a positive modulus produces canonical coefficients.

theorem Hex.ZPoly.reduceModPow_eq_self_of_canonical (f : ZPoly) (p k : Nat) (hpk : 0 < p ^ k) (hf : f.Canonical (p ^ k)) : f.reduceModPow p k = f

Canonical coefficients are fixed by reduceModPow.

This is the theorem that licenses deleting a redundant canonicalisation: a reduction applied to data already reduced to [0, p ^ k) returns its input unchanged, so removing it cannot change any result.

theorem Hex.ZPoly.modP_eq_of_congr (p : Nat) [ZMod64.Bounds p] (f g : ZPoly) (hfg : f.congr g p) : modP p f = modP p g

Congruent integer polynomials have the same reduction modulo p.

@[simp]

theorem Hex.ZPoly.modP_reduceModPow (p k : Nat) [ZMod64.Bounds p] (f : ZPoly) : modP p (f.reduceModPow p (k + 1)) = modP p f

Reducing modulo p^(k+1) does not change the reduction modulo p.

@[simp]

theorem Hex.ZPoly.modP_reduceModPow_of_pos (p k : Nat) [ZMod64.Bounds p] (f : ZPoly) (hk : 0 < k) : modP p (f.reduceModPow p k) = modP p f

Reducing modulo any positive power of p does not change the reduction modulo p.

def Hex.FpPoly.liftToZ {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : ZPoly

Lift F_p coefficients to their standard nonnegative integer representatives.

Equations

• f.liftToZ = Hex.DensePoly.ofList (List.map (fun (i : Nat) => Int.ofNat (Hex.DensePoly.coeff f i).toNat) (List.range (Hex.DensePoly.size f)))

@[simp]

theorem Hex.FpPoly.coeff_liftToZ {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (i : Nat) : DensePoly.coeff f.liftToZ i = Int.ofNat (DensePoly.coeff f i).toNat

Coefficientwise characterisation of liftToZ: each coefficient is the standard nonnegative Nat representative of the corresponding ZMod64 element.

@[simp]

theorem Hex.FpPoly.liftToZ_zero {p : Nat} [ZMod64.Bounds p] : liftToZ 0 = 0

The canonical integer lift of the zero polynomial is zero.

theorem Hex.FpPoly.modP_liftToZ_coeff {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (i : Nat) : DensePoly.coeff (ZPoly.modP p f.liftToZ) i = DensePoly.coeff f i

Reducing the canonical lift back modulo p recovers the original coefficient data.

@[simp]

theorem Hex.FpPoly.modP_liftToZ {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : ZPoly.modP p f.liftToZ = f

Reducing a canonical lift back modulo p recovers the original polynomial.

theorem Hex.FpPoly.monic_liftToZ_of_monic {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hp : 1 < p) (hf : DensePoly.Monic f) : DensePoly.Monic f.liftToZ

The canonical integer lift of a monic polynomial over F_p is monic, provided the modulus is nontrivial. The 1 < p hypothesis is necessary because 1 : ZMod64 1 has representative zero.

theorem Hex.FpPoly.congr_liftToZ_modP {p : Nat} [ZMod64.Bounds p] (f : ZPoly) : (ZPoly.modP p f).liftToZ.congr f p

A polynomial is congruent modulo p to the canonical integer lift of its reduction.

@[simp]

theorem Hex.ZPoly.modP_one (p : Nat) [ZMod64.Bounds p] : modP p 1 = 1

Reducing the integer 1 polynomial modulo p yields the FpPoly p identity. Bottom-of-recursion case for the modP p rewrites used by Hensel lifting modules.