HL0007

hensel_lift_correction_of_root

Every genuine next-modulus root with a bounded digit necessarily satisfies the derivative correction equation.

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

∀ b. ∀ c. ∀ a. ∀ l. ∀ n. ∀ d. ∀ m. ∀ p. ∀ s. ∀ q. ∀ t. ∀ y. ¬m = 0 → HornerDerivative(b,c,a,l,n,d) → Horner(b,c,a + m · t,l,y) → m = p · s → n = m · q → Lt(t,p) → ModEq(p · m,y,0) → Lt(t,p) ∧ ModEq(p,q + d · t,0)

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

Definition DAG

Horner(b,c,x,ell,z) · 1HornerDerivative(b,c,t,l,n,z) · 1Lt(a,b) · 2Dvd(d,n) · 1ModEq(m,a,b) · 4

Actual proof prerequisites

beta_horner_taylor_remainder_exists · checked external prerequisitehensel_square_shift_multiple · checked external prerequisitemultiple_mul_right · checked external prerequisitemultiple_implies_balanced_zero_congruence · checked external prerequisitehensel_mod_add_zero_cancelhensel_lift_linear_identitymod_eq_unscale_nonzero · checked external prerequisitemul_comm · checked external prerequisite
Original expanded first-order statement 
forall b c a l n d m p s q t y. ~(m = 0) -> (exists ff_u_hd_hpl_pair ff_v_hd_hpl_pair ff_d_hd_hpl_pair ff_e_hd_hpl_pair. ((((((exists fs_h_ph_hd_hpl_pair_body_value_start. fs_h_ph_hd_hpl_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_start. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_start * S ((S (0)) * ff_v_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_terminal. fs_h_ph_hd_hpl_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_terminal. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_terminal * S ((S (l)) * ff_v_hd_hpl_pair) + (n))) /\ forall ff_i_ph_hd_hpl_pair_body_value_steps. (exists ph_bound_hd_hpl_pair_body_value_steps. ph_bound_hd_hpl_pair_body_value_steps + S ff_i_ph_hd_hpl_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_value_steps ff_previous_ph_hd_hpl_pair_body_value_steps ff_current_ph_hd_hpl_pair_body_value_steps. ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_coefficient. fs_h_ph_hd_hpl_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_coefficient. b = fs_q_ph_hd_hpl_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_before. fs_h_ph_hd_hpl_pair_body_value_steps_before + S (ff_previous_ph_hd_hpl_pair_body_value_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_before. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_value_steps_after. fs_h_ph_hd_hpl_pair_body_value_steps_after + S (ff_current_ph_hd_hpl_pair_body_value_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_value_steps_after. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_value_steps)) * ff_v_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_value_steps))) /\ ff_current_ph_hd_hpl_pair_body_value_steps = ff_previous_ph_hd_hpl_pair_body_value_steps * a + ff_coefficient_ph_hd_hpl_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_hpl_pair_body_derivative_start. fs_h_ph_hd_hpl_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_start. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_start * S ((S (0)) * ff_e_hd_hpl_pair) + (0))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_terminal. fs_h_ph_hd_hpl_pair_body_derivative_terminal + S (d) = S ((S (l)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_terminal. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_hpl_pair) + (d))) /\ forall ff_i_ph_hd_hpl_pair_body_derivative_steps. (exists ph_bound_hd_hpl_pair_body_derivative_steps. ph_bound_hd_hpl_pair_body_derivative_steps + S ff_i_ph_hd_hpl_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_hpl_pair_body_derivative_steps ff_previous_ph_hd_hpl_pair_body_derivative_steps ff_current_ph_hd_hpl_pair_body_derivative_steps. ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient. fs_h_ph_hd_hpl_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient. ff_u_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_v_hd_hpl_pair) + (ff_coefficient_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_before. fs_h_ph_hd_hpl_pair_body_derivative_steps_before + S (ff_previous_ph_hd_hpl_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_before. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_previous_ph_hd_hpl_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_hpl_pair_body_derivative_steps_after. fs_h_ph_hd_hpl_pair_body_derivative_steps_after + S (ff_current_ph_hd_hpl_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair)) /\ exists fs_q_ph_hd_hpl_pair_body_derivative_steps_after. ff_d_hd_hpl_pair = fs_q_ph_hd_hpl_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_hpl_pair_body_derivative_steps)) * ff_e_hd_hpl_pair) + (ff_current_ph_hd_hpl_pair_body_derivative_steps))) /\ ff_current_ph_hd_hpl_pair_body_derivative_steps = ff_previous_ph_hd_hpl_pair_body_derivative_steps * a + ff_coefficient_ph_hd_hpl_pair_body_derivative_steps)))))))) -> (exists ff_u_ph_hpl_eval ff_v_ph_hpl_eval. ((((exists fs_h_ph_hpl_eval_body_start. fs_h_ph_hpl_eval_body_start + S (0) = S ((S (0)) * ff_v_ph_hpl_eval)) /\ exists fs_q_ph_hpl_eval_body_start. ff_u_ph_hpl_eval = fs_q_ph_hpl_eval_body_start * S ((S (0)) * ff_v_ph_hpl_eval) + (0))) /\ ((((exists fs_h_ph_hpl_eval_body_terminal. fs_h_ph_hpl_eval_body_terminal + S (y) = S ((S (l)) * ff_v_ph_hpl_eval)) /\ exists fs_q_ph_hpl_eval_body_terminal. ff_u_ph_hpl_eval = fs_q_ph_hpl_eval_body_terminal * S ((S (l)) * ff_v_ph_hpl_eval) + (y))) /\ forall ff_i_ph_hpl_eval_body_steps. (exists ph_bound_hpl_eval_body_steps. ph_bound_hpl_eval_body_steps + S ff_i_ph_hpl_eval_body_steps = l) -> exists ff_coefficient_ph_hpl_eval_body_steps ff_previous_ph_hpl_eval_body_steps ff_current_ph_hpl_eval_body_steps. ((((exists fs_h_ph_hpl_eval_body_steps_coefficient. fs_h_ph_hpl_eval_body_steps_coefficient + S (ff_coefficient_ph_hpl_eval_body_steps) = S ((S (ff_i_ph_hpl_eval_body_steps)) * c)) /\ exists fs_q_ph_hpl_eval_body_steps_coefficient. b = fs_q_ph_hpl_eval_body_steps_coefficient * S ((S (ff_i_ph_hpl_eval_body_steps)) * c) + (ff_coefficient_ph_hpl_eval_body_steps))) /\ ((((exists fs_h_ph_hpl_eval_body_steps_before. fs_h_ph_hpl_eval_body_steps_before + S (ff_previous_ph_hpl_eval_body_steps) = S ((S (ff_i_ph_hpl_eval_body_steps)) * ff_v_ph_hpl_eval)) /\ exists fs_q_ph_hpl_eval_body_steps_before. ff_u_ph_hpl_eval = fs_q_ph_hpl_eval_body_steps_before * S ((S (ff_i_ph_hpl_eval_body_steps)) * ff_v_ph_hpl_eval) + (ff_previous_ph_hpl_eval_body_steps))) /\ ((((exists fs_h_ph_hpl_eval_body_steps_after. fs_h_ph_hpl_eval_body_steps_after + S (ff_current_ph_hpl_eval_body_steps) = S ((S (S ff_i_ph_hpl_eval_body_steps)) * ff_v_ph_hpl_eval)) /\ exists fs_q_ph_hpl_eval_body_steps_after. ff_u_ph_hpl_eval = fs_q_ph_hpl_eval_body_steps_after * S ((S (S ff_i_ph_hpl_eval_body_steps)) * ff_v_ph_hpl_eval) + (ff_current_ph_hpl_eval_body_steps))) /\ ff_current_ph_hpl_eval_body_steps = ff_previous_ph_hpl_eval_body_steps * (a + m * t) + ff_coefficient_ph_hpl_eval_body_steps)))))) -> m = p * s -> n = m * q -> (exists hpl_gap_bound. hpl_gap_bound + S (t) = (p)) -> (exists hgcrt_mod_left_hpl_mod hgcrt_mod_right_hpl_mod. y + (p * m) * hgcrt_mod_left_hpl_mod = 0 + (p * m) * hgcrt_mod_right_hpl_mod) -> (((exists ff_lt_pth_hpl_correction_bound. ff_lt_pth_hpl_correction_bound + S t = p) /\ (exists hgcrt_mod_left_pth_hpl_correction_annihilation hgcrt_mod_right_pth_hpl_correction_annihilation. (q + d * t) + p * hgcrt_mod_left_pth_hpl_correction_annihilation = 0 + p * hgcrt_mod_right_pth_hpl_correction_annihilation)))

