HD0008

beta_horner_derivative_successor_decompose

A successor polynomial obeys both exact Horner recurrences: f_new=f_old*t+a and f'_new=f'_old*t+f_old.

Alpha v34 checked-use · first admitted v24 · 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 arbitrary natural polynomial values and unique formal derivatives. G095 is now closed in the separate Alpha-v27 hensel-lifting branch for integer polynomials, unrestricted input roots, unique canonical lifts, and every positive prime power. Full G095 proof · Alpha v27

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ t. ∀ l. ∀ n. ∀ z. HornerDerivative(b,c,t,S l,n,z) → ∃ x. ∃ y. ∃ m. Beta(b,c,l,x) ∧ (HornerDerivative(b,c,t,l,y,m) ∧ (n = y · t + x ∧ z = m · t + y))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Beta(b,c,i,x) · 1HornerDerivative(b,c,t,l,n,z) · 2

Actual proof prerequisites

le_refl · checked external prerequisitele_succ · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall b c t l n z. (exists ff_u_hd_successor ff_v_hd_successor ff_d_hd_successor ff_e_hd_successor. ((((((exists fs_h_ph_hd_successor_body_value_start. fs_h_ph_hd_successor_body_value_start + S (0) = S ((S (0)) * ff_v_hd_successor)) /\ exists fs_q_ph_hd_successor_body_value_start. ff_u_hd_successor = fs_q_ph_hd_successor_body_value_start * S ((S (0)) * ff_v_hd_successor) + (0))) /\ ((((exists fs_h_ph_hd_successor_body_value_terminal. fs_h_ph_hd_successor_body_value_terminal + S (n) = S ((S (S l)) * ff_v_hd_successor)) /\ exists fs_q_ph_hd_successor_body_value_terminal. ff_u_hd_successor = fs_q_ph_hd_successor_body_value_terminal * S ((S (S l)) * ff_v_hd_successor) + (n))) /\ forall ff_i_ph_hd_successor_body_value_steps. (exists ph_bound_hd_successor_body_value_steps. ph_bound_hd_successor_body_value_steps + S ff_i_ph_hd_successor_body_value_steps = S l) -> exists ff_coefficient_ph_hd_successor_body_value_steps ff_previous_ph_hd_successor_body_value_steps ff_current_ph_hd_successor_body_value_steps. ((((exists fs_h_ph_hd_successor_body_value_steps_coefficient. fs_h_ph_hd_successor_body_value_steps_coefficient + S (ff_coefficient_ph_hd_successor_body_value_steps) = S ((S (ff_i_ph_hd_successor_body_value_steps)) * c)) /\ exists fs_q_ph_hd_successor_body_value_steps_coefficient. b = fs_q_ph_hd_successor_body_value_steps_coefficient * S ((S (ff_i_ph_hd_successor_body_value_steps)) * c) + (ff_coefficient_ph_hd_successor_body_value_steps))) /\ ((((exists fs_h_ph_hd_successor_body_value_steps_before. fs_h_ph_hd_successor_body_value_steps_before + S (ff_previous_ph_hd_successor_body_value_steps) = S ((S (ff_i_ph_hd_successor_body_value_steps)) * ff_v_hd_successor)) /\ exists fs_q_ph_hd_successor_body_value_steps_before. ff_u_hd_successor = fs_q_ph_hd_successor_body_value_steps_before * S ((S (ff_i_ph_hd_successor_body_value_steps)) * ff_v_hd_successor) + (ff_previous_ph_hd_successor_body_value_steps))) /\ ((((exists fs_h_ph_hd_successor_body_value_steps_after. fs_h_ph_hd_successor_body_value_steps_after + S (ff_current_ph_hd_successor_body_value_steps) = S ((S (S ff_i_ph_hd_successor_body_value_steps)) * ff_v_hd_successor)) /\ exists fs_q_ph_hd_successor_body_value_steps_after. ff_u_hd_successor = fs_q_ph_hd_successor_body_value_steps_after * S ((S (S ff_i_ph_hd_successor_body_value_steps)) * ff_v_hd_successor) + (ff_current_ph_hd_successor_body_value_steps))) /\ ff_current_ph_hd_successor_body_value_steps = ff_previous_ph_hd_successor_body_value_steps * t + ff_coefficient_ph_hd_successor_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_successor_body_derivative_start. fs_h_ph_hd_successor_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_successor)) /\ exists fs_q_ph_hd_successor_body_derivative_start. ff_d_hd_successor = fs_q_ph_hd_successor_body_derivative_start * S ((S (0)) * ff_e_hd_successor) + (0))) /\ ((((exists fs_h_ph_hd_successor_body_derivative_terminal. fs_h_ph_hd_successor_body_derivative_terminal + S (z) = S ((S (S l)) * ff_e_hd_successor)) /\ exists fs_q_ph_hd_successor_body_derivative_terminal. ff_d_hd_successor = fs_q_ph_hd_successor_body_derivative_terminal * S ((S (S l)) * ff_e_hd_successor) + (z))) /\ forall ff_i_ph_hd_successor_body_derivative_steps. (exists ph_bound_hd_successor_body_derivative_steps. ph_bound_hd_successor_body_derivative_steps + S ff_i_ph_hd_successor_body_derivative_steps = S l) -> exists ff_coefficient_ph_hd_successor_body_derivative_steps ff_previous_ph_hd_successor_body_derivative_steps ff_current_ph_hd_successor_body_derivative_steps. ((((exists fs_h_ph_hd_successor_body_derivative_steps_coefficient. fs_h_ph_hd_successor_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_successor_body_derivative_steps) = S ((S (ff_i_ph_hd_successor_body_derivative_steps)) * ff_v_hd_successor)) /\ exists fs_q_ph_hd_successor_body_derivative_steps_coefficient. ff_u_hd_successor = fs_q_ph_hd_successor_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_successor_body_derivative_steps)) * ff_v_hd_successor) + (ff_coefficient_ph_hd_successor_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_successor_body_derivative_steps_before. fs_h_ph_hd_successor_body_derivative_steps_before + S (ff_previous_ph_hd_successor_body_derivative_steps) = S ((S (ff_i_ph_hd_successor_body_derivative_steps)) * ff_e_hd_successor)) /\ exists fs_q_ph_hd_successor_body_derivative_steps_before. ff_d_hd_successor = fs_q_ph_hd_successor_body_derivative_steps_before * S ((S (ff_i_ph_hd_successor_body_derivative_steps)) * ff_e_hd_successor) + (ff_previous_ph_hd_successor_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_successor_body_derivative_steps_after. fs_h_ph_hd_successor_body_derivative_steps_after + S (ff_current_ph_hd_successor_body_derivative_steps) = S ((S (S ff_i_ph_hd_successor_body_derivative_steps)) * ff_e_hd_successor)) /\ exists fs_q_ph_hd_successor_body_derivative_steps_after. ff_d_hd_successor = fs_q_ph_hd_successor_body_derivative_steps_after * S ((S (S ff_i_ph_hd_successor_body_derivative_steps)) * ff_e_hd_successor) + (ff_current_ph_hd_successor_body_derivative_steps))) /\ ff_current_ph_hd_successor_body_derivative_steps = ff_previous_ph_hd_successor_body_derivative_steps * t + ff_coefficient_ph_hd_successor_body_derivative_steps)))))))) -> exists a r q. ((((exists fs_h_hd_successor_coefficient. fs_h_hd_successor_coefficient + S (a) = S ((S (l)) * c)) /\ exists fs_q_hd_successor_coefficient. b = fs_q_hd_successor_coefficient * S ((S (l)) * c) + (a))) /\ ((exists ff_u_hd_successor_prefix ff_v_hd_successor_prefix ff_d_hd_successor_prefix ff_e_hd_successor_prefix. ((((((exists fs_h_ph_hd_successor_prefix_body_value_start. fs_h_ph_hd_successor_prefix_body_value_start + S (0) = S ((S (0)) * ff_v_hd_successor_prefix)) /\ exists fs_q_ph_hd_successor_prefix_body_value_start. ff_u_hd_successor_prefix = fs_q_ph_hd_successor_prefix_body_value_start * S ((S (0)) * ff_v_hd_successor_prefix) + (0))) /\ ((((exists fs_h_ph_hd_successor_prefix_body_value_terminal. fs_h_ph_hd_successor_prefix_body_value_terminal + S (r) = S ((S (l)) * ff_v_hd_successor_prefix)) /\ exists fs_q_ph_hd_successor_prefix_body_value_terminal. ff_u_hd_successor_prefix = fs_q_ph_hd_successor_prefix_body_value_terminal * S ((S (l)) * ff_v_hd_successor_prefix) + (r))) /\ forall ff_i_ph_hd_successor_prefix_body_value_steps. (exists ph_bound_hd_successor_prefix_body_value_steps. ph_bound_hd_successor_prefix_body_value_steps + S ff_i_ph_hd_successor_prefix_body_value_steps = l) -> exists ff_coefficient_ph_hd_successor_prefix_body_value_steps ff_previous_ph_hd_successor_prefix_body_value_steps ff_current_ph_hd_successor_prefix_body_value_steps. ((((exists fs_h_ph_hd_successor_prefix_body_value_steps_coefficient. fs_h_ph_hd_successor_prefix_body_value_steps_coefficient + S (ff_coefficient_ph_hd_successor_prefix_body_value_steps) = S ((S (ff_i_ph_hd_successor_prefix_body_value_steps)) * c)) /\ exists fs_q_ph_hd_successor_prefix_body_value_steps_coefficient. b = fs_q_ph_hd_successor_prefix_body_value_steps_coefficient * S ((S (ff_i_ph_hd_successor_prefix_body_value_steps)) * c) + (ff_coefficient_ph_hd_successor_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_successor_prefix_body_value_steps_before. fs_h_ph_hd_successor_prefix_body_value_steps_before + S (ff_previous_ph_hd_successor_prefix_body_value_steps) = S ((S (ff_i_ph_hd_successor_prefix_body_value_steps)) * ff_v_hd_successor_prefix)) /\ exists fs_q_ph_hd_successor_prefix_body_value_steps_before. ff_u_hd_successor_prefix = fs_q_ph_hd_successor_prefix_body_value_steps_before * S ((S (ff_i_ph_hd_successor_prefix_body_value_steps)) * ff_v_hd_successor_prefix) + (ff_previous_ph_hd_successor_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_successor_prefix_body_value_steps_after. fs_h_ph_hd_successor_prefix_body_value_steps_after + S (ff_current_ph_hd_successor_prefix_body_value_steps) = S ((S (S ff_i_ph_hd_successor_prefix_body_value_steps)) * ff_v_hd_successor_prefix)) /\ exists fs_q_ph_hd_successor_prefix_body_value_steps_after. ff_u_hd_successor_prefix = fs_q_ph_hd_successor_prefix_body_value_steps_after * S ((S (S ff_i_ph_hd_successor_prefix_body_value_steps)) * ff_v_hd_successor_prefix) + (ff_current_ph_hd_successor_prefix_body_value_steps))) /\ ff_current_ph_hd_successor_prefix_body_value_steps = ff_previous_ph_hd_successor_prefix_body_value_steps * t + ff_coefficient_ph_hd_successor_prefix_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_successor_prefix_body_derivative_start. fs_h_ph_hd_successor_prefix_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_successor_prefix)) /\ exists fs_q_ph_hd_successor_prefix_body_derivative_start. ff_d_hd_successor_prefix = fs_q_ph_hd_successor_prefix_body_derivative_start * S ((S (0)) * ff_e_hd_successor_prefix) + (0))) /\ ((((exists fs_h_ph_hd_successor_prefix_body_derivative_terminal. fs_h_ph_hd_successor_prefix_body_derivative_terminal + S (q) = S ((S (l)) * ff_e_hd_successor_prefix)) /\ exists fs_q_ph_hd_successor_prefix_body_derivative_terminal. ff_d_hd_successor_prefix = fs_q_ph_hd_successor_prefix_body_derivative_terminal * S ((S (l)) * ff_e_hd_successor_prefix) + (q))) /\ forall ff_i_ph_hd_successor_prefix_body_derivative_steps. (exists ph_bound_hd_successor_prefix_body_derivative_steps. ph_bound_hd_successor_prefix_body_derivative_steps + S ff_i_ph_hd_successor_prefix_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_successor_prefix_body_derivative_steps ff_previous_ph_hd_successor_prefix_body_derivative_steps ff_current_ph_hd_successor_prefix_body_derivative_steps. ((((exists fs_h_ph_hd_successor_prefix_body_derivative_steps_coefficient. fs_h_ph_hd_successor_prefix_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_successor_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_successor_prefix_body_derivative_steps)) * ff_v_hd_successor_prefix)) /\ exists fs_q_ph_hd_successor_prefix_body_derivative_steps_coefficient. ff_u_hd_successor_prefix = fs_q_ph_hd_successor_prefix_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_successor_prefix_body_derivative_steps)) * ff_v_hd_successor_prefix) + (ff_coefficient_ph_hd_successor_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_successor_prefix_body_derivative_steps_before. fs_h_ph_hd_successor_prefix_body_derivative_steps_before + S (ff_previous_ph_hd_successor_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_successor_prefix_body_derivative_steps)) * ff_e_hd_successor_prefix)) /\ exists fs_q_ph_hd_successor_prefix_body_derivative_steps_before. ff_d_hd_successor_prefix = fs_q_ph_hd_successor_prefix_body_derivative_steps_before * S ((S (ff_i_ph_hd_successor_prefix_body_derivative_steps)) * ff_e_hd_successor_prefix) + (ff_previous_ph_hd_successor_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_successor_prefix_body_derivative_steps_after. fs_h_ph_hd_successor_prefix_body_derivative_steps_after + S (ff_current_ph_hd_successor_prefix_body_derivative_steps) = S ((S (S ff_i_ph_hd_successor_prefix_body_derivative_steps)) * ff_e_hd_successor_prefix)) /\ exists fs_q_ph_hd_successor_prefix_body_derivative_steps_after. ff_d_hd_successor_prefix = fs_q_ph_hd_successor_prefix_body_derivative_steps_after * S ((S (S ff_i_ph_hd_successor_prefix_body_derivative_steps)) * ff_e_hd_successor_prefix) + (ff_current_ph_hd_successor_prefix_body_derivative_steps))) /\ ff_current_ph_hd_successor_prefix_body_derivative_steps = ff_previous_ph_hd_successor_prefix_body_derivative_steps * t + ff_coefficient_ph_hd_successor_prefix_body_derivative_steps)))))))) /\ ((n = r * t + a) /\ z = q * t + r)))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

