Exact quadratic Taylor witness · bounded inverse correction · G095 partial · Constructive arithmetic

Constructive Taylor remainders and one-step Hensel lifting

f(a)=m·q ∧ gcd(f′(a),p)=1 ⇒ ∃t<p. p·m ∣ f(a+m·t)

Nineteen independently checked constructive theorems prove exact witnessed quadratic Taylor remainders for arbitrary beta-coded polynomials, unique bounded modular correction digits and a genuine one-step simple-root divisibility lift.

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 867 native tactic lines and 69 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem TH0013 and follow only the lemmas and conservative definitions supporting beta_horner_hensel_lift_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G095 milestone → theorem and definition dependencies.
Major independently established statements: TH0004 beta_horner_eval_mod_congruence · TH0005 beta_horner_derivative_mod_congruence · TH0008 beta_horner_taylor_remainder_exists · TH000B hensel_correction_exists_unique · TH000C horner_derivative_coprime_bounded_inverse · TH000D beta_horner_taylor_square_congruence · TH0012 beta_horner_hensel_lift_divisibility · TH0013 beta_horner_hensel_lift_exists.
Independently verified Alpha v34 checked-use theorem family: 19 dependency-curried kernel-checked theorem bodies · 69 proof prerequisites · 16 linked definitions · 18 definition-dependency arrows · 867 exact tactic lines · first admitted v25 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 302 bundle nodes; SHA-256 d4532076049be869e4e397d0fcee81b668bd3fd5c7d9173028bb1bdb80b9793a.
Exact mathematical boundary: Historical partial components only: this chapter proves exact natural polynomial Taylor remainders, bounded corrections, and one-step divisibility lifts. G095 is now closed in the separate Alpha-v27 hensel-lifting branch for integer polynomials, unrestricted input roots, unique canonical representatives, and every positive prime power.

Separate complete second-wave branches: Full G095 proof · Alpha v27.