TH000A

hensel_correction_unique

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

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable

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.

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. Full G095 proof · Alpha v27

Exact theorem in conservative defined notation

∀ d. ∀ p. ∀ q. ∀ t. ∀ u. ¬p = 0 → Coprime(d,p) → HenselCorrection(d,p,q,t) → HenselCorrection(d,p,q,u) → t = u

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

HenselCorrection(d,p,q,t) · 2Coprime(a,b) · 1

Actual proof prerequisites

mod_eq_symm · checked external prerequisitemod_eq_trans · checked external prerequisitemod_eq_add_cancel_left · checked external prerequisitemod_eq_cancel_coprime · checked external prerequisitemod_eq_bounded_unique · checked external prerequisite
Original expanded first-order statement 
forall d p q t u. ~(p = 0) -> (forall hmi_divisor_pth_correction. (exists hmi_left_factor_pth_correction. d = hmi_divisor_pth_correction * hmi_left_factor_pth_correction) -> (exists hmi_right_factor_pth_correction. p = hmi_divisor_pth_correction * hmi_right_factor_pth_correction) -> hmi_divisor_pth_correction = 1) -> (((exists ff_lt_pth_correction_t_bound. ff_lt_pth_correction_t_bound + S t = p) /\ (exists hgcrt_mod_left_pth_correction_t_annihilation hgcrt_mod_right_pth_correction_t_annihilation. (q + d * t) + p * hgcrt_mod_left_pth_correction_t_annihilation = 0 + p * hgcrt_mod_right_pth_correction_t_annihilation))) -> (((exists ff_lt_pth_correction_u_bound. ff_lt_pth_correction_u_bound + S u = p) /\ (exists hgcrt_mod_left_pth_correction_u_annihilation hgcrt_mod_right_pth_correction_u_annihilation. (q + d * u) + p * hgcrt_mod_left_pth_correction_u_annihilation = 0 + p * hgcrt_mod_right_pth_correction_u_annihilation))) -> t = u

Complete unchanged native tactic proof

All 48 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

48 script commands · 7 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–9

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro d
  2. L2
    intro p
  3. L3
    intro q
  4. L4
    intro t
  5. L5
    intro u
  6. L6
    intro hp
  7. L7
    intro hcop
  8. L8
    intro ht
  9. L9
    intro hu
02Separate the logical casesL10–11

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L10
    cases ht
  2. L11
    cases hu
03Establish hreverseL12–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L12
    have hreverse : exists hgcrt_mod_left_pth_correction_reverse hgcrt_mod_right_pth_correction_reverse. 0 + p * hgcrt_mod_left_pth_correction_reverse = (q + d * u) + p * hgcrt_mod_right_pth_correction_reverse
  2. L13
    specialize mod_eq_symm p
  3. L14
    specialize mod_eq_symm (q + d * u)
  4. L15
    specialize mod_eq_symm 0
  5. L16
    apply mod_eq_symm
  6. L17
    exact hu_right
04Establish hbothL18–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L18
    have hboth : exists hgcrt_mod_left_pth_correction_both hgcrt_mod_right_pth_correction_both. (q + d * t) + p * hgcrt_mod_left_pth_correction_both = (q + d * u) + p * hgcrt_mod_right_pth_correction_both
  2. L19
    specialize mod_eq_trans p
  3. L20
    specialize mod_eq_trans (q + d * t)
  4. L21
    specialize mod_eq_trans 0
  5. L22
    specialize mod_eq_trans (q + d * u)
  6. L23
    apply mod_eq_trans
  7. L24
    exact ht_right
  8. L25
    exact hreverse
05Establish hscaledL26–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq add cancel left.

  1. L26
    have hscaled : exists hgcrt_mod_left_pth_correction_scaled hgcrt_mod_right_pth_correction_scaled. (d * t) + p * hgcrt_mod_left_pth_correction_scaled = (d * u) + p * hgcrt_mod_right_pth_correction_scaled
  2. L27
    specialize mod_eq_add_cancel_left p
  3. L28
    specialize mod_eq_add_cancel_left q
  4. L29
    specialize mod_eq_add_cancel_left (d * t)
  5. L30
    specialize mod_eq_add_cancel_left (d * u)
  6. L31
    apply mod_eq_add_cancel_left
  7. L32
    exact hboth