106 script commands · 31 reading checkpoints · 5 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.

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

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 l
  5. L5
    intro n
  6. L6
    intro z
  7. L7
    intro hpair
02Separate the logical casesL8–16

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

  1. L8
    cases hpair
  2. L9
    cases hpair_witness
  3. L10
    cases hpair_witness_witness
  4. L11
    cases hpair_witness_witness_witness
  5. L12
    cases hpair_witness_witness_witness_witness
  6. L13
    cases hpair_witness_witness_witness_witness_left
  7. L14
    cases hpair_witness_witness_witness_witness_left_right
  8. L15
    cases hpair_witness_witness_witness_witness_right
  9. L16
    cases hpair_witness_witness_witness_witness_right_right
03Establish hvalue_stepL17–21

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

  1. L17
    have hvalue_step : ∃ a. ∃ r. ∃ s. Beta(b,c,l,a) ∧ (Beta(x,x1,l,r) ∧ (Beta(x,x1,S l,s) ∧ s = r · t + a))Definitions: BetaOriginal native command in the exact edition
  2. L18
    specialize hpair_witness_witness_witness_witness_left_right_right l
  3. L19
    apply hpair_witness_witness_witness_witness_left_right_right
  4. L20
    specialize le_refl (S l)
  5. L21
    exact le_refl
