TH0012

beta_horner_hensel_lift_divisibility

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 6 declared prerequisites and contains 73 exact native proof lines.

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

Proof neighborhood

Direct dependencies

TH0008 beta_horner_taylor_remainder_exists TH000F hensel_correction_implies_multiple TH0010 hensel_linear_correction_multiple TH0011 hensel_square_shift_multiple multiple_mul_right Stable theorem; checked-use authorized multiple_add Stable theorem; checked-use authorized

Direct dependents

TH0013 beta_horner_hensel_lift_exists

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

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.

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

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