TH000E

beta_horner_taylor_remainder_total

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

Every coefficient list, natural evaluation point, and natural shift has actual polynomial, derivative, shifted-value, and quadratic-remainder witnesses.

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 t h l. exists n d z q. (((exists ff_u_hd_pth_total_pair ff_v_hd_pth_total_pair ff_d_hd_pth_total_pair ff_e_hd_pth_total_pair. ((((((exists fs_h_ph_hd_pth_total_pair_body_value_start. fs_h_ph_hd_pth_total_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_value_start. ff_u_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_value_start * S ((S (0)) * ff_v_hd_pth_total_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_value_terminal. fs_h_ph_hd_pth_total_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_value_terminal. ff_u_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_value_terminal * S ((S (l)) * ff_v_hd_pth_total_pair) + (n))) /\ forall ff_i_ph_hd_pth_total_pair_body_value_steps. (exists ph_bound_hd_pth_total_pair_body_value_steps. ph_bound_hd_pth_total_pair_body_value_steps + S ff_i_ph_hd_pth_total_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_total_pair_body_value_steps ff_previous_ph_hd_pth_total_pair_body_value_steps ff_current_ph_hd_pth_total_pair_body_value_steps. ((((exists fs_h_ph_hd_pth_total_pair_body_value_steps_coefficient. fs_h_ph_hd_pth_total_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_total_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_total_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_total_pair_body_value_steps_coefficient. b = fs_q_ph_hd_pth_total_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_total_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_total_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_value_steps_before. fs_h_ph_hd_pth_total_pair_body_value_steps_before + S (ff_previous_ph_hd_pth_total_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_total_pair_body_value_steps)) * ff_v_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_value_steps_before. ff_u_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_value_steps_before * S ((S (ff_i_ph_hd_pth_total_pair_body_value_steps)) * ff_v_hd_pth_total_pair) + (ff_previous_ph_hd_pth_total_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_value_steps_after. fs_h_ph_hd_pth_total_pair_body_value_steps_after + S (ff_current_ph_hd_pth_total_pair_body_value_steps) = S ((S (S ff_i_ph_hd_pth_total_pair_body_value_steps)) * ff_v_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_value_steps_after. ff_u_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_total_pair_body_value_steps)) * ff_v_hd_pth_total_pair) + (ff_current_ph_hd_pth_total_pair_body_value_steps))) /\ ff_current_ph_hd_pth_total_pair_body_value_steps = ff_previous_ph_hd_pth_total_pair_body_value_steps * t + ff_coefficient_ph_hd_pth_total_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_total_pair_body_derivative_start. fs_h_ph_hd_pth_total_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_derivative_start. ff_d_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_derivative_start * S ((S (0)) * ff_e_hd_pth_total_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_derivative_terminal. fs_h_ph_hd_pth_total_pair_body_derivative_terminal + S (d) = S ((S (l)) * ff_e_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_derivative_terminal. ff_d_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_total_pair) + (d))) /\ forall ff_i_ph_hd_pth_total_pair_body_derivative_steps. (exists ph_bound_hd_pth_total_pair_body_derivative_steps. ph_bound_hd_pth_total_pair_body_derivative_steps + S ff_i_ph_hd_pth_total_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_total_pair_body_derivative_steps ff_previous_ph_hd_pth_total_pair_body_derivative_steps ff_current_ph_hd_pth_total_pair_body_derivative_steps. ((((exists fs_h_ph_hd_pth_total_pair_body_derivative_steps_coefficient. fs_h_ph_hd_pth_total_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_total_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_v_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_derivative_steps_coefficient. ff_u_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_v_hd_pth_total_pair) + (ff_coefficient_ph_hd_pth_total_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_derivative_steps_before. fs_h_ph_hd_pth_total_pair_body_derivative_steps_before + S (ff_previous_ph_hd_pth_total_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_e_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_derivative_steps_before. ff_d_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_e_hd_pth_total_pair) + (ff_previous_ph_hd_pth_total_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_derivative_steps_after. fs_h_ph_hd_pth_total_pair_body_derivative_steps_after + S (ff_current_ph_hd_pth_total_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_e_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_derivative_steps_after. ff_d_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_e_hd_pth_total_pair) + (ff_current_ph_hd_pth_total_pair_body_derivative_steps))) /\ ff_current_ph_hd_pth_total_pair_body_derivative_steps = ff_previous_ph_hd_pth_total_pair_body_derivative_steps * t + ff_coefficient_ph_hd_pth_total_pair_body_derivative_steps)))))))) /\ ((exists ff_u_ph_pth_total_shifted ff_v_ph_pth_total_shifted. ((((exists fs_h_ph_pth_total_shifted_body_start. fs_h_ph_pth_total_shifted_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_total_shifted)) /\ exists fs_q_ph_pth_total_shifted_body_start. ff_u_ph_pth_total_shifted = fs_q_ph_pth_total_shifted_body_start * S ((S (0)) * ff_v_ph_pth_total_shifted) + (0))) /\ ((((exists fs_h_ph_pth_total_shifted_body_terminal. fs_h_ph_pth_total_shifted_body_terminal + S (z) = S ((S (l)) * ff_v_ph_pth_total_shifted)) /\ exists fs_q_ph_pth_total_shifted_body_terminal. ff_u_ph_pth_total_shifted = fs_q_ph_pth_total_shifted_body_terminal * S ((S (l)) * ff_v_ph_pth_total_shifted) + (z))) /\ forall ff_i_ph_pth_total_shifted_body_steps. (exists ph_bound_pth_total_shifted_body_steps. ph_bound_pth_total_shifted_body_steps + S ff_i_ph_pth_total_shifted_body_steps = l) -> exists ff_coefficient_ph_pth_total_shifted_body_steps ff_previous_ph_pth_total_shifted_body_steps ff_current_ph_pth_total_shifted_body_steps. ((((exists fs_h_ph_pth_total_shifted_body_steps_coefficient. fs_h_ph_pth_total_shifted_body_steps_coefficient + S (ff_coefficient_ph_pth_total_shifted_body_steps) = S ((S (ff_i_ph_pth_total_shifted_body_steps)) * c)) /\ exists fs_q_ph_pth_total_shifted_body_steps_coefficient. b = fs_q_ph_pth_total_shifted_body_steps_coefficient * S ((S (ff_i_ph_pth_total_shifted_body_steps)) * c) + (ff_coefficient_ph_pth_total_shifted_body_steps))) /\ ((((exists fs_h_ph_pth_total_shifted_body_steps_before. fs_h_ph_pth_total_shifted_body_steps_before + S (ff_previous_ph_pth_total_shifted_body_steps) = S ((S (ff_i_ph_pth_total_shifted_body_steps)) * ff_v_ph_pth_total_shifted)) /\ exists fs_q_ph_pth_total_shifted_body_steps_before. ff_u_ph_pth_total_shifted = fs_q_ph_pth_total_shifted_body_steps_before * S ((S (ff_i_ph_pth_total_shifted_body_steps)) * ff_v_ph_pth_total_shifted) + (ff_previous_ph_pth_total_shifted_body_steps))) /\ ((((exists fs_h_ph_pth_total_shifted_body_steps_after. fs_h_ph_pth_total_shifted_body_steps_after + S (ff_current_ph_pth_total_shifted_body_steps) = S ((S (S ff_i_ph_pth_total_shifted_body_steps)) * ff_v_ph_pth_total_shifted)) /\ exists fs_q_ph_pth_total_shifted_body_steps_after. ff_u_ph_pth_total_shifted = fs_q_ph_pth_total_shifted_body_steps_after * S ((S (S ff_i_ph_pth_total_shifted_body_steps)) * ff_v_ph_pth_total_shifted) + (ff_current_ph_pth_total_shifted_body_steps))) /\ ff_current_ph_pth_total_shifted_body_steps = ff_previous_ph_pth_total_shifted_body_steps * (t + h) + ff_coefficient_ph_pth_total_shifted_body_steps)))))) /\ (z = (n + h * d) + (h * h) * q))))

Constructive proof overview

Generated structural guide

Every coefficient list, natural evaluation point, and natural shift has actual polynomial, derivative, shifted-value, and quadratic-remainder witnesses.

The unchanged tactic script uses 3 declared prerequisites and contains 42 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_horner_derivative_value_exists Alpha theorem; checked-use authorized beta_horner_eval_exists Alpha theorem; checked-use authorized TH0008 beta_horner_taylor_remainder_exists

Direct dependents

none

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

42 script commands · 13 reading checkpoints · 3 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 (1)
beta horner taylor remainder exists

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

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
02Establish hpairL6–11

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

  1. L6
    have hpair : ∃ n. ∃ d. HornerDerivative(b,c,t,l,n,d)Definitions: HornerDerivative
  2. L7
    specialize beta_horner_derivative_value_exists b
  3. L8
    specialize beta_horner_derivative_value_exists c
  4. L9
    specialize beta_horner_derivative_value_exists t
  5. L10
    specialize beta_horner_derivative_value_exists l
  6. L11
    exact beta_horner_derivative_value_exists
03Separate the logical casesL12–13

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

  1. L12
    cases hpair
  2. L13
    cases hpair_witness
04Establish hshiftedL14–19

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

  1. L14
    have hshifted : ∃ z. Horner(b,c,t + h,l,z)Definitions: Horner
  2. L15
    specialize beta_horner_eval_exists b
  3. L16
    specialize beta_horner_eval_exists c
  4. L17
    specialize beta_horner_eval_exists (t + h)
  5. L18
    specialize beta_horner_eval_exists l
  6. L19
    exact beta_horner_eval_exists
05Separate the logical casesL20–20

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

  1. L20
    cases hshifted
06Establish hremL21–30

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

  1. L21
    have hrem : exists q. x2 = (x + h * x1) + (h * h) * q
  2. L22
    specialize beta_horner_taylor_remainder_exists b
  3. L23
    specialize beta_horner_taylor_remainder_exists c
  4. L24
    specialize beta_horner_taylor_remainder_exists t
  5. L25
    specialize beta_horner_taylor_remainder_exists h
  6. L26
    specialize beta_horner_taylor_remainder_exists l
  7. L27
    specialize beta_horner_taylor_remainder_exists x
  8. L28
    specialize beta_horner_taylor_remainder_exists x1
  9. L29
    specialize beta_horner_taylor_remainder_exists x2
  10. L30
    apply beta_horner_taylor_remainder_exists
07Use earlier factsL31–32

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

  1. L31
    exact hpair_witness_witness
  2. L32
    exact hshifted_witness
08Separate the logical casesL33–33

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

  1. L33
    cases hrem
09Construct an explicit witnessL34–37

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

  1. L34
    exists x
  2. L35
    exists x1
  3. L36
    exists x2
  4. L37
    exists x3
10Separate the logical casesL38–38

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

  1. L38
    split
11Use earlier factsL39–39

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

  1. L39
    exact hpair_witness_witness
12Separate the logical casesL40–40

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

  1. L40
    split
13Use earlier factsL41–42

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

  1. L41
    exact hshifted_witness
  2. L42
    exact hrem_witness

Library-wide reading audit

Original exact command ledger · 42 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro h
  5. 0005intro l
  6. 0006have hpair : exists n d. (exists ff_u_hd_pth_total_pair ff_v_hd_pth_total_pair ff_d_hd_pth_total_pair ff_e_hd_pth_total_pair. ((((((exists fs_h_ph_hd_pth_total_pair_body_value_start. fs_h_ph_hd_pth_total_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_value_start. ff_u_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_value_start * S ((S (0)) * ff_v_hd_pth_total_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_value_terminal. fs_h_ph_hd_pth_total_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_value_terminal. ff_u_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_value_terminal * S ((S (l)) * ff_v_hd_pth_total_pair) + (n))) /\ forall ff_i_ph_hd_pth_total_pair_body_value_steps. (exists ph_bound_hd_pth_total_pair_body_value_steps. ph_bound_hd_pth_total_pair_body_value_steps + S ff_i_ph_hd_pth_total_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_pth_total_pair_body_value_steps ff_previous_ph_hd_pth_total_pair_body_value_steps ff_current_ph_hd_pth_total_pair_body_value_steps. ((((exists fs_h_ph_hd_pth_total_pair_body_value_steps_coefficient. fs_h_ph_hd_pth_total_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pth_total_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_total_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pth_total_pair_body_value_steps_coefficient. b = fs_q_ph_hd_pth_total_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pth_total_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_pth_total_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_value_steps_before. fs_h_ph_hd_pth_total_pair_body_value_steps_before + S (ff_previous_ph_hd_pth_total_pair_body_value_steps) = S ((S (ff_i_ph_hd_pth_total_pair_body_value_steps)) * ff_v_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_value_steps_before. ff_u_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_value_steps_before * S ((S (ff_i_ph_hd_pth_total_pair_body_value_steps)) * ff_v_hd_pth_total_pair) + (ff_previous_ph_hd_pth_total_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_value_steps_after. fs_h_ph_hd_pth_total_pair_body_value_steps_after + S (ff_current_ph_hd_pth_total_pair_body_value_steps) = S ((S (S ff_i_ph_hd_pth_total_pair_body_value_steps)) * ff_v_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_value_steps_after. ff_u_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_pth_total_pair_body_value_steps)) * ff_v_hd_pth_total_pair) + (ff_current_ph_hd_pth_total_pair_body_value_steps))) /\ ff_current_ph_hd_pth_total_pair_body_value_steps = ff_previous_ph_hd_pth_total_pair_body_value_steps * t + ff_coefficient_ph_hd_pth_total_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pth_total_pair_body_derivative_start. fs_h_ph_hd_pth_total_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_derivative_start. ff_d_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_derivative_start * S ((S (0)) * ff_e_hd_pth_total_pair) + (0))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_derivative_terminal. fs_h_ph_hd_pth_total_pair_body_derivative_terminal + S (d) = S ((S (l)) * ff_e_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_derivative_terminal. ff_d_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_pth_total_pair) + (d))) /\ forall ff_i_ph_hd_pth_total_pair_body_derivative_steps. (exists ph_bound_hd_pth_total_pair_body_derivative_steps. ph_bound_hd_pth_total_pair_body_derivative_steps + S ff_i_ph_hd_pth_total_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pth_total_pair_body_derivative_steps ff_previous_ph_hd_pth_total_pair_body_derivative_steps ff_current_ph_hd_pth_total_pair_body_derivative_steps. ((((exists fs_h_ph_hd_pth_total_pair_body_derivative_steps_coefficient. fs_h_ph_hd_pth_total_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pth_total_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_v_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_derivative_steps_coefficient. ff_u_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_v_hd_pth_total_pair) + (ff_coefficient_ph_hd_pth_total_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_derivative_steps_before. fs_h_ph_hd_pth_total_pair_body_derivative_steps_before + S (ff_previous_ph_hd_pth_total_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_e_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_derivative_steps_before. ff_d_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_e_hd_pth_total_pair) + (ff_previous_ph_hd_pth_total_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pth_total_pair_body_derivative_steps_after. fs_h_ph_hd_pth_total_pair_body_derivative_steps_after + S (ff_current_ph_hd_pth_total_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_e_hd_pth_total_pair)) /\ exists fs_q_ph_hd_pth_total_pair_body_derivative_steps_after. ff_d_hd_pth_total_pair = fs_q_ph_hd_pth_total_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pth_total_pair_body_derivative_steps)) * ff_e_hd_pth_total_pair) + (ff_current_ph_hd_pth_total_pair_body_derivative_steps))) /\ ff_current_ph_hd_pth_total_pair_body_derivative_steps = ff_previous_ph_hd_pth_total_pair_body_derivative_steps * t + ff_coefficient_ph_hd_pth_total_pair_body_derivative_steps))))))))
  7. 0007specialize beta_horner_derivative_value_exists b
  8. 0008specialize beta_horner_derivative_value_exists c
  9. 0009specialize beta_horner_derivative_value_exists t
  10. 0010specialize beta_horner_derivative_value_exists l
  11. 0011exact beta_horner_derivative_value_exists
  12. 0012cases hpair
  13. 0013cases hpair_witness
  14. 0014have hshifted : exists z. (exists ff_u_ph_pth_total_shifted ff_v_ph_pth_total_shifted. ((((exists fs_h_ph_pth_total_shifted_body_start. fs_h_ph_pth_total_shifted_body_start + S (0) = S ((S (0)) * ff_v_ph_pth_total_shifted)) /\ exists fs_q_ph_pth_total_shifted_body_start. ff_u_ph_pth_total_shifted = fs_q_ph_pth_total_shifted_body_start * S ((S (0)) * ff_v_ph_pth_total_shifted) + (0))) /\ ((((exists fs_h_ph_pth_total_shifted_body_terminal. fs_h_ph_pth_total_shifted_body_terminal + S (z) = S ((S (l)) * ff_v_ph_pth_total_shifted)) /\ exists fs_q_ph_pth_total_shifted_body_terminal. ff_u_ph_pth_total_shifted = fs_q_ph_pth_total_shifted_body_terminal * S ((S (l)) * ff_v_ph_pth_total_shifted) + (z))) /\ forall ff_i_ph_pth_total_shifted_body_steps. (exists ph_bound_pth_total_shifted_body_steps. ph_bound_pth_total_shifted_body_steps + S ff_i_ph_pth_total_shifted_body_steps = l) -> exists ff_coefficient_ph_pth_total_shifted_body_steps ff_previous_ph_pth_total_shifted_body_steps ff_current_ph_pth_total_shifted_body_steps. ((((exists fs_h_ph_pth_total_shifted_body_steps_coefficient. fs_h_ph_pth_total_shifted_body_steps_coefficient + S (ff_coefficient_ph_pth_total_shifted_body_steps) = S ((S (ff_i_ph_pth_total_shifted_body_steps)) * c)) /\ exists fs_q_ph_pth_total_shifted_body_steps_coefficient. b = fs_q_ph_pth_total_shifted_body_steps_coefficient * S ((S (ff_i_ph_pth_total_shifted_body_steps)) * c) + (ff_coefficient_ph_pth_total_shifted_body_steps))) /\ ((((exists fs_h_ph_pth_total_shifted_body_steps_before. fs_h_ph_pth_total_shifted_body_steps_before + S (ff_previous_ph_pth_total_shifted_body_steps) = S ((S (ff_i_ph_pth_total_shifted_body_steps)) * ff_v_ph_pth_total_shifted)) /\ exists fs_q_ph_pth_total_shifted_body_steps_before. ff_u_ph_pth_total_shifted = fs_q_ph_pth_total_shifted_body_steps_before * S ((S (ff_i_ph_pth_total_shifted_body_steps)) * ff_v_ph_pth_total_shifted) + (ff_previous_ph_pth_total_shifted_body_steps))) /\ ((((exists fs_h_ph_pth_total_shifted_body_steps_after. fs_h_ph_pth_total_shifted_body_steps_after + S (ff_current_ph_pth_total_shifted_body_steps) = S ((S (S ff_i_ph_pth_total_shifted_body_steps)) * ff_v_ph_pth_total_shifted)) /\ exists fs_q_ph_pth_total_shifted_body_steps_after. ff_u_ph_pth_total_shifted = fs_q_ph_pth_total_shifted_body_steps_after * S ((S (S ff_i_ph_pth_total_shifted_body_steps)) * ff_v_ph_pth_total_shifted) + (ff_current_ph_pth_total_shifted_body_steps))) /\ ff_current_ph_pth_total_shifted_body_steps = ff_previous_ph_pth_total_shifted_body_steps * (t + h) + ff_coefficient_ph_pth_total_shifted_body_steps))))))
  15. 0015specialize beta_horner_eval_exists b
  16. 0016specialize beta_horner_eval_exists c
  17. 0017specialize beta_horner_eval_exists (t + h)
  18. 0018specialize beta_horner_eval_exists l
  19. 0019exact beta_horner_eval_exists
  20. 0020cases hshifted
  21. 0021have hrem : exists q. x2 = (x + h * x1) + (h * h) * q
  22. 0022specialize beta_horner_taylor_remainder_exists b
  23. 0023specialize beta_horner_taylor_remainder_exists c
  24. 0024specialize beta_horner_taylor_remainder_exists t
  25. 0025specialize beta_horner_taylor_remainder_exists h
  26. 0026specialize beta_horner_taylor_remainder_exists l
  27. 0027specialize beta_horner_taylor_remainder_exists x
  28. 0028specialize beta_horner_taylor_remainder_exists x1
  29. 0029specialize beta_horner_taylor_remainder_exists x2
  30. 0030apply beta_horner_taylor_remainder_exists
  31. 0031exact hpair_witness_witness
  32. 0032exact hshifted_witness
  33. 0033cases hrem
  34. 0034exists x
  35. 0035exists x1
  36. 0036exists x2
  37. 0037exists x3
  38. 0038split
  39. 0039exact hpair_witness_witness
  40. 0040split
  41. 0041exact hshifted_witness
  42. 0042exact hrem_witness

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