TH0008

beta_horner_taylor_remainder_exists

Every beta-coded natural polynomial has an exact witnessed quadratic Taylor remainder at every natural 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) → ∃ x. z = n + h · d + h · h · x

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) · 1

Actual proof prerequisites

beta_horner_derivative_empty · checked external prerequisitebeta_horner_eval_empty · checked external prerequisitebeta_horner_derivative_successor_decompose · checked external prerequisitebeta_horner_eval_successor_decompose · checked external prerequisitebeta_at_unique · checked external prerequisitehorner_taylor_successor_identity
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 q. z = (n + h * d) + (h * h) * q

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

93 script commands · 18 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 (1)
horner taylor successor identity

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–4

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
02Induction on lL5–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L5
    induction l
  2. L6
    intro n
  3. L7
    intro d
  4. L8
    intro z
  5. L9
    intro hpair
  6. L10
    intro hshifted
03Establish hzero_pairL11–18

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

  1. L11
    have hzero_pair : (n = 0 /\ d = 0)
  2. L12
    specialize beta_horner_derivative_empty b
  3. L13
    specialize beta_horner_derivative_empty c
  4. L14
    specialize beta_horner_derivative_empty t
  5. L15
    specialize beta_horner_derivative_empty n
  6. L16
    specialize beta_horner_derivative_empty d
  7. L17
    apply beta_horner_derivative_empty
  8. L18
    exact hpair
04Establish hzero_shiftedL19–25

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

  1. L19
    have hzero_shifted : z = 0
  2. L20
    specialize beta_horner_eval_empty b
  3. L21
    specialize beta_horner_eval_empty c
  4. L22
    specialize beta_horner_eval_empty (t + h)
  5. L23
    specialize beta_horner_eval_empty z
  6. L24
    apply beta_horner_eval_empty
  7. L25
    exact hshifted
05Separate the logical casesL26–26

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

  1. L26
    cases hzero_pair
06Construct an explicit witnessL27–27

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

  1. L27
    exists 0
07Calculate and transport equalitiesL28–31

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

  1. L28
    rewrite hzero_shifted
  2. L29
    rewrite hzero_pair_left
  3. L30
    rewrite hzero_pair_right
  4. L31
    simp
08Fix variables and assumptionsL32–36

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

  1. L32
    intro n
  2. L33
    intro d
  3. L34
    intro z
  4. L35
    intro hpair
  5. L36
    intro hshifted
09Establish hfirstL37–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner derivative successor decompose.

  1. L37
    have hfirst : ∃ a. ∃ r. ∃ q. Beta(b,c,l,a) ∧ (HornerDerivative(b,c,t,l,r,q) ∧ (n = r · t + a ∧ d = q · t + r))Definitions: BetaHornerDerivativeOriginal native command in the exact edition
  2. L38
    specialize beta_horner_derivative_successor_decompose b
  3. L39
    specialize beta_horner_derivative_successor_decompose c
  4. L40
    specialize beta_horner_derivative_successor_decompose t
  5. L41
    specialize beta_horner_derivative_successor_decompose l
  6. L42
    specialize beta_horner_derivative_successor_decompose n
  7. L43
    specialize beta_horner_derivative_successor_decompose d
  8. L44
    apply beta_horner_derivative_successor_decompose
  9. L45
    exact hpair
10Separate the logical casesL46–51

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

  1. L46
    cases hfirst
  2. L47
    cases hfirst_witness
  3. L48
    cases hfirst_witness_witness
  4. L49
    cases hfirst_witness_witness_witness
  5. L50
    cases hfirst_witness_witness_witness_right
  6. L51
    cases hfirst_witness_witness_witness_right_right
