HL0005

hensel_canonical_lift_digit_decompose

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

Alpha v34 checked-use · first admitted v27 · 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.

The derivative-nonzero criterion supplies no inverse or power witness: both are constructed. Roots may be arbitrary natural representatives of signed integer polynomials. Singular-root classification and p-adic completion are separate milestones.

Exact theorem in conservative defined notation

∀ m. ∀ p. ∀ a. ∀ z. ¬m = 0 → Lt(a,m) → Lt(z,p · m) → ModEq(m,z,a) → ∃ x. Lt(x,p) ∧ z = a + m · x

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

Definition DAG

Lt(a,b) · 5ModEq(m,a,b) · 1

Actual proof prerequisites

division_remainder_exists · checked external prerequisitecanonical_remainder_from_mod · checked external prerequisitele_or_lt · checked external prerequisitelt_not_le · checked external prerequisitele_trans · checked external prerequisitemul_le_mul_left · checked external prerequisitele_add_right · checked external prerequisitemul_comm · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order statement 
forall m p a z. ~(m = 0) -> (exists hpl_gap_bound. hpl_gap_bound + S (a) = (m)) -> (exists hpl_gap_bound. hpl_gap_bound + S (z) = (p * m)) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. z + m * hgcrt_mod_left_hpl_mod = a + m * hgcrt_mod_right_hpl_mod) -> exists t. ((exists hpl_gap_bound. hpl_gap_bound + S (t) = (p)) /\ z = a + m * t)

Complete tactic proof in conservative notation

All 60 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

60 script commands · 19 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–8

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

  1. L1
    intro m
  2. L2
    intro p
  3. L3
    intro a
  4. L4
    intro z
  5. L5
    intro hm
  6. L6
    intro ha
  7. L7
    intro hz
  8. L8
    intro hmod
02Establish hdivL9–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder exists.

  1. L9
    have hdiv : ∃ q. ∃ r. z = m · q + r ∧ Lt(r,m)Definitions: Lt(r,m)Original native command in the exact edition
  2. L10
    specialize division_remainder_exists m
  3. L11
    specialize division_remainder_exists z
  4. L12
    apply division_remainder_exists
  5. L13
    exact hm
03Separate the logical casesL14–16

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

  1. L14
    cases hdiv
  2. L15
    cases hdiv_witness
  3. L16
    cases hdiv_witness_witness
04Establish hrL17–26

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

  1. L17
    have hr : x1 = a
  2. L18
    specialize canonical_remainder_from_mod m
  3. L19
    specialize canonical_remainder_from_mod z
  4. L20
    specialize canonical_remainder_from_mod x
  5. L21
    specialize canonical_remainder_from_mod x1
  6. L22
    specialize canonical_remainder_from_mod a
  7. L23
    apply canonical_remainder_from_mod
  8. L24
    exact hdiv_witness_witness_left
  9. L25
    exact hdiv_witness_witness_right
  10. L26
    exact ha
05Use earlier factsL27–27

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

  1. L27
    exact hmod
06Establish hboundL28–30

Establish this local claim before using it. It is not an additional assumption.

  1. L28
    have hbound : Lt(x,p)Definitions: Lt(x,p)Original native command in the exact edition
  2. L29
    specialize le_or_lt p
  3. L30
    specialize le_or_lt x
07Separate the logical casesL31–32

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

  1. L31
    cases le_or_lt
  2. L32
    exfalso
08Use earlier factsL33–36

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

  1. L33
    specialize lt_not_le z
  2. L34
    specialize lt_not_le (p * m)
  3. L35
    apply lt_not_le
  4. L36
    exact hz
09Establish hprodL37–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L37
    have hprod : p * m = m * p
  2. L38
    apply mul_comm
  3. L39
    rewrite hprod
  4. L40
    specialize le_trans (m * p)
  5. L41
    specialize le_trans (m * x)
  6. L42
    specialize le_trans z
  7. L43
    apply le_trans
  8. L44
    specialize mul_le_mul_left p
  9. L45
    specialize mul_le_mul_left x
  10. L46
    specialize mul_le_mul_left m
10Use earlier factsL47–48

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

  1. L47
    apply mul_le_mul_left
  2. L48
    exact le_or_lt_left
11Calculate and transport equalitiesL49–49

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L49
    rewrite hdiv_witness_witness_left
12Use earlier factsL50–53

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

  1. L50
    specialize le_add_right (m * x)
  2. L51
    specialize le_add_right x1
  3. L52
    apply le_add_right
  4. L53
    exact le_or_lt_right
13Construct an explicit witnessL54–54

Supply the displayed value, then prove that it has the required property.

  1. L54
    exists x
14Separate the logical casesL55–55

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

  1. L55
    split
15Use earlier factsL56–56

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

  1. L56
    exact hbound
16Calculate and transport equalitiesL57–57

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L57
    trans m * x + x1
17Use earlier factsL58–58

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

  1. L58
    exact hdiv_witness_witness_left
18Calculate and transport equalitiesL59–59

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L59
    rewrite hr
19Use earlier factsL60–60

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

  1. L60
    apply add_comm

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro m
  2. 0002intro p
  3. 0003intro a
  4. 0004intro z
  5. 0005intro hm
  6. 0006intro ha
  7. 0007intro hz
  8. 0008intro hmod
  9. 0009have hdiv : ∃ q. ∃ r. z = m · q + r ∧ Lt(r,m)
  10. 0010specialize division_remainder_exists m
  11. 0011specialize division_remainder_exists z
  12. 0012apply division_remainder_exists
  13. 0013exact hm
  14. 0014cases hdiv
  15. 0015cases hdiv_witness
  16. 0016cases hdiv_witness_witness
  17. 0017have hr : x1 = a
  18. 0018specialize canonical_remainder_from_mod m
  19. 0019specialize canonical_remainder_from_mod z
  20. 0020specialize canonical_remainder_from_mod x
  21. 0021specialize canonical_remainder_from_mod x1
  22. 0022specialize canonical_remainder_from_mod a
  23. 0023apply canonical_remainder_from_mod
  24. 0024exact hdiv_witness_witness_left
  25. 0025exact hdiv_witness_witness_right
  26. 0026exact ha
  27. 0027exact hmod
  28. 0028have hbound : Lt(x,p)
  29. 0029specialize le_or_lt p
  30. 0030specialize le_or_lt x
  31. 0031cases le_or_lt
  32. 0032exfalso
  33. 0033specialize lt_not_le z
  34. 0034specialize lt_not_le (p * m)
  35. 0035apply lt_not_le
  36. 0036exact hz
  37. 0037have hprod : p * m = m * p
  38. 0038apply mul_comm
  39. 0039rewrite hprod
  40. 0040specialize le_trans (m * p)
  41. 0041specialize le_trans (m * x)
  42. 0042specialize le_trans z
  43. 0043apply le_trans
  44. 0044specialize mul_le_mul_left p
  45. 0045specialize mul_le_mul_left x
  46. 0046specialize mul_le_mul_left m
  47. 0047apply mul_le_mul_left
  48. 0048exact le_or_lt_left
  49. 0049rewrite hdiv_witness_witness_left
  50. 0050specialize le_add_right (m * x)
  51. 0051specialize le_add_right x1
  52. 0052apply le_add_right
  53. 0053exact le_or_lt_right
  54. 0054exists x
  55. 0055split
  56. 0056exact hbound
  57. 0057trans m * x + x1
  58. 0058exact hdiv_witness_witness_left
  59. 0059rewrite hr
  60. 0060apply add_comm