Registry · Theorem III.T11 tau-effective formalized

III.T11 — 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.

Book III Part 3 Ch. 16

Dependency Graph

Depends on (1)

III.T10

Depended on by (2)

III.D21 III.R09

Lean Formalization

Module: TauLib.BookIII.Spectral.HenselLifting

Symbol: hensel_lift