TH0012

beta_horner_hensel_lift_divisibility

A real bounded simple-root correction lifts an arbitrary beta-coded polynomial root from m to p*m whenever p divides m.

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

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

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) · 1HenselCorrection(d,p,q,t) · 1Dvd(d,n) · 1

Actual proof prerequisites

beta_horner_taylor_remainder_existshensel_correction_implies_multiplehensel_linear_correction_multiplehensel_square_shift_multiplemultiple_mul_right · checked external prerequisitemultiple_add · checked external prerequisite
Original expanded first-order statement 
forall b c a l n d m p s q t y. ~(p = 0) -> (exists ff_u_hd_pth_lift_pair ff_v_hd_pth_lift_pair ff_d_hd_pth_lift_pair ff_e_hd_pth_lift_pair. ((((((exists fs_h_ph_hd_pth_lift_pair_body_value_start. fs_h_ph_hd_pth_lift_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_value_start. ff_u_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_value_start * S ((S (0)) * ff_v_hd_pth_lift_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_value_terminal. fs_h_ph_hd_pth_lift_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_value_terminal. ff_u_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_value_terminal * S ((S (l)) * ff_v_hd_pth_lift_pair) + (n))) /\ forall ff_i_ph_hd_pth_lift_pair_body_value_steps. (exists ph_bound_hd_pth_lift_pair_body_value_steps. ph_bound_hd_pth_lift_pair_body_value_steps + S ff_i_ph_hd_pth_lift_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_lift_pair_body_value_steps ff_previous_ph_hd_pth_lift_pair_body_value_steps ff_current_ph_hd_pth_lift_pair_body_value_steps. ((((exists fs_h_ph_hd_pth_lift_pair_body_value_steps_coefficient. fs_h_ph_hd_pth_lift_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_lift_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_lift_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_lift_pair_body_value_steps_coefficient. b = fs_q_ph_hd_pth_lift_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_lift_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_lift_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_value_steps_before. fs_h_ph_hd_pth_lift_pair_body_value_steps_before + S (ff_previous_ph_hd_pth_lift_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_lift_pair_body_value_steps)) * ff_v_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_value_steps_before. ff_u_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_value_steps_before * S ((S (ff_i_ph_hd_pth_lift_pair_body_value_steps)) * ff_v_hd_pth_lift_pair) + (ff_previous_ph_hd_pth_lift_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_value_steps_after. fs_h_ph_hd_pth_lift_pair_body_value_steps_after + S (ff_current_ph_hd_pth_lift_pair_body_value_steps) = S ((S (S ff_i_ph_hd_pth_lift_pair_body_value_steps)) * ff_v_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_value_steps_after. ff_u_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_lift_pair_body_value_steps)) * ff_v_hd_pth_lift_pair) + (ff_current_ph_hd_pth_lift_pair_body_value_steps))) /\ ff_current_ph_hd_pth_lift_pair_body_value_steps = ff_previous_ph_hd_pth_lift_pair_body_value_steps * a + ff_coefficient_ph_hd_pth_lift_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_lift_pair_body_derivative_start. fs_h_ph_hd_pth_lift_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_derivative_start. ff_d_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_derivative_start * S ((S (0)) * ff_e_hd_pth_lift_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_derivative_terminal. fs_h_ph_hd_pth_lift_pair_body_derivative_terminal + S (d) = S ((S (l)) * ff_e_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_derivative_terminal. ff_d_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_lift_pair) + (d))) /\ forall ff_i_ph_hd_pth_lift_pair_body_derivative_steps. (exists ph_bound_hd_pth_lift_pair_body_derivative_steps. ph_bound_hd_pth_lift_pair_body_derivative_steps + S ff_i_ph_hd_pth_lift_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_lift_pair_body_derivative_steps ff_previous_ph_hd_pth_lift_pair_body_derivative_steps ff_current_ph_hd_pth_lift_pair_body_derivative_steps. ((((exists fs_h_ph_hd_pth_lift_pair_body_derivative_steps_coefficient. fs_h_ph_hd_pth_lift_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_lift_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_v_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_derivative_steps_coefficient. ff_u_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_v_hd_pth_lift_pair) + (ff_coefficient_ph_hd_pth_lift_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_derivative_steps_before. fs_h_ph_hd_pth_lift_pair_body_derivative_steps_before + S (ff_previous_ph_hd_pth_lift_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_e_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_derivative_steps_before. ff_d_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_e_hd_pth_lift_pair) + (ff_previous_ph_hd_pth_lift_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_lift_pair_body_derivative_steps_after. fs_h_ph_hd_pth_lift_pair_body_derivative_steps_after + S (ff_current_ph_hd_pth_lift_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_e_hd_pth_lift_pair)) /\ exists fs_q_ph_hd_pth_lift_pair_body_derivative_steps_after. ff_d_hd_pth_lift_pair = fs_q_ph_hd_pth_lift_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_lift_pair_body_derivative_steps)) * ff_e_hd_pth_lift_pair) + (ff_current_ph_hd_pth_lift_pair_body_derivative_steps))) /\ ff_current_ph_hd_pth_lift_pair_body_derivative_steps = ff_previous_ph_hd_pth_lift_pair_body_derivative_steps * a + ff_coefficient_ph_hd_pth_lift_pair_body_derivative_steps)))))))) -> (exists ff_u_ph_pth_lift_value ff_v_ph_pth_lift_value. ((((exists fs_h_ph_pth_lift_value_body_start. fs_h_ph_pth_lift_value_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_lift_value)) /\ exists fs_q_ph_pth_lift_value_body_start. ff_u_ph_pth_lift_value = fs_q_ph_pth_lift_value_body_start * S ((S (0)) * ff_v_ph_pth_lift_value) + (0))) /\ ((((exists fs_h_ph_pth_lift_value_body_terminal. fs_h_ph_pth_lift_value_body_terminal + S (y) = S ((S (l)) * ff_v_ph_pth_lift_value)) /\ exists fs_q_ph_pth_lift_value_body_terminal. ff_u_ph_pth_lift_value = fs_q_ph_pth_lift_value_body_terminal * S ((S (l)) * ff_v_ph_pth_lift_value) + (y))) /\ forall ff_i_ph_pth_lift_value_body_steps. (exists ph_bound_pth_lift_value_body_steps. ph_bound_pth_lift_value_body_steps + S ff_i_ph_pth_lift_value_body_steps = l) -> exists ff_coefficient_ph_pth_lift_value_body_steps ff_previous_ph_pth_lift_value_body_steps ff_current_ph_pth_lift_value_body_steps. ((((exists fs_h_ph_pth_lift_value_body_steps_coefficient. fs_h_ph_pth_lift_value_body_steps_coefficient + S (ff_coefficient_ph_pth_lift_value_body_steps) = S ((S (ff_i_ph_pth_lift_value_body_steps)) * c)) /\ exists fs_q_ph_pth_lift_value_body_steps_coefficient. b = fs_q_ph_pth_lift_value_body_steps_coefficient * S ((S (ff_i_ph_pth_lift_value_body_steps)) * c) + (ff_coefficient_ph_pth_lift_value_body_steps))) /\ ((((exists fs_h_ph_pth_lift_value_body_steps_before. fs_h_ph_pth_lift_value_body_steps_before + S (ff_previous_ph_pth_lift_value_body_steps) = S ((S (ff_i_ph_pth_lift_value_body_steps)) * ff_v_ph_pth_lift_value)) /\ exists fs_q_ph_pth_lift_value_body_steps_before. ff_u_ph_pth_lift_value = fs_q_ph_pth_lift_value_body_steps_before * S ((S (ff_i_ph_pth_lift_value_body_steps)) * ff_v_ph_pth_lift_value) + (ff_previous_ph_pth_lift_value_body_steps))) /\ ((((exists fs_h_ph_pth_lift_value_body_steps_after. fs_h_ph_pth_lift_value_body_steps_after + S (ff_current_ph_pth_lift_value_body_steps) = S ((S (S ff_i_ph_pth_lift_value_body_steps)) * ff_v_ph_pth_lift_value)) /\ exists fs_q_ph_pth_lift_value_body_steps_after. ff_u_ph_pth_lift_value = fs_q_ph_pth_lift_value_body_steps_after * S ((S (S ff_i_ph_pth_lift_value_body_steps)) * ff_v_ph_pth_lift_value) + (ff_current_ph_pth_lift_value_body_steps))) /\ ff_current_ph_pth_lift_value_body_steps = ff_previous_ph_pth_lift_value_body_steps * (a + m * t) + ff_coefficient_ph_pth_lift_value_body_steps)))))) -> m = p * s -> n = m * q -> (((exists ff_lt_pth_lift_correction_bound. ff_lt_pth_lift_correction_bound + S t = p) /\ (exists hgcrt_mod_left_pth_lift_correction_annihilation hgcrt_mod_right_pth_lift_correction_annihilation. (q + d * t) + p * hgcrt_mod_left_pth_lift_correction_annihilation = 0 + p * hgcrt_mod_right_pth_lift_correction_annihilation))) -> exists w. y = (p * m) * w

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

