Full constructive simple-root Hensel lifting — Exact Proof Explorer

A known zero-congruent summand can be cancelled without subtraction.

A derivative remains coprime to a nonzero modulus after any genuine congruence transport.

Every unrestricted natural input has a constructed canonical residue at every nonzero modulus.

A bounded old representative and bounded correction digit give the exact next-modulus bound.

Every canonical next-modulus element in an old residue class has an actual bounded correction digit.

The lifted first-order Taylor term factors exactly by the old modulus.

Every genuine next-modulus root with a bounded digit necessarily satisfies the derivative correction equation.

A canonical old simple root has exactly one bounded next-modulus lift among all roots in its old residue class.

An unrestricted natural input can be normalized without losing its exact polynomial root or simple derivative.

Every unrestricted natural-polynomial simple root has a unique canonical lift, with no supplied correction or representative bound.

An actual polynomial root transports to every congruent natural point.

A witnessed root modulo a multiple is also a root modulo the old divisor.

Every lifted root in a simple residue class has an actual evaluated derivative that remains coprime to the base.

At iteration zero every unrestricted root has exactly one representative in its own canonical residue interval.

Every actual positive power of a nonzero base supplies both nonzeroness and an explicit base factor.

A positive prime-power-level simple root at an unrestricted input has a unique canonical lift and an actual next-power witness; the theorem even permits every nonzero base.

Every genuine canonical lift preserves simplicity, with an actual new polynomial/derivative trace rather than a supplied derivative oracle.

HA induction constructs unique canonical simple-root lifts through every finite number of prime-power steps, including iteration zero, and proves uniqueness among all roots in the original residue class.

From every positive initial prime-power exponent, arbitrary finite further lifting constructs the actual higher power and its unique canonical root while preserving the entire initial residue class.

Every pair of finite integer-coefficient component codes admits an actual natural positive+weight*negative coefficient code.

Both the Horner value and derivative transitions preserve an exact weighted coefficient combination.

For every finite coefficient list, the actual recoded polynomial and its actual formal derivative are the exact weighted combinations of their signed components.

The natural recoding and its negative component balance to the positive component plus a full modulus multiple.

Natural recoding preserves every signed residue modulo every divisor of the selected final modulus.

The recoded natural value is zero modulo an old or new modulus exactly when the original signed value is zero there.

An actual inverse of the integer derivative proves the recoded natural derivative coprime to the lifting base.

At every natural point the recoded natural root condition is equivalent to the original integer-polynomial root condition, not merely implied by it.

Every actual signed-polynomial root has actual positive/negative value and formal-derivative traces consistent with its witnessed root equation.

The same bounded inverse transports an integer derivative through congruent positive and negative components.

Every canonical integer-polynomial lift retains an actual invertible formal derivative, with explicit coupled traces for both signed components.

Every arbitrary integer-coefficient simple root has unique canonical lifts through any finite number of prime-power steps; both existence and all-root uniqueness transport from an actually constructed natural polynomial.

An unrestricted root of any finite integer-coefficient polynomial has exactly one canonical next-modulus lift whenever its actual integer derivative is a unit.

Full integer-coefficient simple-root Hensel lifting constructs the actual next power and its unique bounded root, with no bound on the original input and no supplied correction.

Full integer-coefficient Hensel iteration constructs the actual arbitrary higher power and the unique canonical root in the entire original prime-power residue class.

G095: every integer-polynomial simple root at any natural representative modulo a positive prime power has one and only one canonical lift modulo the next actual power.

For arbitrary finite j, an integer-polynomial simple root modulo p^k has a unique canonical lift modulo the actually constructed p^(k+j), retaining its full original residue class.

A derivative nonzero modulo a genuine prime yields a bounded signed inverse through the actual natural blend dp+(p-1)*dn, with coprimality and both residue transports proved explicitly.

The ordinary signed nonzero-mod-prime derivative condition constructs the full bounded derivative-unit witness; neither an inverse nor a natural blend is supplied.

A genuine integer-polynomial root with derivative merely nonzero modulo the prime satisfies the unchanged unit-based simple-root interface, using the same actual Horner value and derivative witnesses.

Exact full G095: a root modulo a prime with signed derivative nonzero modulo that prime has a uniquely determined bounded lift in its residue class at every positive precision; the actual power, inverse and lift are all constructed rather than supplied.