HD0006

beta_horner_derivative_first_component_functional

The value component of every simultaneous polynomial/derivative evaluation is unique.

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. ∀ m. ∀ w. HornerDerivative(b,c,t,l,n,z) → HornerDerivative(b,c,t,l,m,w) → n = m

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

Definition DAG

HornerDerivative(b,c,t,l,n,z) · 2

Actual proof prerequisites

beta_horner_derivative_value_projectionbeta_horner_eval_functional · checked external prerequisite
Original expanded first-order statement 
forall b c t l n z m w. (exists ff_u_hd_pair ff_v_hd_pair ff_d_hd_pair ff_e_hd_pair. ((((((exists fs_h_ph_hd_pair_body_value_start. fs_h_ph_hd_pair_body_value_start + S (0) = S ((S (0)) * ff_v_hd_pair)) /\ exists fs_q_ph_hd_pair_body_value_start. ff_u_hd_pair = fs_q_ph_hd_pair_body_value_start * S ((S (0)) * ff_v_hd_pair) + (0))) /\ ((((exists fs_h_ph_hd_pair_body_value_terminal. fs_h_ph_hd_pair_body_value_terminal + S (n) = S ((S (l)) * ff_v_hd_pair)) /\ exists fs_q_ph_hd_pair_body_value_terminal. ff_u_hd_pair = fs_q_ph_hd_pair_body_value_terminal * S ((S (l)) * ff_v_hd_pair) + (n))) /\ forall ff_i_ph_hd_pair_body_value_steps. (exists ph_bound_hd_pair_body_value_steps. ph_bound_hd_pair_body_value_steps + S ff_i_ph_hd_pair_body_value_steps = l) -> exists ff_coefficient_ph_hd_pair_body_value_steps ff_previous_ph_hd_pair_body_value_steps ff_current_ph_hd_pair_body_value_steps. ((((exists fs_h_ph_hd_pair_body_value_steps_coefficient. fs_h_ph_hd_pair_body_value_steps_coefficient + S (ff_coefficient_ph_hd_pair_body_value_steps) = S ((S (ff_i_ph_hd_pair_body_value_steps)) * c)) /\ exists fs_q_ph_hd_pair_body_value_steps_coefficient. b = fs_q_ph_hd_pair_body_value_steps_coefficient * S ((S (ff_i_ph_hd_pair_body_value_steps)) * c) + (ff_coefficient_ph_hd_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pair_body_value_steps_before. fs_h_ph_hd_pair_body_value_steps_before + S (ff_previous_ph_hd_pair_body_value_steps) = S ((S (ff_i_ph_hd_pair_body_value_steps)) * ff_v_hd_pair)) /\ exists fs_q_ph_hd_pair_body_value_steps_before. ff_u_hd_pair = fs_q_ph_hd_pair_body_value_steps_before * S ((S (ff_i_ph_hd_pair_body_value_steps)) * ff_v_hd_pair) + (ff_previous_ph_hd_pair_body_value_steps))) /\ ((((exists fs_h_ph_hd_pair_body_value_steps_after. fs_h_ph_hd_pair_body_value_steps_after + S (ff_current_ph_hd_pair_body_value_steps) = S ((S (S ff_i_ph_hd_pair_body_value_steps)) * ff_v_hd_pair)) /\ exists fs_q_ph_hd_pair_body_value_steps_after. ff_u_hd_pair = fs_q_ph_hd_pair_body_value_steps_after * S ((S (S ff_i_ph_hd_pair_body_value_steps)) * ff_v_hd_pair) + (ff_current_ph_hd_pair_body_value_steps))) /\ ff_current_ph_hd_pair_body_value_steps = ff_previous_ph_hd_pair_body_value_steps * t + ff_coefficient_ph_hd_pair_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_pair_body_derivative_start. fs_h_ph_hd_pair_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_pair)) /\ exists fs_q_ph_hd_pair_body_derivative_start. ff_d_hd_pair = fs_q_ph_hd_pair_body_derivative_start * S ((S (0)) * ff_e_hd_pair) + (0))) /\ ((((exists fs_h_ph_hd_pair_body_derivative_terminal. fs_h_ph_hd_pair_body_derivative_terminal + S (z) = S ((S (l)) * ff_e_hd_pair)) /\ exists fs_q_ph_hd_pair_body_derivative_terminal. ff_d_hd_pair = fs_q_ph_hd_pair_body_derivative_terminal * S ((S (l)) * ff_e_hd_pair) + (z))) /\ forall ff_i_ph_hd_pair_body_derivative_steps. (exists ph_bound_hd_pair_body_derivative_steps. ph_bound_hd_pair_body_derivative_steps + S ff_i_ph_hd_pair_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_pair_body_derivative_steps ff_previous_ph_hd_pair_body_derivative_steps ff_current_ph_hd_pair_body_derivative_steps. ((((exists fs_h_ph_hd_pair_body_derivative_steps_coefficient. fs_h_ph_hd_pair_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pair_body_derivative_steps)) * ff_v_hd_pair)) /\ exists fs_q_ph_hd_pair_body_derivative_steps_coefficient. ff_u_hd_pair = fs_q_ph_hd_pair_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_pair_body_derivative_steps)) * ff_v_hd_pair) + (ff_coefficient_ph_hd_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pair_body_derivative_steps_before. fs_h_ph_hd_pair_body_derivative_steps_before + S (ff_previous_ph_hd_pair_body_derivative_steps) = S ((S (ff_i_ph_hd_pair_body_derivative_steps)) * ff_e_hd_pair)) /\ exists fs_q_ph_hd_pair_body_derivative_steps_before. ff_d_hd_pair = fs_q_ph_hd_pair_body_derivative_steps_before * S ((S (ff_i_ph_hd_pair_body_derivative_steps)) * ff_e_hd_pair) + (ff_previous_ph_hd_pair_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_pair_body_derivative_steps_after. fs_h_ph_hd_pair_body_derivative_steps_after + S (ff_current_ph_hd_pair_body_derivative_steps) = S ((S (S ff_i_ph_hd_pair_body_derivative_steps)) * ff_e_hd_pair)) /\ exists fs_q_ph_hd_pair_body_derivative_steps_after. ff_d_hd_pair = fs_q_ph_hd_pair_body_derivative_steps_after * S ((S (S ff_i_ph_hd_pair_body_derivative_steps)) * ff_e_hd_pair) + (ff_current_ph_hd_pair_body_derivative_steps))) /\ ff_current_ph_hd_pair_body_derivative_steps = ff_previous_ph_hd_pair_body_derivative_steps * t + ff_coefficient_ph_hd_pair_body_derivative_steps)))))))) -> (exists ff_u_hd_other ff_v_hd_other ff_d_hd_other ff_e_hd_other. ((((((exists fs_h_ph_hd_other_body_value_start. fs_h_ph_hd_other_body_value_start + S (0) = S ((S (0)) * ff_v_hd_other)) /\ exists fs_q_ph_hd_other_body_value_start. ff_u_hd_other = fs_q_ph_hd_other_body_value_start * S ((S (0)) * ff_v_hd_other) + (0))) /\ ((((exists fs_h_ph_hd_other_body_value_terminal. fs_h_ph_hd_other_body_value_terminal + S (m) = S ((S (l)) * ff_v_hd_other)) /\ exists fs_q_ph_hd_other_body_value_terminal. ff_u_hd_other = fs_q_ph_hd_other_body_value_terminal * S ((S (l)) * ff_v_hd_other) + (m))) /\ forall ff_i_ph_hd_other_body_value_steps. (exists ph_bound_hd_other_body_value_steps. ph_bound_hd_other_body_value_steps + S ff_i_ph_hd_other_body_value_steps = l) -> exists ff_coefficient_ph_hd_other_body_value_steps ff_previous_ph_hd_other_body_value_steps ff_current_ph_hd_other_body_value_steps. ((((exists fs_h_ph_hd_other_body_value_steps_coefficient. fs_h_ph_hd_other_body_value_steps_coefficient + S (ff_coefficient_ph_hd_other_body_value_steps) = S ((S (ff_i_ph_hd_other_body_value_steps)) * c)) /\ exists fs_q_ph_hd_other_body_value_steps_coefficient. b = fs_q_ph_hd_other_body_value_steps_coefficient * S ((S (ff_i_ph_hd_other_body_value_steps)) * c) + (ff_coefficient_ph_hd_other_body_value_steps))) /\ ((((exists fs_h_ph_hd_other_body_value_steps_before. fs_h_ph_hd_other_body_value_steps_before + S (ff_previous_ph_hd_other_body_value_steps) = S ((S (ff_i_ph_hd_other_body_value_steps)) * ff_v_hd_other)) /\ exists fs_q_ph_hd_other_body_value_steps_before. ff_u_hd_other = fs_q_ph_hd_other_body_value_steps_before * S ((S (ff_i_ph_hd_other_body_value_steps)) * ff_v_hd_other) + (ff_previous_ph_hd_other_body_value_steps))) /\ ((((exists fs_h_ph_hd_other_body_value_steps_after. fs_h_ph_hd_other_body_value_steps_after + S (ff_current_ph_hd_other_body_value_steps) = S ((S (S ff_i_ph_hd_other_body_value_steps)) * ff_v_hd_other)) /\ exists fs_q_ph_hd_other_body_value_steps_after. ff_u_hd_other = fs_q_ph_hd_other_body_value_steps_after * S ((S (S ff_i_ph_hd_other_body_value_steps)) * ff_v_hd_other) + (ff_current_ph_hd_other_body_value_steps))) /\ ff_current_ph_hd_other_body_value_steps = ff_previous_ph_hd_other_body_value_steps * t + ff_coefficient_ph_hd_other_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_other_body_derivative_start. fs_h_ph_hd_other_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_other)) /\ exists fs_q_ph_hd_other_body_derivative_start. ff_d_hd_other = fs_q_ph_hd_other_body_derivative_start * S ((S (0)) * ff_e_hd_other) + (0))) /\ ((((exists fs_h_ph_hd_other_body_derivative_terminal. fs_h_ph_hd_other_body_derivative_terminal + S (w) = S ((S (l)) * ff_e_hd_other)) /\ exists fs_q_ph_hd_other_body_derivative_terminal. ff_d_hd_other = fs_q_ph_hd_other_body_derivative_terminal * S ((S (l)) * ff_e_hd_other) + (w))) /\ forall ff_i_ph_hd_other_body_derivative_steps. (exists ph_bound_hd_other_body_derivative_steps. ph_bound_hd_other_body_derivative_steps + S ff_i_ph_hd_other_body_derivative_steps = l) -> exists ff_coefficient_ph_hd_other_body_derivative_steps ff_previous_ph_hd_other_body_derivative_steps ff_current_ph_hd_other_body_derivative_steps. ((((exists fs_h_ph_hd_other_body_derivative_steps_coefficient. fs_h_ph_hd_other_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_other_body_derivative_steps) = S ((S (ff_i_ph_hd_other_body_derivative_steps)) * ff_v_hd_other)) /\ exists fs_q_ph_hd_other_body_derivative_steps_coefficient. ff_u_hd_other = fs_q_ph_hd_other_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_other_body_derivative_steps)) * ff_v_hd_other) + (ff_coefficient_ph_hd_other_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_other_body_derivative_steps_before. fs_h_ph_hd_other_body_derivative_steps_before + S (ff_previous_ph_hd_other_body_derivative_steps) = S ((S (ff_i_ph_hd_other_body_derivative_steps)) * ff_e_hd_other)) /\ exists fs_q_ph_hd_other_body_derivative_steps_before. ff_d_hd_other = fs_q_ph_hd_other_body_derivative_steps_before * S ((S (ff_i_ph_hd_other_body_derivative_steps)) * ff_e_hd_other) + (ff_previous_ph_hd_other_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_other_body_derivative_steps_after. fs_h_ph_hd_other_body_derivative_steps_after + S (ff_current_ph_hd_other_body_derivative_steps) = S ((S (S ff_i_ph_hd_other_body_derivative_steps)) * ff_e_hd_other)) /\ exists fs_q_ph_hd_other_body_derivative_steps_after. ff_d_hd_other = fs_q_ph_hd_other_body_derivative_steps_after * S ((S (S ff_i_ph_hd_other_body_derivative_steps)) * ff_e_hd_other) + (ff_current_ph_hd_other_body_derivative_steps))) /\ ff_current_ph_hd_other_body_derivative_steps = ff_previous_ph_hd_other_body_derivative_steps * t + ff_coefficient_ph_hd_other_body_derivative_steps)))))))) -> n = m

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

