Constructive Hensel Lifting

Given a root mod p, lift to root mod p^n by modular Newton iteration. No signed arithmetic: correction via modular complement. Lifting is unique (p-adic contraction). Fully constructive proof.

Constructive Hensel Lifting

Summary

Given a root mod p, lift to root mod p^n by modular Newton iteration. No signed arithmetic: correction via modular complement. Lifting is unique (p-adic contraction). Fully constructive proof.

Statement

%
\label{thm:constructive-hensel}
Let $p$ be a prime, $f \in (\Z / p^{n+1} \Z)[x]$
a polynomial with residue coefficients,
and $a_n \in \Z / p^n \Z$ a root of~$f$
modulo~$p^n$ such that $f'(a_n)$ is a unit
modulo~$p$.
Then there exists a unique $a_{n+1} \in \Z / p^{n+1} \Z$
satisfying:
\begin{enumerate}
    \item[\textup{(i)}]
          $a_{n+1} \equiv a_n \pmod{p^n}$
          \textup{(compatibility)},
    \item[\textup{(ii)}]
          $f(a_{n+1}) \equiv 0 \pmod{p^{n+1}}$
          \textup{(root condition)},
    \item[\textup{(iii)}]
          $a_{n+1}$ is given by
          \eqref{eq:ch16-lifted-root}
          using only addition, multiplication,
          and the modular complement $p - q_n$
          \textup{(no signed arithmetic)}.
\end{enumerate}
Moreover, $f'(a_{n+1})$ is again a unit modulo~$p$,
so the lifting can be iterated indefinitely.

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 44
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part03/ch16-hensel-lifting-and-local-fields.tex lines 157-183

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Spectral.HenselLifting
• Name: hensel_lift

Dependencies

• Canonical: III.T10

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.