73 script commands · 14 reading checkpoints · 6 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 (4)
beta horner taylor remainder existshensel correction implies multiplehensel linear correction multiplehensel square shift multiple
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–18

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

  1. L11
    intro t
  2. L12
    intro y
  3. L13
    intro hp
  4. L14
    intro hpair
  5. L15
    intro hvalue
  6. L16
    intro hfactor
  7. L17
    intro hroot
  8. L18
    intro hcorrection
03Establish htaylorL19–28

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

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

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

  1. L29
    exact hpair
  2. L30
    exact hvalue
05Separate the logical casesL31–31

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

  1. L31
    cases htaylor
06Establish hcorrection_multipleL32–39

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

  1. L32
    have hcorrection_multiple : exists w. q + d * t = p * w
  2. L33
    specialize hensel_correction_implies_multiple d
  3. L34
    specialize hensel_correction_implies_multiple p
  4. L35
    specialize hensel_correction_implies_multiple q
  5. L36
    specialize hensel_correction_implies_multiple t
  6. L37
    apply hensel_correction_implies_multiple
  7. L38
    exact hp
  8. L39
    exact hcorrection
07Establish hlinearL40–48

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

  1. L40
    have hlinear : exists w. n + (m * t) * d = (p * m) * w
  2. L41
    rewrite hroot
  3. L42
    specialize hensel_linear_correction_multiple m
  4. L43
    specialize hensel_linear_correction_multiple d
  5. L44
    specialize hensel_linear_correction_multiple q
  6. L45
    specialize hensel_linear_correction_multiple t
  7. L46
    specialize hensel_linear_correction_multiple p
  8. L47
    apply hensel_linear_correction_multiple
  9. L48
    exact hcorrection_multiple
