13.2. Coefficientwise reduction🔗

Every lift step works modulo a fixed modulus, so the primitive operation is reduction of each integer coefficient to its canonical representative in [0, modulus). Hex.ZPoly.reduceModPow reduces modulo a prime power p^k, and Hex.QuadraticLiftResult.reduceModSquare is the squaring-step specialization that reduces modulo m^2.

def

Hex.ZPoly.reduceModPow (f : Hex.ZPoly) (p k : ℕ) : Hex.ZPoly
Hex.ZPoly.reduceModPow (f : Hex.ZPoly)
  (p k : ℕ) : Hex.ZPoly

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

def

Hex.QuadraticLiftResult.reduceModSquare (f : Hex.ZPoly) (m : ℕ) :
  Hex.ZPoly
Hex.QuadraticLiftResult.reduceModSquare
  (f : Hex.ZPoly) (m : ℕ) : Hex.ZPoly

Canonical coefficient reduction modulo m^2.

The reduced polynomial is congruent to the original modulo the modulus. Every later step relies on this to preserve the factorization relation across reductions.

theorem

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

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

13.2.1. Worked example: coefficient reduction🔗

The block below reduces the coefficients of 100 - 3x + 50x². Modulo 7² = 49 the coefficients become 2, 46, 1; modulo 5² = 25 they become 0, 22, 0, and the trailing zero is trimmed by normalization.

open Hex Hex.DensePoly Hex.QuadraticLiftResult

namespace HexHenselChapterReduce

private def f : ZPoly := ofCoeffs #[100, -3, 50]

-- 100 ≡ 2, -3 ≡ 46, 50 ≡ 1  (mod 7² = 49)
private def a : ZPoly := ZPoly.reduceModPow f 7 2
#guard a.toArray.toList = [2, 46, 1]

-- 100 ≡ 0, -3 ≡ 22, 50 ≡ 0  (mod 5² = 25)
private def b : ZPoly := reduceModSquare f 5
#guard b.toArray.toList = [0, 22]

end HexHenselChapterReduce