TH000D

beta_horner_taylor_square_congruence

Every polynomial value at a shifted natural point is congruent to its exact first-order Taylor linearization modulo the square shift.

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. ∀ t. ∀ h. ∀ l. ∀ n. ∀ d. ∀ z. HornerDerivative(b,c,t,l,n,d) → Horner(b,c,t + h,l,z) → ModEq(h · h,z,n + h · d)

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) · 1ModEq(m,a,b) · 1

Actual proof prerequisites

beta_horner_taylor_remainder_exists
Original expanded first-order statement 
forall b c t h l n d z. (exists ff_u_hd_pth_taylor_pair ff_v_hd_pth_taylor_pair ff_d_hd_pth_taylor_pair ff_e_hd_pth_taylor_pair. ((((((exists fs_h_ph_hd_pth_taylor_pair_body_value_start. fs_h_ph_hd_pth_taylor_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_taylor_pair)) /\ exists fs_q_ph_hd_pth_taylor_pair_body_value_start. ff_u_hd_pth_taylor_pair = fs_q_ph_hd_pth_taylor_pair_body_value_start * S ((S (0)) * ff_v_hd_pth_taylor_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_taylor_pair_body_value_terminal. fs_h_ph_hd_pth_taylor_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_pth_taylor_pair)) /\ exists fs_q_ph_hd_pth_taylor_pair_body_value_terminal. ff_u_hd_pth_taylor_pair = fs_q_ph_hd_pth_taylor_pair_body_value_terminal * S ((S (l)) * ff_v_hd_pth_taylor_pair) + (n))) /\ forall ff_i_ph_hd_pth_taylor_pair_body_value_steps. (exists ph_bound_hd_pth_taylor_pair_body_value_steps. ph_bound_hd_pth_taylor_pair_body_value_steps + S ff_i_ph_hd_pth_taylor_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_taylor_pair_body_value_steps ff_previous_ph_hd_pth_taylor_pair_body_value_steps ff_current_ph_hd_pth_taylor_pair_body_value_steps. ((((exists fs_h_ph_hd_pth_taylor_pair_body_value_steps_coefficient. fs_h_ph_hd_pth_taylor_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_taylor_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_taylor_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_taylor_pair_body_value_steps_coefficient. b = fs_q_ph_hd_pth_taylor_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_taylor_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_taylor_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_taylor_pair_body_value_steps_before. fs_h_ph_hd_pth_taylor_pair_body_value_steps_before + S (ff_previous_ph_hd_pth_taylor_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_taylor_pair_body_value_steps)) * ff_v_hd_pth_taylor_pair)) /\ exists fs_q_ph_hd_pth_taylor_pair_body_value_steps_before. ff_u_hd_pth_taylor_pair = fs_q_ph_hd_pth_taylor_pair_body_value_steps_before * S ((S (ff_i_ph_hd_pth_taylor_pair_body_value_steps)) * ff_v_hd_pth_taylor_pair) + (ff_previous_ph_hd_pth_taylor_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_taylor_pair_body_value_steps_after. fs_h_ph_hd_pth_taylor_pair_body_value_steps_after + S (ff_current_ph_hd_pth_taylor_pair_body_value_steps) = S ((S (S ff_i_ph_hd_pth_taylor_pair_body_value_steps)) * ff_v_hd_pth_taylor_pair)) /\ exists fs_q_ph_hd_pth_taylor_pair_body_value_steps_after. ff_u_hd_pth_taylor_pair = fs_q_ph_hd_pth_taylor_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_taylor_pair_body_value_steps)) * ff_v_hd_pth_taylor_pair) + (ff_current_ph_hd_pth_taylor_pair_body_value_steps))) /\ ff_current_ph_hd_pth_taylor_pair_body_value_steps = ff_previous_ph_hd_pth_taylor_pair_body_value_steps * t + ff_coefficient_ph_hd_pth_taylor_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_taylor_pair_body_derivative_start. fs_h_ph_hd_pth_taylor_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_taylor_pair)) /\ exists fs_q_ph_hd_pth_taylor_pair_body_derivative_start. ff_d_hd_pth_taylor_pair = fs_q_ph_hd_pth_taylor_pair_body_derivative_start * S ((S (0)) * ff_e_hd_pth_taylor_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_taylor_pair_body_derivative_terminal. fs_h_ph_hd_pth_taylor_pair_body_derivative_terminal + S (d) = S ((S (l)) * ff_e_hd_pth_taylor_pair)) /\ exists fs_q_ph_hd_pth_taylor_pair_body_derivative_terminal. ff_d_hd_pth_taylor_pair = fs_q_ph_hd_pth_taylor_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_taylor_pair) + (d))) /\ forall ff_i_ph_hd_pth_taylor_pair_body_derivative_steps. (exists ph_bound_hd_pth_taylor_pair_body_derivative_steps. ph_bound_hd_pth_taylor_pair_body_derivative_steps + S ff_i_ph_hd_pth_taylor_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_taylor_pair_body_derivative_steps ff_previous_ph_hd_pth_taylor_pair_body_derivative_steps ff_current_ph_hd_pth_taylor_pair_body_derivative_steps. ((((exists fs_h_ph_hd_pth_taylor_pair_body_derivative_steps_coefficient. fs_h_ph_hd_pth_taylor_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_taylor_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_taylor_pair_body_derivative_steps)) * ff_v_hd_pth_taylor_pair)) /\ exists fs_q_ph_hd_pth_taylor_pair_body_derivative_steps_coefficient. ff_u_hd_pth_taylor_pair = fs_q_ph_hd_pth_taylor_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_taylor_pair_body_derivative_steps)) * ff_v_hd_pth_taylor_pair) + (ff_coefficient_ph_hd_pth_taylor_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_taylor_pair_body_derivative_steps_before. fs_h_ph_hd_pth_taylor_pair_body_derivative_steps_before + S (ff_previous_ph_hd_pth_taylor_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_taylor_pair_body_derivative_steps)) * ff_e_hd_pth_taylor_pair)) /\ exists fs_q_ph_hd_pth_taylor_pair_body_derivative_steps_before. ff_d_hd_pth_taylor_pair = fs_q_ph_hd_pth_taylor_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_taylor_pair_body_derivative_steps)) * ff_e_hd_pth_taylor_pair) + (ff_previous_ph_hd_pth_taylor_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_taylor_pair_body_derivative_steps_after. fs_h_ph_hd_pth_taylor_pair_body_derivative_steps_after + S (ff_current_ph_hd_pth_taylor_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_taylor_pair_body_derivative_steps)) * ff_e_hd_pth_taylor_pair)) /\ exists fs_q_ph_hd_pth_taylor_pair_body_derivative_steps_after. ff_d_hd_pth_taylor_pair = fs_q_ph_hd_pth_taylor_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_taylor_pair_body_derivative_steps)) * ff_e_hd_pth_taylor_pair) + (ff_current_ph_hd_pth_taylor_pair_body_derivative_steps))) /\ ff_current_ph_hd_pth_taylor_pair_body_derivative_steps = ff_previous_ph_hd_pth_taylor_pair_body_derivative_steps * t + ff_coefficient_ph_hd_pth_taylor_pair_body_derivative_steps)))))))) -> (exists ff_u_ph_pth_taylor_shifted ff_v_ph_pth_taylor_shifted. ((((exists fs_h_ph_pth_taylor_shifted_body_start. fs_h_ph_pth_taylor_shifted_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_taylor_shifted)) /\ exists fs_q_ph_pth_taylor_shifted_body_start. ff_u_ph_pth_taylor_shifted = fs_q_ph_pth_taylor_shifted_body_start * S ((S (0)) * ff_v_ph_pth_taylor_shifted) + (0))) /\ ((((exists fs_h_ph_pth_taylor_shifted_body_terminal. fs_h_ph_pth_taylor_shifted_body_terminal + S (z) = S ((S (l)) * ff_v_ph_pth_taylor_shifted)) /\ exists fs_q_ph_pth_taylor_shifted_body_terminal. ff_u_ph_pth_taylor_shifted = fs_q_ph_pth_taylor_shifted_body_terminal * S ((S (l)) * ff_v_ph_pth_taylor_shifted) + (z))) /\ forall ff_i_ph_pth_taylor_shifted_body_steps. (exists ph_bound_pth_taylor_shifted_body_steps. ph_bound_pth_taylor_shifted_body_steps + S ff_i_ph_pth_taylor_shifted_body_steps = l) -> exists ff_coefficient_ph_pth_taylor_shifted_body_steps ff_previous_ph_pth_taylor_shifted_body_steps ff_current_ph_pth_taylor_shifted_body_steps. ((((exists fs_h_ph_pth_taylor_shifted_body_steps_coefficient. fs_h_ph_pth_taylor_shifted_body_steps_coefficient + S (ff_coefficient_ph_pth_taylor_shifted_body_steps) = S ((S (ff_i_ph_pth_taylor_shifted_body_steps)) * c)) /\ exists fs_q_ph_pth_taylor_shifted_body_steps_coefficient. b = fs_q_ph_pth_taylor_shifted_body_steps_coefficient * S ((S (ff_i_ph_pth_taylor_shifted_body_steps)) * c) + (ff_coefficient_ph_pth_taylor_shifted_body_steps))) /\ ((((exists fs_h_ph_pth_taylor_shifted_body_steps_before. fs_h_ph_pth_taylor_shifted_body_steps_before + S (ff_previous_ph_pth_taylor_shifted_body_steps) = S ((S (ff_i_ph_pth_taylor_shifted_body_steps)) * ff_v_ph_pth_taylor_shifted)) /\ exists fs_q_ph_pth_taylor_shifted_body_steps_before. ff_u_ph_pth_taylor_shifted = fs_q_ph_pth_taylor_shifted_body_steps_before * S ((S (ff_i_ph_pth_taylor_shifted_body_steps)) * ff_v_ph_pth_taylor_shifted) + (ff_previous_ph_pth_taylor_shifted_body_steps))) /\ ((((exists fs_h_ph_pth_taylor_shifted_body_steps_after. fs_h_ph_pth_taylor_shifted_body_steps_after + S (ff_current_ph_pth_taylor_shifted_body_steps) = S ((S (S ff_i_ph_pth_taylor_shifted_body_steps)) * ff_v_ph_pth_taylor_shifted)) /\ exists fs_q_ph_pth_taylor_shifted_body_steps_after. ff_u_ph_pth_taylor_shifted = fs_q_ph_pth_taylor_shifted_body_steps_after * S ((S (S ff_i_ph_pth_taylor_shifted_body_steps)) * ff_v_ph_pth_taylor_shifted) + (ff_current_ph_pth_taylor_shifted_body_steps))) /\ ff_current_ph_pth_taylor_shifted_body_steps = ff_previous_ph_pth_taylor_shifted_body_steps * (t + h) + ff_coefficient_ph_pth_taylor_shifted_body_steps)))))) -> (exists hgcrt_mod_left_pth_taylor_square hgcrt_mod_right_pth_taylor_square. z + (h * h) * hgcrt_mod_left_pth_taylor_square = (n + h * d) + (h * h) * hgcrt_mod_right_pth_taylor_square)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