11Establish hsecondL52–59

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner eval successor decompose.

  1. L52
    have hsecond : ∃ a. ∃ r. Beta(b,c,l,a) ∧ (Horner(b,c,t + h,l,r) ∧ z = r · (t + h) + a)Definitions: BetaHornerOriginal native command in the exact edition
  2. L53
    specialize beta_horner_eval_successor_decompose b
  3. L54
    specialize beta_horner_eval_successor_decompose c
  4. L55
    specialize beta_horner_eval_successor_decompose (t + h)
  5. L56
    specialize beta_horner_eval_successor_decompose l
  6. L57
    specialize beta_horner_eval_successor_decompose z
  7. L58
    apply beta_horner_eval_successor_decompose
  8. L59
    exact hshifted
12Separate the logical casesL60–63

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

  1. L60
    cases hsecond
  2. L61
    cases hsecond_witness
  3. L62
    cases hsecond_witness_witness
  4. L63
    cases hsecond_witness_witness_right
13Establish hcoefficientL64–72

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L64
    have hcoefficient : x = x3
  2. L65
    specialize beta_at_unique b
  3. L66
    specialize beta_at_unique c
  4. L67
    specialize beta_at_unique l
  5. L68
    specialize beta_at_unique x
  6. L69
    specialize beta_at_unique x3
  7. L70
    apply beta_at_unique
  8. L71
    exact hfirst_witness_witness_witness_left
  9. L72
    exact hsecond_witness_witness_left
14Establish hprefixL73–79

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

  1. L73
    have hprefix : exists q. x4 = (x1 + h * x2) + (h * h) * q
  2. L74
    specialize IH x1
  3. L75
    specialize IH x2
  4. L76
    specialize IH x4
  5. L77
    apply IH
  6. L78
    exact hfirst_witness_witness_witness_right_left
  7. L79
    exact hsecond_witness_witness_right_left
15Separate the logical casesL80–80

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

  1. L80
    cases hprefix
16Construct an explicit witnessL81–81

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

  1. L81
    exists x5 * (t + h) + x2
17Calculate and transport equalitiesL82–86

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

  1. L82
    rewrite hsecond_witness_witness_right_right
  2. L83
    rewrite hfirst_witness_witness_witness_right_right_left
  3. L84
    rewrite hfirst_witness_witness_witness_right_right_right
  4. L85
    rewrite hprefix_witness
  5. L86
    rewrite <- hcoefficient
18Use earlier factsL87–93

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

  1. L87
    specialize horner_taylor_successor_identity x1
  2. L88
    specialize horner_taylor_successor_identity x2
  3. L89
    specialize horner_taylor_successor_identity h
  4. L90
    specialize horner_taylor_successor_identity x5
  5. L91
    specialize horner_taylor_successor_identity t
  6. L92
    specialize horner_taylor_successor_identity x
  7. L93
    exact horner_taylor_successor_identity

Library-wide reading audit