04Separate the logical casesL22–27

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

  1. L22
    cases hvalue_step
  2. L23
    cases hvalue_step_witness
  3. L24
    cases hvalue_step_witness_witness
  4. L25
    cases hvalue_step_witness_witness_witness
  5. L26
    cases hvalue_step_witness_witness_witness_right
  6. L27
    cases hvalue_step_witness_witness_witness_right_right
05Establish hderivative_stepL28–32

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

  1. L28
    have hderivative_step : ∃ a. ∃ q. ∃ s. Beta(x,x1,l,a) ∧ (Beta(x2,x3,l,q) ∧ (Beta(x2,x3,S l,s) ∧ s = q · t + a))Definitions: BetaOriginal native command in the exact edition
  2. L29
    specialize hpair_witness_witness_witness_witness_right_right_right l
  3. L30
    apply hpair_witness_witness_witness_witness_right_right_right
  4. L31
    specialize le_refl (S l)
  5. L32
    exact le_refl
06Separate the logical casesL33–38

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

  1. L33
    cases hderivative_step
  2. L34
    cases hderivative_step_witness
  3. L35
    cases hderivative_step_witness_witness
  4. L36
    cases hderivative_step_witness_witness_witness
  5. L37
    cases hderivative_step_witness_witness_witness_right
  6. L38
    cases hderivative_step_witness_witness_witness_right_right
