13.1. Introduction🔗

HexHensel does executable Hensel lifting. Hensel lifting turns a factorization known only modulo a prime p into a factorization modulo a prime power p^k: given f ≡ g · h (mod p) together with a Bezout certificate s · g + t · h ≡ 1 (mod p), it refines g and h step by step until they multiply to f modulo p^k. The precision k is chosen large enough (via a Mignotte bound) that the lifted factors coincide with the true integer factors. This connects the prime-field factorization in HexPolyFp to the integer factorization pipelines built on top of it.

The library connects integer polynomials (HexPolyZ, Hex.ZPoly) with prime-field polynomials (HexPolyFp, Hex.FpPoly p). It provides coefficientwise reduction modulo powers of p, the linear and quadratic single-step corrections, the iterative Hex.ZPoly.henselLift wrapper, and the ordered multifactor lift API the factorization pipeline consumes. It is Mathlib-free and depends only on HexPolyFp and HexPolyZ. See Cross-references.