Complete tactic proof in conservative notation

All 80 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

80 script commands · 13 reading checkpoints · 7 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.

Named ingredients (2)
hensel mod add zero cancelhensel lift linear identity
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro a
  4. L4
    intro l
  5. L5
    intro n
  6. L6
    intro d
  7. L7
    intro m
  8. L8
    intro p
  9. L9
    intro s
  10. L10
    intro q
02Fix variables and assumptionsL11–19

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

  1. L11
    intro t
  2. L12
    intro y
  3. L13
    intro hm
  4. L14
    intro hpair
  5. L15
    intro hvalue
  6. L16
    intro hfactor
  7. L17
    intro hn
  8. L18
    intro ht
  9. L19
    intro hroot
03Establish htaylorL20–29

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

  1. L20
    have htaylor : exists w. y = (n + (m * t) * d) + ((m * t) * (m * t)) * w
  2. L21
    specialize beta_horner_taylor_remainder_exists b
  3. L22
    specialize beta_horner_taylor_remainder_exists c
  4. L23
    specialize beta_horner_taylor_remainder_exists a
  5. L24
    specialize beta_horner_taylor_remainder_exists (m * t)
  6. L25
    specialize beta_horner_taylor_remainder_exists l
  7. L26
    specialize beta_horner_taylor_remainder_exists n
  8. L27
    specialize beta_horner_taylor_remainder_exists d
  9. L28
    specialize beta_horner_taylor_remainder_exists y
  10. L29
    apply beta_horner_taylor_remainder_exists