07Establish hcoefficientL39–47

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

  1. L39
    have hcoefficient : x7 = x5
  2. L40
    specialize beta_at_unique x
  3. L41
    specialize beta_at_unique x1
  4. L42
    specialize beta_at_unique l
  5. L43
    specialize beta_at_unique x7
  6. L44
    specialize beta_at_unique x5
  7. L45
    apply beta_at_unique
  8. L46
    exact hderivative_step_witness_witness_witness_left
  9. L47
    exact hvalue_step_witness_witness_witness_right_left
08Establish hfinal_valueL48–56

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

  1. L48
    have hfinal_value : n = x6
  2. L49
    specialize beta_at_unique x
  3. L50
    specialize beta_at_unique x1
  4. L51
    specialize beta_at_unique (S l)
  5. L52
    specialize beta_at_unique n
  6. L53
    specialize beta_at_unique x6
  7. L54
    apply beta_at_unique
  8. L55
    exact hpair_witness_witness_witness_witness_left_right_left
  9. L56
    exact hvalue_step_witness_witness_witness_right_right_left
09Establish hfinal_derivativeL57–65

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

  1. L57
    have hfinal_derivative : z = x9
  2. L58
    specialize beta_at_unique x2
  3. L59
    specialize beta_at_unique x3
  4. L60
    specialize beta_at_unique (S l)
  5. L61
    specialize beta_at_unique z
  6. L62
    specialize beta_at_unique x9
  7. L63
    apply beta_at_unique
  8. L64
    exact hpair_witness_witness_witness_witness_right_right_left
  9. L65
    exact hderivative_step_witness_witness_witness_right_right_left
