8.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; the forward theorems linearHenselStep_g and linearHenselStep_h provide simplifying equations for them.

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

Guarded selection: the word-sized step when its guard holds, else the bignum step.