Constructive Taylor remainders and one-step Hensel lifting — Exact Proof Explorer

The predecessor of every positive modulus gives a witnessed subtraction-free negative residue.

One genuine Horner value transition preserves balanced congruence at congruent evaluation points.

One coupled formal-derivative Horner transition preserves balanced value and derivative congruence.

Every arbitrary beta-coded natural polynomial preserves balanced congruence between evaluation points.

Every beta-coded natural polynomial and its exact formal derivative simultaneously preserve balanced congruence.

Two adjacent natural summands can be swapped inside a right-associated finite sum.

The successor Horner transition has an exact subtraction-free quadratic Taylor remainder.

Every beta-coded natural polynomial has an exact witnessed quadratic Taylor remainder at every natural shift.

Every coprime derivative at a nonzero modulus has an actual strictly bounded subtraction-free root correction.

At every nonzero modulus a coprime derivative has at most one strictly bounded root-correction digit.

Every coprime formal derivative at a nonzero modulus has exactly one canonical bounded correction digit.

An actual evaluated coprime formal derivative has a strictly bounded constructive modular inverse.

Every polynomial value at a shifted natural point is congruent to its exact first-order Taylor linearization modulo the square shift.

Every coefficient list, natural evaluation point, and natural shift has actual polynomial, derivative, shifted-value, and quadratic-remainder witnesses.

Every verified bounded Hensel correction supplies an actual natural divisibility witness for its annihilated linear residual.

A root-correction divisibility witness makes the complete first-order lifted value a multiple of the next modulus.

Whenever the old modulus contains its lifting factor, every squared modulus shift is divisible by the next modulus.

A real bounded simple-root correction lifts an arbitrary beta-coded polynomial root from m to p*m whenever p divides m.

Every genuinely evaluated coprime simple root modulo a p-divisible modulus has an actual bounded correction and an actual polynomial root modulo the next modulus.