10Construct an explicit witnessL66–68

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

  1. L66
    exists x4
  2. L67
    exists x5
  3. L68
    exists x8
11Separate the logical casesL69–69

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

  1. L69
    split
12Use earlier factsL70–70

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

  1. L70
    exact hvalue_step_witness_witness_witness_left
13Separate the logical casesL71–71

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

  1. L71
    split
14Construct an explicit witnessL72–75

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

  1. L72
    exists x
  2. L73
    exists x1
  3. L74
    exists x2
  4. L75
    exists x3
15Separate the logical casesL76–77

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

  1. L76
    split
  2. L77
    split
16Use earlier factsL78–78

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

  1. L78
    exact hpair_witness_witness_witness_witness_left_left
17Separate the logical casesL79–79

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

  1. L79
    split
18Use earlier factsL80–80

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

  1. L80
    exact hvalue_step_witness_witness_witness_right_left
19Fix variables and assumptionsL81–82

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

  1. L81
    intro i
  2. L82
    intro hi
20Use earlier factsL83–88

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

  1. L83
    specialize hpair_witness_witness_witness_witness_left_right_right i
  2. L84
    apply hpair_witness_witness_witness_witness_left_right_right
  3. L85
    specialize le_succ (S i)
  4. L86
    specialize le_succ l
  5. L87
    apply le_succ
  6. L88
    exact hi
