Integer polynomials · unrestricted roots · every prime power · Constructive arithmetic

Full constructive simple-root Hensel lifting

f(a)≡0 (mod p) ∧ f′(a)≢0 (mod p) ⇒ ∀k>0. ∃!r<pᵏ. r≡a (mod p) ∧ f(r)≡0 (mod pᵏ)

Evaluate actual signed polynomials, derive the derivative inverse from nonvanishing modulo the prime, and construct the unique canonical lift at every positive prime-power precision.

Open the definition-aware map Read the final theorem See campaign milestone G095

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 2692 native tactic lines and 197 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem HL0028 and follow only the lemmas and conservative definitions supporting integer_polynomial_prime_simple_root_lifts_all_positive_powers.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G095 milestone → theorem and definition dependencies.
Major independently established statements: HL0023 integer_polynomial_prime_power_hensel_lift_exists_unique · HL0024 integer_polynomial_prime_power_hensel_iterated_exists_unique · HL0028 integer_polynomial_prime_simple_root_lifts_all_positive_powers.
Independently verified Alpha v34 checked-use theorem family: 40 dependency-curried kernel-checked theorem bodies · 197 proof prerequisites · 25 linked definitions · 38 definition-dependency arrows · 2692 exact tactic lines · first admitted v27 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 1224 bundle nodes; SHA-256 c4711433c92b67d2ebeb30131669c60563c70e0464dafa851d417fb88fb21a6d.
Exact mathematical boundary: The derivative-nonzero criterion supplies no inverse or power witness: both are constructed. Roots may be arbitrary natural representatives of signed integer polynomials. Singular-root classification and p-adic completion are separate milestones.