33 script commands · 4 reading checkpoints · 0 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 derivative value projection
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 l
  5. L5
    intro n
  6. L6
    intro z
  7. L7
    intro m
  8. L8
    intro w
  9. L9
    intro hleft
  10. L10
    intro hright
02Use earlier factsL11–20

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

  1. L11
    specialize beta_horner_eval_functional b
  2. L12
    specialize beta_horner_eval_functional c
  3. L13
    specialize beta_horner_eval_functional t
  4. L14
    specialize beta_horner_eval_functional l
  5. L15
    specialize beta_horner_eval_functional n
  6. L16
    specialize beta_horner_eval_functional m
  7. L17
    apply beta_horner_eval_functional
  8. L18
    specialize beta_horner_derivative_value_projection b
  9. L19
    specialize beta_horner_derivative_value_projection c
  10. L20
    specialize beta_horner_derivative_value_projection t
03Use earlier factsL21–30

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

  1. L21
    specialize beta_horner_derivative_value_projection l
  2. L22
    specialize beta_horner_derivative_value_projection n
  3. L23
    specialize beta_horner_derivative_value_projection z
  4. L24
    apply beta_horner_derivative_value_projection
  5. L25
    exact hleft
  6. L26
    specialize beta_horner_derivative_value_projection b
  7. L27
    specialize beta_horner_derivative_value_projection c
  8. L28
    specialize beta_horner_derivative_value_projection t
  9. L29
    specialize beta_horner_derivative_value_projection l
  10. L30
    specialize beta_horner_derivative_value_projection m