21Separate the logical casesL89–89

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

  1. L89
    split
22Use earlier factsL90–90

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

  1. L90
    exact hpair_witness_witness_witness_witness_right_left
23Separate the logical casesL91–91

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

  1. L91
    split
24Use earlier factsL92–92

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

  1. L92
    exact hderivative_step_witness_witness_witness_right_left
25Fix variables and assumptionsL93–94

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

  1. L93
    intro i
  2. L94
    intro hi
26Use earlier factsL95–100

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

  1. L95
    specialize hpair_witness_witness_witness_witness_right_right_right i
  2. L96
    apply hpair_witness_witness_witness_witness_right_right_right
  3. L97
    specialize le_succ (S i)
  4. L98
    specialize le_succ l
  5. L99
    apply le_succ
  6. L100
    exact hi
27Separate the logical casesL101–101

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

  1. L101
    split
28Calculate and transport equalitiesL102–102

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

  1. L102
    rewrite hfinal_value
29Use earlier factsL103–103

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

  1. L103
    exact hvalue_step_witness_witness_witness_right_right_right
30Calculate and transport equalitiesL104–105

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

  1. L104
    rewrite hfinal_derivative
  2. L105
    rewrite <- hcoefficient
31Use earlier factsL106–106

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

  1. L106
    exact hderivative_step_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 106 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro l
  5. 0005intro n
  6. 0006intro z
  7. 0007intro hpair
  8. 0008cases hpair
  9. 0009cases hpair_witness
  10. 0010cases hpair_witness_witness
  11. 0011cases hpair_witness_witness_witness
  12. 0012cases hpair_witness_witness_witness_witness
  13. 0013cases hpair_witness_witness_witness_witness_left
  14. 0014cases hpair_witness_witness_witness_witness_left_right
  15. 0015cases hpair_witness_witness_witness_witness_right
  16. 0016cases hpair_witness_witness_witness_witness_right_right
  17. 0017have hvalue_step : exists a r s. ((((exists fs_h_hd_step_coefficient. fs_h_hd_step_coefficient + S (a) = S ((S (l)) * c)) /\ exists fs_q_hd_step_coefficient. b = fs_q_hd_step_coefficient * S ((S (l)) * c) + (a))) /\ ((((exists fs_h_hd_step_value_previous. fs_h_hd_step_value_previous + S (r) = S ((S (l)) * x1)) /\ exists fs_q_hd_step_value_previous. x = fs_q_hd_step_value_previous * S ((S (l)) * x1) + (r))) /\ ((((exists fs_h_hd_step_value_next. fs_h_hd_step_value_next + S (s) = S ((S (S l)) * x1)) /\ exists fs_q_hd_step_value_next. x = fs_q_hd_step_value_next * S ((S (S l)) * x1) + (s))) /\ s = r * t + a)))
  18. 0018specialize hpair_witness_witness_witness_witness_left_right_right l
  19. 0019apply hpair_witness_witness_witness_witness_left_right_right
  20. 0020specialize le_refl (S l)
  21. 0021exact le_refl
  22. 0022cases hvalue_step
  23. 0023cases hvalue_step_witness
  24. 0024cases hvalue_step_witness_witness
  25. 0025cases hvalue_step_witness_witness_witness
  26. 0026cases hvalue_step_witness_witness_witness_right
  27. 0027cases hvalue_step_witness_witness_witness_right_right
  28. 0028have hderivative_step : exists a q s. ((((exists fs_h_hd_step_derivative_coefficient. fs_h_hd_step_derivative_coefficient + S (a) = S ((S (l)) * x1)) /\ exists fs_q_hd_step_derivative_coefficient. x = fs_q_hd_step_derivative_coefficient * S ((S (l)) * x1) + (a))) /\ ((((exists fs_h_hd_step_derivative_previous. fs_h_hd_step_derivative_previous + S (q) = S ((S (l)) * x3)) /\ exists fs_q_hd_step_derivative_previous. x2 = fs_q_hd_step_derivative_previous * S ((S (l)) * x3) + (q))) /\ ((((exists fs_h_hd_step_derivative_next. fs_h_hd_step_derivative_next + S (s) = S ((S (S l)) * x3)) /\ exists fs_q_hd_step_derivative_next. x2 = fs_q_hd_step_derivative_next * S ((S (S l)) * x3) + (s))) /\ s = q * t + a)))
  29. 0029specialize hpair_witness_witness_witness_witness_right_right_right l
  30. 0030apply hpair_witness_witness_witness_witness_right_right_right
  31. 0031specialize le_refl (S l)
  32. 0032exact le_refl
  33. 0033cases hderivative_step
  34. 0034cases hderivative_step_witness
  35. 0035cases hderivative_step_witness_witness
  36. 0036cases hderivative_step_witness_witness_witness
  37. 0037cases hderivative_step_witness_witness_witness_right
  38. 0038cases hderivative_step_witness_witness_witness_right_right
  39. 0039have hcoefficient : x7 = x5
  40. 0040specialize beta_at_unique x
  41. 0041specialize beta_at_unique x1
  42. 0042specialize beta_at_unique l
  43. 0043specialize beta_at_unique x7
  44. 0044specialize beta_at_unique x5
  45. 0045apply beta_at_unique
  46. 0046exact hderivative_step_witness_witness_witness_left
  47. 0047exact hvalue_step_witness_witness_witness_right_left
  48. 0048have hfinal_value : n = x6
  49. 0049specialize beta_at_unique x
  50. 0050specialize beta_at_unique x1
  51. 0051specialize beta_at_unique (S l)
  52. 0052specialize beta_at_unique n
  53. 0053specialize beta_at_unique x6
  54. 0054apply beta_at_unique
  55. 0055exact hpair_witness_witness_witness_witness_left_right_left
  56. 0056exact hvalue_step_witness_witness_witness_right_right_left
  57. 0057have hfinal_derivative : z = x9
  58. 0058specialize beta_at_unique x2
  59. 0059specialize beta_at_unique x3
  60. 0060specialize beta_at_unique (S l)
  61. 0061specialize beta_at_unique z
  62. 0062specialize beta_at_unique x9
  63. 0063apply beta_at_unique
  64. 0064exact hpair_witness_witness_witness_witness_right_right_left
  65. 0065exact hderivative_step_witness_witness_witness_right_right_left
  66. 0066exists x4
  67. 0067exists x5
  68. 0068exists x8
  69. 0069split
  70. 0070exact hvalue_step_witness_witness_witness_left
  71. 0071split
  72. 0072exists x
  73. 0073exists x1
  74. 0074exists x2
  75. 0075exists x3
  76. 0076split
  77. 0077split
  78. 0078exact hpair_witness_witness_witness_witness_left_left
  79. 0079split
  80. 0080exact hvalue_step_witness_witness_witness_right_left
  81. 0081intro i
  82. 0082intro hi
  83. 0083specialize hpair_witness_witness_witness_witness_left_right_right i
  84. 0084apply hpair_witness_witness_witness_witness_left_right_right
  85. 0085specialize le_succ (S i)
  86. 0086specialize le_succ l
  87. 0087apply le_succ
  88. 0088exact hi
  89. 0089split
  90. 0090exact hpair_witness_witness_witness_witness_right_left
  91. 0091split
  92. 0092exact hderivative_step_witness_witness_witness_right_left
  93. 0093intro i
  94. 0094intro hi
  95. 0095specialize hpair_witness_witness_witness_witness_right_right_right i
  96. 0096apply hpair_witness_witness_witness_witness_right_right_right
  97. 0097specialize le_succ (S i)
  98. 0098specialize le_succ l
  99. 0099apply le_succ
  100. 0100exact hi
  101. 0101split
  102. 0102rewrite hfinal_value
  103. 0103exact hvalue_step_witness_witness_witness_right_right_right
  104. 0104rewrite hfinal_derivative
  105. 0105rewrite <- hcoefficient
  106. 0106exact hderivative_step_witness_witness_witness_right_right_right