TH000A

hensel_correction_unique

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 expanded first-order arithmetic 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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 48 exact native proof lines.

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

Proof neighborhood

Direct dependencies

mod_eq_symm Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized mod_eq_add_cancel_left Alpha theorem; checked-use authorized mod_eq_cancel_coprime Stable theorem; checked-use authorized mod_eq_bounded_unique Stable theorem; checked-use authorized

Direct dependents

TH000B hensel_correction_exists_unique

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact 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

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