08Establish hsquareL49–55

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

  1. L49
    have hsquare : exists w. (m * t) * (m * t) = (p * m) * w
  2. L50
    specialize hensel_square_shift_multiple m
  3. L51
    specialize hensel_square_shift_multiple t
  4. L52
    specialize hensel_square_shift_multiple p
  5. L53
    specialize hensel_square_shift_multiple s
  6. L54
    apply hensel_square_shift_multiple
  7. L55
    exact hfactor
09Establish hquadraticL56–61

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

  1. L56
    have hquadratic : exists w. ((m * t) * (m * t)) * x = (p * m) * w
  2. L57
    specialize multiple_mul_right (p * m)
  3. L58
    specialize multiple_mul_right ((m * t) * (m * t))
  4. L59
    specialize multiple_mul_right x
  5. L60
    apply multiple_mul_right
  6. L61
    exact hsquare
10Establish hsumL62–68

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

  1. L62
    have hsum : exists w. (n + (m * t) * d) + ((m * t) * (m * t)) * x = (p * m) * w
  2. L63
    specialize multiple_add (p * m)
  3. L64
    specialize multiple_add (n + (m * t) * d)
  4. L65
    specialize multiple_add (((m * t) * (m * t)) * x)
  5. L66
    apply multiple_add
  6. L67
    exact hlinear
  7. L68
    exact hquadratic