28 script commands · 7 reading checkpoints · 1 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 (1)
beta horner taylor remainder exists
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 t
  4. L4
    intro h
  5. L5
    intro l
  6. L6
    intro n
  7. L7
    intro d
  8. L8
    intro z
  9. L9
    intro hpair
  10. L10
    intro hshifted
02Establish hremL11–20

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

  1. L11
    have hrem : exists q. z = (n + h * d) + (h * h) * q
  2. L12
    specialize beta_horner_taylor_remainder_exists b
  3. L13
    specialize beta_horner_taylor_remainder_exists c
  4. L14
    specialize beta_horner_taylor_remainder_exists t
  5. L15
    specialize beta_horner_taylor_remainder_exists h
  6. L16
    specialize beta_horner_taylor_remainder_exists l
  7. L17
    specialize beta_horner_taylor_remainder_exists n
  8. L18
    specialize beta_horner_taylor_remainder_exists d
  9. L19
    specialize beta_horner_taylor_remainder_exists z
  10. L20
    apply beta_horner_taylor_remainder_exists
03Use earlier factsL21–22

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

  1. L21
    exact hpair
  2. L22
    exact hshifted
04Separate the logical casesL23–23

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

  1. L23
    cases hrem
05Construct an explicit witnessL24–25

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

  1. L24
    exists 0
  2. L25
    exists x