04Use earlier factsL31–33

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

  1. L31
    specialize beta_horner_derivative_value_projection w
  2. L32
    apply beta_horner_derivative_value_projection
  3. L33
    exact hright

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro l
  5. 0005intro n
  6. 0006intro z
  7. 0007intro m
  8. 0008intro w
  9. 0009intro hleft
  10. 0010intro hright
  11. 0011specialize beta_horner_eval_functional b
  12. 0012specialize beta_horner_eval_functional c
  13. 0013specialize beta_horner_eval_functional t
  14. 0014specialize beta_horner_eval_functional l
  15. 0015specialize beta_horner_eval_functional n
  16. 0016specialize beta_horner_eval_functional m
  17. 0017apply beta_horner_eval_functional
  18. 0018specialize beta_horner_derivative_value_projection b
  19. 0019specialize beta_horner_derivative_value_projection c
  20. 0020specialize beta_horner_derivative_value_projection t
  21. 0021specialize beta_horner_derivative_value_projection l
  22. 0022specialize beta_horner_derivative_value_projection n
  23. 0023specialize beta_horner_derivative_value_projection z
  24. 0024apply beta_horner_derivative_value_projection
  25. 0025exact hleft
  26. 0026specialize beta_horner_derivative_value_projection b
  27. 0027specialize beta_horner_derivative_value_projection c
  28. 0028specialize beta_horner_derivative_value_projection t
  29. 0029specialize beta_horner_derivative_value_projection l
  30. 0030specialize beta_horner_derivative_value_projection m
  31. 0031specialize beta_horner_derivative_value_projection w
  32. 0032apply beta_horner_derivative_value_projection
  33. 0033exact hright