HD0002

beta_horner_derivative_value_exists

Every arbitrary beta-coded natural polynomial has an actual simultaneous value and exact formal derivative.

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)

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

Definition DAG

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

Actual proof prerequisites

beta_horner_derivative_trace_existsbeta_at_exists · checked external prerequisite
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))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

44 script commands · 16 reading checkpoints · 2 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 trace exists
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_trace_exists b
  2. L6
    specialize beta_horner_derivative_trace_exists c
  3. L7
    specialize beta_horner_derivative_trace_exists t
  4. L8
    specialize beta_horner_derivative_trace_exists l
03Separate the logical casesL9–15

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

  1. L9
    cases beta_horner_derivative_trace_exists
  2. L10
    cases beta_horner_derivative_trace_exists_witness
  3. L11
    cases beta_horner_derivative_trace_exists_witness_witness
  4. L12
    cases beta_horner_derivative_trace_exists_witness_witness_witness
  5. L13
    cases beta_horner_derivative_trace_exists_witness_witness_witness_witness
  6. L14
    cases beta_horner_derivative_trace_exists_witness_witness_witness_witness_left
  7. L15
    cases beta_horner_derivative_trace_exists_witness_witness_witness_witness_right
04Establish hvalueL16–20

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

  1. L16
    have hvalue : exists n. (((exists fs_h_hd_value_terminal. fs_h_hd_value_terminal + S (n) = S ((S (l)) * x1)) /\ exists fs_q_hd_value_terminal. x = fs_q_hd_value_terminal * S ((S (l)) * x1) + (n)))
  2. L17
    specialize beta_at_exists x
  3. L18
    specialize beta_at_exists x1
  4. L19
    specialize beta_at_exists l
  5. L20
    exact beta_at_exists
05Separate the logical casesL21–21

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

  1. L21
    cases hvalue
06Establish hderivativeL22–26

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

  1. L22
    have hderivative : exists z. (((exists fs_h_hd_derivative_terminal. fs_h_hd_derivative_terminal + S (z) = S ((S (l)) * x3)) /\ exists fs_q_hd_derivative_terminal. x2 = fs_q_hd_derivative_terminal * S ((S (l)) * x3) + (z)))
  2. L23
    specialize beta_at_exists x2
  3. L24
    specialize beta_at_exists x3
  4. L25
    specialize beta_at_exists l
  5. L26
    exact beta_at_exists
07Separate the logical casesL27–27

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

  1. L27
    cases hderivative
08Construct an explicit witnessL28–33

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

  1. L28
    exists x4
  2. L29
    exists x5
  3. L30
    exists x
  4. L31
    exists x1
  5. L32
    exists x2
  6. L33
    exists x3
09Separate the logical casesL34–35

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

  1. L34
    split
  2. L35
    split
10Use earlier factsL36–36

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

  1. L36
    exact beta_horner_derivative_trace_exists_witness_witness_witness_witness_left_left
11Separate the logical casesL37–37

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

  1. L37
    split
12Use earlier factsL38–39

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

  1. L38
    exact hvalue_witness
  2. L39
    exact beta_horner_derivative_trace_exists_witness_witness_witness_witness_left_right
13Separate the logical casesL40–40

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

  1. L40
    split
14Use earlier factsL41–41

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

  1. L41
    exact beta_horner_derivative_trace_exists_witness_witness_witness_witness_right_left
15Separate the logical casesL42–42

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

  1. L42
    split
16Use earlier factsL43–44

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

  1. L43
    exact hderivative_witness
  2. L44
    exact beta_horner_derivative_trace_exists_witness_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro l
  5. 0005specialize beta_horner_derivative_trace_exists b
  6. 0006specialize beta_horner_derivative_trace_exists c
  7. 0007specialize beta_horner_derivative_trace_exists t
  8. 0008specialize beta_horner_derivative_trace_exists l
  9. 0009cases beta_horner_derivative_trace_exists
  10. 0010cases beta_horner_derivative_trace_exists_witness
  11. 0011cases beta_horner_derivative_trace_exists_witness_witness
  12. 0012cases beta_horner_derivative_trace_exists_witness_witness_witness
  13. 0013cases beta_horner_derivative_trace_exists_witness_witness_witness_witness
  14. 0014cases beta_horner_derivative_trace_exists_witness_witness_witness_witness_left
  15. 0015cases beta_horner_derivative_trace_exists_witness_witness_witness_witness_right
  16. 0016have hvalue : exists n. (((exists fs_h_hd_value_terminal. fs_h_hd_value_terminal + S (n) = S ((S (l)) * x1)) /\ exists fs_q_hd_value_terminal. x = fs_q_hd_value_terminal * S ((S (l)) * x1) + (n)))
  17. 0017specialize beta_at_exists x
  18. 0018specialize beta_at_exists x1
  19. 0019specialize beta_at_exists l
  20. 0020exact beta_at_exists
  21. 0021cases hvalue
  22. 0022have hderivative : exists z. (((exists fs_h_hd_derivative_terminal. fs_h_hd_derivative_terminal + S (z) = S ((S (l)) * x3)) /\ exists fs_q_hd_derivative_terminal. x2 = fs_q_hd_derivative_terminal * S ((S (l)) * x3) + (z)))
  23. 0023specialize beta_at_exists x2
  24. 0024specialize beta_at_exists x3
  25. 0025specialize beta_at_exists l
  26. 0026exact beta_at_exists
  27. 0027cases hderivative
  28. 0028exists x4
  29. 0029exists x5
  30. 0030exists x
  31. 0031exists x1
  32. 0032exists x2
  33. 0033exists x3
  34. 0034split
  35. 0035split
  36. 0036exact beta_horner_derivative_trace_exists_witness_witness_witness_witness_left_left
  37. 0037split
  38. 0038exact hvalue_witness
  39. 0039exact beta_horner_derivative_trace_exists_witness_witness_witness_witness_left_right
  40. 0040split
  41. 0041exact beta_horner_derivative_trace_exists_witness_witness_witness_witness_right_left
  42. 0042split
  43. 0043exact hderivative_witness
  44. 0044exact beta_horner_derivative_trace_exists_witness_witness_witness_witness_right_right