06Establish hdigitsL33–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq cancel coprime.

  1. L33
    have hdigits : exists hgcrt_mod_left_pth_correction_digits hgcrt_mod_right_pth_correction_digits. t + p * hgcrt_mod_left_pth_correction_digits = u + p * hgcrt_mod_right_pth_correction_digits
  2. L34
    specialize mod_eq_cancel_coprime p
  3. L35
    specialize mod_eq_cancel_coprime d
  4. L36
    specialize mod_eq_cancel_coprime t
  5. L37
    specialize mod_eq_cancel_coprime u
  6. L38
    apply mod_eq_cancel_coprime
  7. L39
    exact hp
  8. L40
    exact hcop
  9. L41
    exact hscaled
  10. L42
    specialize mod_eq_bounded_unique p
07Use earlier factsL43–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L43
    specialize mod_eq_bounded_unique t
  2. L44
    specialize mod_eq_bounded_unique u
  3. L45
    apply mod_eq_bounded_unique
  4. L46
    exact ht_left
  5. L47
    exact hu_left
  6. L48
    exact hdigits

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro d
  2. 0002intro p
  3. 0003intro q
  4. 0004intro t
  5. 0005intro u
  6. 0006intro hp
  7. 0007intro hcop
  8. 0008intro ht
  9. 0009intro hu
  10. 0010cases ht
  11. 0011cases hu
  12. 0012have hreverse : exists hgcrt_mod_left_pth_correction_reverse hgcrt_mod_right_pth_correction_reverse. 0 + p * hgcrt_mod_left_pth_correction_reverse = (q + d * u) + p * hgcrt_mod_right_pth_correction_reverse
  13. 0013specialize mod_eq_symm p
  14. 0014specialize mod_eq_symm (q + d * u)
  15. 0015specialize mod_eq_symm 0
  16. 0016apply mod_eq_symm
  17. 0017exact hu_right
  18. 0018have hboth : exists hgcrt_mod_left_pth_correction_both hgcrt_mod_right_pth_correction_both. (q + d * t) + p * hgcrt_mod_left_pth_correction_both = (q + d * u) + p * hgcrt_mod_right_pth_correction_both
  19. 0019specialize mod_eq_trans p
  20. 0020specialize mod_eq_trans (q + d * t)
  21. 0021specialize mod_eq_trans 0
  22. 0022specialize mod_eq_trans (q + d * u)
  23. 0023apply mod_eq_trans
  24. 0024exact ht_right
  25. 0025exact hreverse
  26. 0026have hscaled : exists hgcrt_mod_left_pth_correction_scaled hgcrt_mod_right_pth_correction_scaled. (d * t) + p * hgcrt_mod_left_pth_correction_scaled = (d * u) + p * hgcrt_mod_right_pth_correction_scaled
  27. 0027specialize mod_eq_add_cancel_left p
  28. 0028specialize mod_eq_add_cancel_left q
  29. 0029specialize mod_eq_add_cancel_left (d * t)
  30. 0030specialize mod_eq_add_cancel_left (d * u)
  31. 0031apply mod_eq_add_cancel_left
  32. 0032exact hboth
  33. 0033have hdigits : exists hgcrt_mod_left_pth_correction_digits hgcrt_mod_right_pth_correction_digits. t + p * hgcrt_mod_left_pth_correction_digits = u + p * hgcrt_mod_right_pth_correction_digits
  34. 0034specialize mod_eq_cancel_coprime p
  35. 0035specialize mod_eq_cancel_coprime d
  36. 0036specialize mod_eq_cancel_coprime t
  37. 0037specialize mod_eq_cancel_coprime u
  38. 0038apply mod_eq_cancel_coprime
  39. 0039exact hp
  40. 0040exact hcop
  41. 0041exact hscaled
  42. 0042specialize mod_eq_bounded_unique p
  43. 0043specialize mod_eq_bounded_unique t
  44. 0044specialize mod_eq_bounded_unique u
  45. 0045apply mod_eq_bounded_unique
  46. 0046exact ht_left
  47. 0047exact hu_left
  48. 0048exact hdigits