Original defined command ledger · 93 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro h
  5. 0005induction l
  6. 0006intro n
  7. 0007intro d
  8. 0008intro z
  9. 0009intro hpair
  10. 0010intro hshifted
  11. 0011have hzero_pair : (n = 0 /\ d = 0)
  12. 0012specialize beta_horner_derivative_empty b
  13. 0013specialize beta_horner_derivative_empty c
  14. 0014specialize beta_horner_derivative_empty t
  15. 0015specialize beta_horner_derivative_empty n
  16. 0016specialize beta_horner_derivative_empty d
  17. 0017apply beta_horner_derivative_empty
  18. 0018exact hpair
  19. 0019have hzero_shifted : z = 0
  20. 0020specialize beta_horner_eval_empty b
  21. 0021specialize beta_horner_eval_empty c
  22. 0022specialize beta_horner_eval_empty (t + h)
  23. 0023specialize beta_horner_eval_empty z
  24. 0024apply beta_horner_eval_empty
  25. 0025exact hshifted
  26. 0026cases hzero_pair
  27. 0027exists 0
  28. 0028rewrite hzero_shifted
  29. 0029rewrite hzero_pair_left
  30. 0030rewrite hzero_pair_right
  31. 0031simp
  32. 0032intro n
  33. 0033intro d
  34. 0034intro z
  35. 0035intro hpair
  36. 0036intro hshifted
  37. 0037have hfirst : exists a r q. ((((exists fs_h_pth_taylor_first_coefficient. fs_h_pth_taylor_first_coefficient + S (a) = S ((S (l)) * c)) /\ exists fs_q_pth_taylor_first_coefficient. b = fs_q_pth_taylor_first_coefficient * S ((S (l)) * c) + (a))) /\ ((exists ff_u_hd_pth_taylor_first_prefix ff_v_hd_pth_taylor_first_prefix ff_d_hd_pth_taylor_first_prefix ff_e_hd_pth_taylor_first_prefix. ((((((exists fs_h_ph_hd_pth_taylor_first_prefix_body_value_start. fs_h_ph_hd_pth_taylor_first_prefix_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_taylor_first_prefix)) /\ exists fs_q_ph_hd_pth_taylor_first_prefix_body_value_start. ff_u_hd_pth_taylor_first_prefix = fs_q_ph_hd_pth_taylor_first_prefix_body_value_start * S ((S (0)) * ff_v_hd_pth_taylor_first_prefix) + (0))) /\ ((((exists fs_h_ph_hd_pth_taylor_first_prefix_body_value_terminal. fs_h_ph_hd_pth_taylor_first_prefix_body_value_terminal + S (r) = S ((S (l)) * ff_v_hd_pth_taylor_first_prefix)) /\ exists fs_q_ph_hd_pth_taylor_first_prefix_body_value_terminal. ff_u_hd_pth_taylor_first_prefix = fs_q_ph_hd_pth_taylor_first_prefix_body_value_terminal * S ((S (l)) * ff_v_hd_pth_taylor_first_prefix) + (r))) /\ forall ff_i_ph_hd_pth_taylor_first_prefix_body_value_steps. (exists ph_bound_hd_pth_taylor_first_prefix_body_value_steps. ph_bound_hd_pth_taylor_first_prefix_body_value_steps + S ff_i_ph_hd_pth_taylor_first_prefix_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_taylor_first_prefix_body_value_steps ff_previous_ph_hd_pth_taylor_first_prefix_body_value_steps ff_current_ph_hd_pth_taylor_first_prefix_body_value_steps. ((((exists fs_h_ph_hd_pth_taylor_first_prefix_body_value_steps_coefficient. fs_h_ph_hd_pth_taylor_first_prefix_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_taylor_first_prefix_body_value_steps) = S ((S (ff_i_ph_hd_pth_taylor_first_prefix_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_taylor_first_prefix_body_value_steps_coefficient. b = fs_q_ph_hd_pth_taylor_first_prefix_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_taylor_first_prefix_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_taylor_first_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_taylor_first_prefix_body_value_steps_before. fs_h_ph_hd_pth_taylor_first_prefix_body_value_steps_before + S (ff_previous_ph_hd_pth_taylor_first_prefix_body_value_steps) = S ((S (ff_i_ph_hd_pth_taylor_first_prefix_body_value_steps)) * ff_v_hd_pth_taylor_first_prefix)) /\ exists fs_q_ph_hd_pth_taylor_first_prefix_body_value_steps_before. ff_u_hd_pth_taylor_first_prefix = fs_q_ph_hd_pth_taylor_first_prefix_body_value_steps_before * S ((S (ff_i_ph_hd_pth_taylor_first_prefix_body_value_steps)) * ff_v_hd_pth_taylor_first_prefix) + (ff_previous_ph_hd_pth_taylor_first_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_taylor_first_prefix_body_value_steps_after. fs_h_ph_hd_pth_taylor_first_prefix_body_value_steps_after + S (ff_current_ph_hd_pth_taylor_first_prefix_body_value_steps) = S ((S (S ff_i_ph_hd_pth_taylor_first_prefix_body_value_steps)) * ff_v_hd_pth_taylor_first_prefix)) /\ exists fs_q_ph_hd_pth_taylor_first_prefix_body_value_steps_after. ff_u_hd_pth_taylor_first_prefix = fs_q_ph_hd_pth_taylor_first_prefix_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_taylor_first_prefix_body_value_steps)) * ff_v_hd_pth_taylor_first_prefix) + (ff_current_ph_hd_pth_taylor_first_prefix_body_value_steps))) /\ ff_current_ph_hd_pth_taylor_first_prefix_body_value_steps = ff_previous_ph_hd_pth_taylor_first_prefix_body_value_steps * t + ff_coefficient_ph_hd_pth_taylor_first_prefix_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_taylor_first_prefix_body_derivative_start. fs_h_ph_hd_pth_taylor_first_prefix_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_taylor_first_prefix)) /\ exists fs_q_ph_hd_pth_taylor_first_prefix_body_derivative_start. ff_d_hd_pth_taylor_first_prefix = fs_q_ph_hd_pth_taylor_first_prefix_body_derivative_start * S ((S (0)) * ff_e_hd_pth_taylor_first_prefix) + (0))) /\ ((((exists fs_h_ph_hd_pth_taylor_first_prefix_body_derivative_terminal. fs_h_ph_hd_pth_taylor_first_prefix_body_derivative_terminal + S (q) = S ((S (l)) * ff_e_hd_pth_taylor_first_prefix)) /\ exists fs_q_ph_hd_pth_taylor_first_prefix_body_derivative_terminal. ff_d_hd_pth_taylor_first_prefix = fs_q_ph_hd_pth_taylor_first_prefix_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_taylor_first_prefix) + (q))) /\ forall ff_i_ph_hd_pth_taylor_first_prefix_body_derivative_steps. (exists ph_bound_hd_pth_taylor_first_prefix_body_derivative_steps. ph_bound_hd_pth_taylor_first_prefix_body_derivative_steps + S ff_i_ph_hd_pth_taylor_first_prefix_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_taylor_first_prefix_body_derivative_steps ff_previous_ph_hd_pth_taylor_first_prefix_body_derivative_steps ff_current_ph_hd_pth_taylor_first_prefix_body_derivative_steps. ((((exists fs_h_ph_hd_pth_taylor_first_prefix_body_derivative_steps_coefficient. fs_h_ph_hd_pth_taylor_first_prefix_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_taylor_first_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_taylor_first_prefix_body_derivative_steps)) * ff_v_hd_pth_taylor_first_prefix)) /\ exists fs_q_ph_hd_pth_taylor_first_prefix_body_derivative_steps_coefficient. ff_u_hd_pth_taylor_first_prefix = fs_q_ph_hd_pth_taylor_first_prefix_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_taylor_first_prefix_body_derivative_steps)) * ff_v_hd_pth_taylor_first_prefix) + (ff_coefficient_ph_hd_pth_taylor_first_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_taylor_first_prefix_body_derivative_steps_before. fs_h_ph_hd_pth_taylor_first_prefix_body_derivative_steps_before + S (ff_previous_ph_hd_pth_taylor_first_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_taylor_first_prefix_body_derivative_steps)) * ff_e_hd_pth_taylor_first_prefix)) /\ exists fs_q_ph_hd_pth_taylor_first_prefix_body_derivative_steps_before. ff_d_hd_pth_taylor_first_prefix = fs_q_ph_hd_pth_taylor_first_prefix_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_taylor_first_prefix_body_derivative_steps)) * ff_e_hd_pth_taylor_first_prefix) + (ff_previous_ph_hd_pth_taylor_first_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_taylor_first_prefix_body_derivative_steps_after. fs_h_ph_hd_pth_taylor_first_prefix_body_derivative_steps_after + S (ff_current_ph_hd_pth_taylor_first_prefix_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_taylor_first_prefix_body_derivative_steps)) * ff_e_hd_pth_taylor_first_prefix)) /\ exists fs_q_ph_hd_pth_taylor_first_prefix_body_derivative_steps_after. ff_d_hd_pth_taylor_first_prefix = fs_q_ph_hd_pth_taylor_first_prefix_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_taylor_first_prefix_body_derivative_steps)) * ff_e_hd_pth_taylor_first_prefix) + (ff_current_ph_hd_pth_taylor_first_prefix_body_derivative_steps))) /\ ff_current_ph_hd_pth_taylor_first_prefix_body_derivative_steps = ff_previous_ph_hd_pth_taylor_first_prefix_body_derivative_steps * t + ff_coefficient_ph_hd_pth_taylor_first_prefix_body_derivative_steps)))))))) /\ ((n = r * t + a) /\ d = q * t + r)))
  38. 0038specialize beta_horner_derivative_successor_decompose b
  39. 0039specialize beta_horner_derivative_successor_decompose c
  40. 0040specialize beta_horner_derivative_successor_decompose t
  41. 0041specialize beta_horner_derivative_successor_decompose l
  42. 0042specialize beta_horner_derivative_successor_decompose n
  43. 0043specialize beta_horner_derivative_successor_decompose d
  44. 0044apply beta_horner_derivative_successor_decompose
  45. 0045exact hpair
  46. 0046cases hfirst
  47. 0047cases hfirst_witness
  48. 0048cases hfirst_witness_witness
  49. 0049cases hfirst_witness_witness_witness
  50. 0050cases hfirst_witness_witness_witness_right
  51. 0051cases hfirst_witness_witness_witness_right_right
  52. 0052have hsecond : exists a r. ((((exists fs_h_pth_taylor_second_coefficient. fs_h_pth_taylor_second_coefficient + S (a) = S ((S (l)) * c)) /\ exists fs_q_pth_taylor_second_coefficient. b = fs_q_pth_taylor_second_coefficient * S ((S (l)) * c) + (a))) /\ ((exists ff_u_ph_pth_taylor_second_prefix ff_v_ph_pth_taylor_second_prefix. ((((exists fs_h_ph_pth_taylor_second_prefix_body_start. fs_h_ph_pth_taylor_second_prefix_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_taylor_second_prefix)) /\ exists fs_q_ph_pth_taylor_second_prefix_body_start. ff_u_ph_pth_taylor_second_prefix = fs_q_ph_pth_taylor_second_prefix_body_start * S ((S (0)) * ff_v_ph_pth_taylor_second_prefix) + (0))) /\ ((((exists fs_h_ph_pth_taylor_second_prefix_body_terminal. fs_h_ph_pth_taylor_second_prefix_body_terminal + S (r) = S ((S (l)) * ff_v_ph_pth_taylor_second_prefix)) /\ exists fs_q_ph_pth_taylor_second_prefix_body_terminal. ff_u_ph_pth_taylor_second_prefix = fs_q_ph_pth_taylor_second_prefix_body_terminal * S ((S (l)) * ff_v_ph_pth_taylor_second_prefix) + (r))) /\ forall ff_i_ph_pth_taylor_second_prefix_body_steps. (exists ph_bound_pth_taylor_second_prefix_body_steps. ph_bound_pth_taylor_second_prefix_body_steps + S ff_i_ph_pth_taylor_second_prefix_body_steps = l) -> exists ff_coefficient_ph_pth_taylor_second_prefix_body_steps ff_previous_ph_pth_taylor_second_prefix_body_steps ff_current_ph_pth_taylor_second_prefix_body_steps. ((((exists fs_h_ph_pth_taylor_second_prefix_body_steps_coefficient. fs_h_ph_pth_taylor_second_prefix_body_steps_coefficient + S (ff_coefficient_ph_pth_taylor_second_prefix_body_steps) = S ((S (ff_i_ph_pth_taylor_second_prefix_body_steps)) * c)) /\ exists fs_q_ph_pth_taylor_second_prefix_body_steps_coefficient. b = fs_q_ph_pth_taylor_second_prefix_body_steps_coefficient * S ((S (ff_i_ph_pth_taylor_second_prefix_body_steps)) * c) + (ff_coefficient_ph_pth_taylor_second_prefix_body_steps))) /\ ((((exists fs_h_ph_pth_taylor_second_prefix_body_steps_before. fs_h_ph_pth_taylor_second_prefix_body_steps_before + S (ff_previous_ph_pth_taylor_second_prefix_body_steps) = S ((S (ff_i_ph_pth_taylor_second_prefix_body_steps)) * ff_v_ph_pth_taylor_second_prefix)) /\ exists fs_q_ph_pth_taylor_second_prefix_body_steps_before. ff_u_ph_pth_taylor_second_prefix = fs_q_ph_pth_taylor_second_prefix_body_steps_before * S ((S (ff_i_ph_pth_taylor_second_prefix_body_steps)) * ff_v_ph_pth_taylor_second_prefix) + (ff_previous_ph_pth_taylor_second_prefix_body_steps))) /\ ((((exists fs_h_ph_pth_taylor_second_prefix_body_steps_after. fs_h_ph_pth_taylor_second_prefix_body_steps_after + S (ff_current_ph_pth_taylor_second_prefix_body_steps) = S ((S (S ff_i_ph_pth_taylor_second_prefix_body_steps)) * ff_v_ph_pth_taylor_second_prefix)) /\ exists fs_q_ph_pth_taylor_second_prefix_body_steps_after. ff_u_ph_pth_taylor_second_prefix = fs_q_ph_pth_taylor_second_prefix_body_steps_after * S ((S (S ff_i_ph_pth_taylor_second_prefix_body_steps)) * ff_v_ph_pth_taylor_second_prefix) + (ff_current_ph_pth_taylor_second_prefix_body_steps))) /\ ff_current_ph_pth_taylor_second_prefix_body_steps = ff_previous_ph_pth_taylor_second_prefix_body_steps * (t + h) + ff_coefficient_ph_pth_taylor_second_prefix_body_steps)))))) /\ z = r * (t + h) + a))
  53. 0053specialize beta_horner_eval_successor_decompose b
  54. 0054specialize beta_horner_eval_successor_decompose c
  55. 0055specialize beta_horner_eval_successor_decompose (t + h)
  56. 0056specialize beta_horner_eval_successor_decompose l
  57. 0057specialize beta_horner_eval_successor_decompose z
  58. 0058apply beta_horner_eval_successor_decompose
  59. 0059exact hshifted
  60. 0060cases hsecond
  61. 0061cases hsecond_witness
  62. 0062cases hsecond_witness_witness
  63. 0063cases hsecond_witness_witness_right
  64. 0064have hcoefficient : x = x3
  65. 0065specialize beta_at_unique b
  66. 0066specialize beta_at_unique c
  67. 0067specialize beta_at_unique l
  68. 0068specialize beta_at_unique x
  69. 0069specialize beta_at_unique x3
  70. 0070apply beta_at_unique
  71. 0071exact hfirst_witness_witness_witness_left
  72. 0072exact hsecond_witness_witness_left
  73. 0073have hprefix : exists q. x4 = (x1 + h * x2) + (h * h) * q
  74. 0074specialize IH x1
  75. 0075specialize IH x2
  76. 0076specialize IH x4
  77. 0077apply IH
  78. 0078exact hfirst_witness_witness_witness_right_left
  79. 0079exact hsecond_witness_witness_right_left
  80. 0080cases hprefix
  81. 0081exists x5 * (t + h) + x2
  82. 0082rewrite hsecond_witness_witness_right_right
  83. 0083rewrite hfirst_witness_witness_witness_right_right_left
  84. 0084rewrite hfirst_witness_witness_witness_right_right_right
  85. 0085rewrite hprefix_witness
  86. 0086rewrite <- hcoefficient
  87. 0087specialize horner_taylor_successor_identity x1
  88. 0088specialize horner_taylor_successor_identity x2
  89. 0089specialize horner_taylor_successor_identity h
  90. 0090specialize horner_taylor_successor_identity x5
  91. 0091specialize horner_taylor_successor_identity t
  92. 0092specialize horner_taylor_successor_identity x
  93. 0093exact horner_taylor_successor_identity