04Use earlier factsL30–31

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

  1. L30
    exact hpair
  2. L31
    exact hvalue
05Separate the logical casesL32–32

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

  1. L32
    cases htaylor
06Establish hsquareL33–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hensel square shift multiple.

  1. L33
    have hsquare : Dvd(p · m,m · t · (m · t))Definitions: Dvd(p · m,m · t · (m · t))Original native command in the exact edition
  2. L34
    specialize hensel_square_shift_multiple m
  3. L35
    specialize hensel_square_shift_multiple t
  4. L36
    specialize hensel_square_shift_multiple p
  5. L37
    specialize hensel_square_shift_multiple s
  6. L38
    apply hensel_square_shift_multiple
  7. L39
    exact hfactor
07Establish hquadL40–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple implies balanced zero congruence.

  1. L40
    have hquad : ModEq(p · m,m · t · (m · t) · x,0)Definitions: ModEq(p · m,m · t · (m · t) · x,0)Original native command in the exact edition
  2. L41
    specialize multiple_implies_balanced_zero_congruence (p * m)
  3. L42
    specialize multiple_implies_balanced_zero_congruence (((m * t) * (m * t)) * x)
  4. L43
    apply multiple_implies_balanced_zero_congruence
  5. L44
    specialize multiple_mul_right (p * m)
  6. L45
    specialize multiple_mul_right ((m * t) * (m * t))
  7. L46
    specialize multiple_mul_right x
  8. L47
    apply multiple_mul_right
  9. L48
    exact hsquare
08Establish hlinearL49–56

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

  1. L49
    have hlinear : ModEq(p · m,n + m · t · d,0)Definitions: ModEq(p · m,n + m · t · d,0)Original native command in the exact edition
  2. L50
    specialize hensel_mod_add_zero_cancel (p * m)
  3. L51
    specialize hensel_mod_add_zero_cancel (n + (m * t) * d)
  4. L52
    specialize hensel_mod_add_zero_cancel (((m * t) * (m * t)) * x)
  5. L53
    apply hensel_mod_add_zero_cancel
  6. L54
    rewrite <- htaylor_witness
  7. L55
    exact hroot
  8. L56
    exact hquad
09Separate the logical casesL57–57

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

  1. L57
    split
10Use earlier factsL58–64

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

  1. L58
    exact ht
  2. L59
    specialize mod_eq_unscale_nonzero m
  3. L60
    specialize mod_eq_unscale_nonzero p
  4. L61
    specialize mod_eq_unscale_nonzero (q + d * t)
  5. L62
    specialize mod_eq_unscale_nonzero 0
  6. L63
    apply mod_eq_unscale_nonzero
  7. L64
    exact hm
11Establish hproductL65–68

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

  1. L65
    have hproduct : m * p = p * m
  2. L66
    apply mul_comm
  3. L67
    rewrite hproduct
  4. L68
    rewrite hproduct
12Establish hzeroL69–71

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

  1. L69
    have hzero : m * 0 = 0
  2. L70
    simp
  3. L71
    rewrite hzero
