13.3. Single-step corrections🔗

Hensel lifting comes in two flavours that differ in how fast the precision grows. The linear step refines the modulus by one prime power per step (p^k → p^(k+1)); the quadratic step doubles it (m → m^2), reaching precision p^k in O(log k) steps rather than O(k), at the cost of also lifting the Bezout witnesses each step.

The linear step returns the corrected pair of factors.

structure

Hex.LinearLiftResult : Type
Hex.LinearLiftResult : Type

Result of one linear Hensel lift step, packaging the lifted first factor g and the lifted complementary factor h. Callers can pattern-match on the two projections directly, or rewrite via the unfolding simp lemmas linearHenselStep_g / linearHenselStep_h.

Constructor

Hex.LinearLiftResult.mk

Fields

g : Hex.ZPoly

The lifted first factor.

h : Hex.ZPoly

The lifted complementary factor.

def

Hex.ZPoly.linearHenselStep (p k : ℕ) [Hex.ZMod64.Bounds p]
  (f g h : Hex.ZPoly) (s t : Hex.FpPoly p) : Hex.LinearLiftResult
Hex.ZPoly.linearHenselStep (p k : ℕ)
  [Hex.ZMod64.Bounds p]
  (f g h : Hex.ZPoly)
  (s t : Hex.FpPoly p) :
  Hex.LinearLiftResult

One linear Hensel correction step from modulus p^k to p^(k+1).

The quadratic step doubles the modulus and so must carry the Bezout witnesses forward alongside the factors. Its result bundles all four.

Hex.QuadraticLiftResult packages the updated leading factor g (monic), the complementary factor h, and the updated Bezout witnesses s and t satisfying s · g + t · h ≡ 1 (mod m²).

def

Hex.ZPoly.quadraticHenselStep (m : ℕ) (f g h s t : Hex.ZPoly) :
  Hex.QuadraticLiftResult
Hex.ZPoly.quadraticHenselStep (m : ℕ)
  (f g h s t : Hex.ZPoly) :
  Hex.QuadraticLiftResult

One quadratic Hensel correction step from modulus m to modulus m^2.

Inputs: the target polynomial f, the current monic factor g, the complementary factor h, and the Bezout witnesses s, t for the current factorisation. Preconditions consumed by the spec theorems below are g monic, g * h ≡ f (mod m), and s * g + t * h ≡ 1 (mod m); the returned QuadraticLiftResult then satisfies the same conjuncts modulo m^2.