11Separate the logical casesL69–69

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

  1. L69
    cases hsum
12Construct an explicit witnessL70–70

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

  1. L70
    exists x1
13Calculate and transport equalitiesL71–71

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

  1. L71
    trans (n + (m * t) * d) + ((m * t) * (m * t)) * x
14Use earlier factsL72–73

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

  1. L72
    exact htaylor_witness
  2. L73
    exact hsum_witness

Library-wide reading audit

Original defined command ledger · 73 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 hp
  14. 0014intro hpair
  15. 0015intro hvalue
  16. 0016intro hfactor
  17. 0017intro hroot
  18. 0018intro hcorrection
  19. 0019have htaylor : exists w. y = (n + (m * t) * d) + ((m * t) * (m * t)) * w
  20. 0020specialize beta_horner_taylor_remainder_exists b
  21. 0021specialize beta_horner_taylor_remainder_exists c
  22. 0022specialize beta_horner_taylor_remainder_exists a
  23. 0023specialize beta_horner_taylor_remainder_exists (m * t)
  24. 0024specialize beta_horner_taylor_remainder_exists l
  25. 0025specialize beta_horner_taylor_remainder_exists n
  26. 0026specialize beta_horner_taylor_remainder_exists d
  27. 0027specialize beta_horner_taylor_remainder_exists y
  28. 0028apply beta_horner_taylor_remainder_exists
  29. 0029exact hpair
  30. 0030exact hvalue
  31. 0031cases htaylor
  32. 0032have hcorrection_multiple : exists w. q + d * t = p * w
  33. 0033specialize hensel_correction_implies_multiple d
  34. 0034specialize hensel_correction_implies_multiple p
  35. 0035specialize hensel_correction_implies_multiple q
  36. 0036specialize hensel_correction_implies_multiple t
  37. 0037apply hensel_correction_implies_multiple
  38. 0038exact hp
  39. 0039exact hcorrection
  40. 0040have hlinear : exists w. n + (m * t) * d = (p * m) * w
  41. 0041rewrite hroot
  42. 0042specialize hensel_linear_correction_multiple m
  43. 0043specialize hensel_linear_correction_multiple d
  44. 0044specialize hensel_linear_correction_multiple q
  45. 0045specialize hensel_linear_correction_multiple t
  46. 0046specialize hensel_linear_correction_multiple p
  47. 0047apply hensel_linear_correction_multiple
  48. 0048exact hcorrection_multiple
  49. 0049have hsquare : exists w. (m * t) * (m * t) = (p * m) * w
  50. 0050specialize hensel_square_shift_multiple m
  51. 0051specialize hensel_square_shift_multiple t
  52. 0052specialize hensel_square_shift_multiple p
  53. 0053specialize hensel_square_shift_multiple s
  54. 0054apply hensel_square_shift_multiple
  55. 0055exact hfactor
  56. 0056have hquadratic : exists w. ((m * t) * (m * t)) * x = (p * m) * w
  57. 0057specialize multiple_mul_right (p * m)
  58. 0058specialize multiple_mul_right ((m * t) * (m * t))
  59. 0059specialize multiple_mul_right x
  60. 0060apply multiple_mul_right
  61. 0061exact hsquare
  62. 0062have hsum : exists w. (n + (m * t) * d) + ((m * t) * (m * t)) * x = (p * m) * w
  63. 0063specialize multiple_add (p * m)
  64. 0064specialize multiple_add (n + (m * t) * d)
  65. 0065specialize multiple_add (((m * t) * (m * t)) * x)
  66. 0066apply multiple_add
  67. 0067exact hlinear
  68. 0068exact hquadratic
  69. 0069cases hsum
  70. 0070exists x1
  71. 0071trans (n + (m * t) * d) + ((m * t) * (m * t)) * x
  72. 0072exact htaylor_witness
  73. 0073exact hsum_witness