06Calculate and transport equalitiesL26–27

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

  1. L26
    rewrite PA5
  2. L27
    rewrite PA3
07Use earlier factsL28–28

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

  1. L28
    exact hrem_witness

Library-wide reading audit

Original defined command ledger · 28 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro h
  5. 0005intro l
  6. 0006intro n
  7. 0007intro d
  8. 0008intro z
  9. 0009intro hpair
  10. 0010intro hshifted
  11. 0011have hrem : exists q. z = (n + h * d) + (h * h) * q
  12. 0012specialize beta_horner_taylor_remainder_exists b
  13. 0013specialize beta_horner_taylor_remainder_exists c
  14. 0014specialize beta_horner_taylor_remainder_exists t
  15. 0015specialize beta_horner_taylor_remainder_exists h
  16. 0016specialize beta_horner_taylor_remainder_exists l
  17. 0017specialize beta_horner_taylor_remainder_exists n
  18. 0018specialize beta_horner_taylor_remainder_exists d
  19. 0019specialize beta_horner_taylor_remainder_exists z
  20. 0020apply beta_horner_taylor_remainder_exists
  21. 0021exact hpair
  22. 0022exact hshifted
  23. 0023cases hrem
  24. 0024exists 0
  25. 0025exists x
  26. 0026rewrite PA5
  27. 0027rewrite PA3
  28. 0028exact hrem_witness