13Establish hidentityL72–80

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hensel lift linear identity.

  1. L72
    have hidentity : m * (q + d * t) = n + (m * t) * d
  2. L73
    rewrite hn
  3. L74
    specialize hensel_lift_linear_identity m
  4. L75
    specialize hensel_lift_linear_identity d
  5. L76
    specialize hensel_lift_linear_identity q
  6. L77
    specialize hensel_lift_linear_identity t
  7. L78
    apply hensel_lift_linear_identity
  8. L79
    rewrite hidentity
  9. L80
    exact hlinear

Library-wide reading audit

Original defined command ledger · 80 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro l
  5. 0005intro n
  6. 0006intro d
  7. 0007intro m
  8. 0008intro p
  9. 0009intro s
  10. 0010intro q
  11. 0011intro t
  12. 0012intro y
  13. 0013intro hm
  14. 0014intro hpair
  15. 0015intro hvalue
  16. 0016intro hfactor
  17. 0017intro hn
  18. 0018intro ht
  19. 0019intro hroot
  20. 0020have htaylor : exists w. y = (n + (m * t) * d) + ((m * t) * (m * t)) * w
  21. 0021specialize beta_horner_taylor_remainder_exists b
  22. 0022specialize beta_horner_taylor_remainder_exists c
  23. 0023specialize beta_horner_taylor_remainder_exists a
  24. 0024specialize beta_horner_taylor_remainder_exists (m * t)
  25. 0025specialize beta_horner_taylor_remainder_exists l
  26. 0026specialize beta_horner_taylor_remainder_exists n
  27. 0027specialize beta_horner_taylor_remainder_exists d
  28. 0028specialize beta_horner_taylor_remainder_exists y
  29. 0029apply beta_horner_taylor_remainder_exists
  30. 0030exact hpair
  31. 0031exact hvalue
  32. 0032cases htaylor
  33. 0033have hsquare : Dvd(p · m,m · t · (m · t))
  34. 0034specialize hensel_square_shift_multiple m
  35. 0035specialize hensel_square_shift_multiple t
  36. 0036specialize hensel_square_shift_multiple p
  37. 0037specialize hensel_square_shift_multiple s
  38. 0038apply hensel_square_shift_multiple
  39. 0039exact hfactor
  40. 0040have hquad : ModEq(p · m,m · t · (m · t) · x,0)
  41. 0041specialize multiple_implies_balanced_zero_congruence (p * m)
  42. 0042specialize multiple_implies_balanced_zero_congruence (((m * t) * (m * t)) * x)
  43. 0043apply multiple_implies_balanced_zero_congruence
  44. 0044specialize multiple_mul_right (p * m)
  45. 0045specialize multiple_mul_right ((m * t) * (m * t))
  46. 0046specialize multiple_mul_right x
  47. 0047apply multiple_mul_right
  48. 0048exact hsquare
  49. 0049have hlinear : ModEq(p · m,n + m · t · d,0)
  50. 0050specialize hensel_mod_add_zero_cancel (p * m)
  51. 0051specialize hensel_mod_add_zero_cancel (n + (m * t) * d)
  52. 0052specialize hensel_mod_add_zero_cancel (((m * t) * (m * t)) * x)
  53. 0053apply hensel_mod_add_zero_cancel
  54. 0054rewrite <- htaylor_witness
  55. 0055exact hroot
  56. 0056exact hquad
  57. 0057split
  58. 0058exact ht
  59. 0059specialize mod_eq_unscale_nonzero m
  60. 0060specialize mod_eq_unscale_nonzero p
  61. 0061specialize mod_eq_unscale_nonzero (q + d * t)
  62. 0062specialize mod_eq_unscale_nonzero 0
  63. 0063apply mod_eq_unscale_nonzero
  64. 0064exact hm
  65. 0065have hproduct : m * p = p * m
  66. 0066apply mul_comm
  67. 0067rewrite hproduct
  68. 0068rewrite hproduct
  69. 0069have hzero : m * 0 = 0
  70. 0070simp
  71. 0071rewrite hzero
  72. 0072have hidentity : m * (q + d * t) = n + (m * t) * d
  73. 0073rewrite hn
  74. 0074specialize hensel_lift_linear_identity m
  75. 0075specialize hensel_lift_linear_identity d
  76. 0076specialize hensel_lift_linear_identity q
  77. 0077specialize hensel_lift_linear_identity t
  78. 0078apply hensel_lift_linear_identity
  79. 0079rewrite hidentity
  80. 0080exact hlinear