HD000B

beta_horner_derivative_exists_unique

Every arbitrary beta-coded natural polynomial has exactly one simultaneously evaluated value/formal-derivative pair.

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

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_existsbeta_horner_derivative_functional
Original expanded first-order statement 
forall b c t l. exists n z. ((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)))))))) /\ forall m w. (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 /\ z = w))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

28 script commands · 9 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 (2)
beta horner derivative value existsbeta horner derivative functional
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 l
02Use earlier factsL5–8

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

  1. L5
    specialize beta_horner_derivative_value_exists b
  2. L6
    specialize beta_horner_derivative_value_exists c
  3. L7
    specialize beta_horner_derivative_value_exists t
  4. L8
    specialize beta_horner_derivative_value_exists l
03Separate the logical casesL9–10

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

  1. L9
    cases beta_horner_derivative_value_exists
  2. L10
    cases beta_horner_derivative_value_exists_witness
04Construct an explicit witnessL11–12

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

  1. L11
    exists x
  2. L12
    exists x1
05Separate the logical casesL13–13

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

  1. L13
    split
06Use earlier factsL14–14

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

  1. L14
    exact beta_horner_derivative_value_exists_witness_witness
07Fix variables and assumptionsL15–17

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

  1. L15
    intro m
  2. L16
    intro w
  3. L17
    intro hother
08Use earlier factsL18–27

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

  1. L18
    specialize beta_horner_derivative_functional b
  2. L19
    specialize beta_horner_derivative_functional c
  3. L20
    specialize beta_horner_derivative_functional t
  4. L21
    specialize beta_horner_derivative_functional l
  5. L22
    specialize beta_horner_derivative_functional x
  6. L23
    specialize beta_horner_derivative_functional x1
  7. L24
    specialize beta_horner_derivative_functional m
  8. L25
    specialize beta_horner_derivative_functional w
  9. L26
    apply beta_horner_derivative_functional
  10. L27
    exact beta_horner_derivative_value_exists_witness_witness
09Use earlier factsL28–28

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

  1. L28
    exact hother

Library-wide reading audit

Original defined command ledger · 28 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro l
  5. 0005specialize beta_horner_derivative_value_exists b
  6. 0006specialize beta_horner_derivative_value_exists c
  7. 0007specialize beta_horner_derivative_value_exists t
  8. 0008specialize beta_horner_derivative_value_exists l
  9. 0009cases beta_horner_derivative_value_exists
  10. 0010cases beta_horner_derivative_value_exists_witness
  11. 0011exists x
  12. 0012exists x1
  13. 0013split
  14. 0014exact beta_horner_derivative_value_exists_witness_witness
  15. 0015intro m
  16. 0016intro w
  17. 0017intro hother
  18. 0018specialize beta_horner_derivative_functional b
  19. 0019specialize beta_horner_derivative_functional c
  20. 0020specialize beta_horner_derivative_functional t
  21. 0021specialize beta_horner_derivative_functional l
  22. 0022specialize beta_horner_derivative_functional x
  23. 0023specialize beta_horner_derivative_functional x1
  24. 0024specialize beta_horner_derivative_functional m
  25. 0025specialize beta_horner_derivative_functional w
  26. 0026apply beta_horner_derivative_functional
  27. 0027exact beta_horner_derivative_value_exists_witness_witness
  28. 0028exact hother