HD000E

beta_horner_derivative_constant

A one-coefficient polynomial evaluates to its actual decoded constant and has formal derivative zero.

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. ∀ n. ∀ z. HornerDerivative(b,c,t,1,n,z) → ∃ x. Beta(b,c,0,x) ∧ (n = x ∧ z = 0)

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) · 1

Actual proof prerequisites

beta_horner_derivative_successor_decomposebeta_horner_derivative_emptymul_zero_left · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall b c t n z. (exists ff_u_hd_constant ff_v_hd_constant ff_d_hd_constant ff_e_hd_constant. ((((((exists fs_h_ph_hd_constant_body_value_start. fs_h_ph_hd_constant_body_value_start + S (0) = S ((S (0)) * ff_v_hd_constant)) /\ exists fs_q_ph_hd_constant_body_value_start. ff_u_hd_constant = fs_q_ph_hd_constant_body_value_start * S ((S (0)) * ff_v_hd_constant) + (0))) /\ ((((exists fs_h_ph_hd_constant_body_value_terminal. fs_h_ph_hd_constant_body_value_terminal + S (n) = S ((S (S 0)) * ff_v_hd_constant)) /\ exists fs_q_ph_hd_constant_body_value_terminal. ff_u_hd_constant = fs_q_ph_hd_constant_body_value_terminal * S ((S (S 0)) * ff_v_hd_constant) + (n))) /\ forall ff_i_ph_hd_constant_body_value_steps. (exists ph_bound_hd_constant_body_value_steps. ph_bound_hd_constant_body_value_steps + S ff_i_ph_hd_constant_body_value_steps = S 0) -> exists ff_coefficient_ph_hd_constant_body_value_steps ff_previous_ph_hd_constant_body_value_steps ff_current_ph_hd_constant_body_value_steps. ((((exists fs_h_ph_hd_constant_body_value_steps_coefficient. fs_h_ph_hd_constant_body_value_steps_coefficient + S (ff_coefficient_ph_hd_constant_body_value_steps) = S ((S (ff_i_ph_hd_constant_body_value_steps)) * c)) /\ exists fs_q_ph_hd_constant_body_value_steps_coefficient. b = fs_q_ph_hd_constant_body_value_steps_coefficient * S ((S (ff_i_ph_hd_constant_body_value_steps)) * c) + (ff_coefficient_ph_hd_constant_body_value_steps))) /\ ((((exists fs_h_ph_hd_constant_body_value_steps_before. fs_h_ph_hd_constant_body_value_steps_before + S (ff_previous_ph_hd_constant_body_value_steps) = S ((S (ff_i_ph_hd_constant_body_value_steps)) * ff_v_hd_constant)) /\ exists fs_q_ph_hd_constant_body_value_steps_before. ff_u_hd_constant = fs_q_ph_hd_constant_body_value_steps_before * S ((S (ff_i_ph_hd_constant_body_value_steps)) * ff_v_hd_constant) + (ff_previous_ph_hd_constant_body_value_steps))) /\ ((((exists fs_h_ph_hd_constant_body_value_steps_after. fs_h_ph_hd_constant_body_value_steps_after + S (ff_current_ph_hd_constant_body_value_steps) = S ((S (S ff_i_ph_hd_constant_body_value_steps)) * ff_v_hd_constant)) /\ exists fs_q_ph_hd_constant_body_value_steps_after. ff_u_hd_constant = fs_q_ph_hd_constant_body_value_steps_after * S ((S (S ff_i_ph_hd_constant_body_value_steps)) * ff_v_hd_constant) + (ff_current_ph_hd_constant_body_value_steps))) /\ ff_current_ph_hd_constant_body_value_steps = ff_previous_ph_hd_constant_body_value_steps * t + ff_coefficient_ph_hd_constant_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_constant_body_derivative_start. fs_h_ph_hd_constant_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_constant)) /\ exists fs_q_ph_hd_constant_body_derivative_start. ff_d_hd_constant = fs_q_ph_hd_constant_body_derivative_start * S ((S (0)) * ff_e_hd_constant) + (0))) /\ ((((exists fs_h_ph_hd_constant_body_derivative_terminal. fs_h_ph_hd_constant_body_derivative_terminal + S (z) = S ((S (S 0)) * ff_e_hd_constant)) /\ exists fs_q_ph_hd_constant_body_derivative_terminal. ff_d_hd_constant = fs_q_ph_hd_constant_body_derivative_terminal * S ((S (S 0)) * ff_e_hd_constant) + (z))) /\ forall ff_i_ph_hd_constant_body_derivative_steps. (exists ph_bound_hd_constant_body_derivative_steps. ph_bound_hd_constant_body_derivative_steps + S ff_i_ph_hd_constant_body_derivative_steps = S 0) -> exists ff_coefficient_ph_hd_constant_body_derivative_steps ff_previous_ph_hd_constant_body_derivative_steps ff_current_ph_hd_constant_body_derivative_steps. ((((exists fs_h_ph_hd_constant_body_derivative_steps_coefficient. fs_h_ph_hd_constant_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_constant_body_derivative_steps) = S ((S (ff_i_ph_hd_constant_body_derivative_steps)) * ff_v_hd_constant)) /\ exists fs_q_ph_hd_constant_body_derivative_steps_coefficient. ff_u_hd_constant = fs_q_ph_hd_constant_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_constant_body_derivative_steps)) * ff_v_hd_constant) + (ff_coefficient_ph_hd_constant_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_constant_body_derivative_steps_before. fs_h_ph_hd_constant_body_derivative_steps_before + S (ff_previous_ph_hd_constant_body_derivative_steps) = S ((S (ff_i_ph_hd_constant_body_derivative_steps)) * ff_e_hd_constant)) /\ exists fs_q_ph_hd_constant_body_derivative_steps_before. ff_d_hd_constant = fs_q_ph_hd_constant_body_derivative_steps_before * S ((S (ff_i_ph_hd_constant_body_derivative_steps)) * ff_e_hd_constant) + (ff_previous_ph_hd_constant_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_constant_body_derivative_steps_after. fs_h_ph_hd_constant_body_derivative_steps_after + S (ff_current_ph_hd_constant_body_derivative_steps) = S ((S (S ff_i_ph_hd_constant_body_derivative_steps)) * ff_e_hd_constant)) /\ exists fs_q_ph_hd_constant_body_derivative_steps_after. ff_d_hd_constant = fs_q_ph_hd_constant_body_derivative_steps_after * S ((S (S ff_i_ph_hd_constant_body_derivative_steps)) * ff_e_hd_constant) + (ff_current_ph_hd_constant_body_derivative_steps))) /\ ff_current_ph_hd_constant_body_derivative_steps = ff_previous_ph_hd_constant_body_derivative_steps * t + ff_coefficient_ph_hd_constant_body_derivative_steps)))))))) -> exists a. ((((exists fs_h_hd_constant_coefficient. fs_h_hd_constant_coefficient + S (a) = S ((S (0)) * c)) /\ exists fs_q_hd_constant_coefficient. b = fs_q_hd_constant_coefficient * S ((S (0)) * c) + (a))) /\ ((n = a) /\ z = 0))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

49 script commands · 21 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 (2)
beta horner derivative successor decomposebeta horner derivative empty

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

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 n
  5. L5
    intro z
  6. L6
    intro hpair
02Establish hdecompositionL7–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner derivative successor decompose.

  1. L7
    have hdecomposition : ∃ a. ∃ r. ∃ q. Beta(b,c,0,a) ∧ (HornerDerivative(b,c,t,0,r,q) ∧ (n = r · t + a ∧ z = q · t + r))Definitions: BetaHornerDerivativeOriginal native command in the exact edition
  2. L8
    specialize beta_horner_derivative_successor_decompose b
  3. L9
    specialize beta_horner_derivative_successor_decompose c
  4. L10
    specialize beta_horner_derivative_successor_decompose t
  5. L11
    specialize beta_horner_derivative_successor_decompose 0
  6. L12
    specialize beta_horner_derivative_successor_decompose n
  7. L13
    specialize beta_horner_derivative_successor_decompose z
  8. L14
    apply beta_horner_derivative_successor_decompose
  9. L15
    exact hpair
03Separate the logical casesL16–21

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

  1. L16
    cases hdecomposition
  2. L17
    cases hdecomposition_witness
  3. L18
    cases hdecomposition_witness_witness
  4. L19
    cases hdecomposition_witness_witness_witness
  5. L20
    cases hdecomposition_witness_witness_witness_right
  6. L21
    cases hdecomposition_witness_witness_witness_right_right
04Establish hzeroL22–29

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

  1. L22
    have hzero : (x1 = 0 /\ x2 = 0)
  2. L23
    specialize beta_horner_derivative_empty b
  3. L24
    specialize beta_horner_derivative_empty c
  4. L25
    specialize beta_horner_derivative_empty t
  5. L26
    specialize beta_horner_derivative_empty x1
  6. L27
    specialize beta_horner_derivative_empty x2
  7. L28
    apply beta_horner_derivative_empty
  8. L29
    exact hdecomposition_witness_witness_witness_right_left
05Separate the logical casesL30–30

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

  1. L30
    cases hzero
06Construct an explicit witnessL31–31

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

  1. L31
    exists x
07Separate the logical casesL32–32

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

  1. L32
    split
08Use earlier factsL33–33

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

  1. L33
    exact hdecomposition_witness_witness_witness_left
09Separate the logical casesL34–34

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

  1. L34
    split
10Calculate and transport equalitiesL35–35

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

  1. L35
    trans x1 * t + x
11Use earlier factsL36–36

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

  1. L36
    exact hdecomposition_witness_witness_witness_right_right_left
12Calculate and transport equalitiesL37–37

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

  1. L37
    rewrite hzero_left
13Use earlier factsL38–38

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

  1. L38
    specialize mul_zero_left t
14Calculate and transport equalitiesL39–39

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

  1. L39
    rewrite mul_zero_left
15Use earlier factsL40–41

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

  1. L40
    specialize zero_add x
  2. L41
    exact zero_add
16Calculate and transport equalitiesL42–42

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

  1. L42
    trans x2 * t + x1
17Use earlier factsL43–43

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

  1. L43
    exact hdecomposition_witness_witness_witness_right_right_right
18Calculate and transport equalitiesL44–45

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

  1. L44
    rewrite hzero_right
  2. L45
    rewrite hzero_left
19Use earlier factsL46–46

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

  1. L46
    specialize mul_zero_left t
20Calculate and transport equalitiesL47–47

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

  1. L47
    rewrite mul_zero_left
21Use earlier factsL48–49

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

  1. L48
    specialize zero_add 0
  2. L49
    exact zero_add

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro n
  5. 0005intro z
  6. 0006intro hpair
  7. 0007have hdecomposition : exists a r q. ((((exists fs_h_hd_constant_step. fs_h_hd_constant_step + S (a) = S ((S (0)) * c)) /\ exists fs_q_hd_constant_step. b = fs_q_hd_constant_step * S ((S (0)) * c) + (a))) /\ ((exists ff_u_hd_constant_prefix ff_v_hd_constant_prefix ff_d_hd_constant_prefix ff_e_hd_constant_prefix. ((((((exists fs_h_ph_hd_constant_prefix_body_value_start. fs_h_ph_hd_constant_prefix_body_value_start + S (0) = S ((S (0)) * ff_v_hd_constant_prefix)) /\ exists fs_q_ph_hd_constant_prefix_body_value_start. ff_u_hd_constant_prefix = fs_q_ph_hd_constant_prefix_body_value_start * S ((S (0)) * ff_v_hd_constant_prefix) + (0))) /\ ((((exists fs_h_ph_hd_constant_prefix_body_value_terminal. fs_h_ph_hd_constant_prefix_body_value_terminal + S (r) = S ((S (0)) * ff_v_hd_constant_prefix)) /\ exists fs_q_ph_hd_constant_prefix_body_value_terminal. ff_u_hd_constant_prefix = fs_q_ph_hd_constant_prefix_body_value_terminal * S ((S (0)) * ff_v_hd_constant_prefix) + (r))) /\ forall ff_i_ph_hd_constant_prefix_body_value_steps. (exists ph_bound_hd_constant_prefix_body_value_steps. ph_bound_hd_constant_prefix_body_value_steps + S ff_i_ph_hd_constant_prefix_body_value_steps = 0) -> exists ff_coefficient_ph_hd_constant_prefix_body_value_steps ff_previous_ph_hd_constant_prefix_body_value_steps ff_current_ph_hd_constant_prefix_body_value_steps. ((((exists fs_h_ph_hd_constant_prefix_body_value_steps_coefficient. fs_h_ph_hd_constant_prefix_body_value_steps_coefficient + S (ff_coefficient_ph_hd_constant_prefix_body_value_steps) = S ((S (ff_i_ph_hd_constant_prefix_body_value_steps)) * c)) /\ exists fs_q_ph_hd_constant_prefix_body_value_steps_coefficient. b = fs_q_ph_hd_constant_prefix_body_value_steps_coefficient * S ((S (ff_i_ph_hd_constant_prefix_body_value_steps)) * c) + (ff_coefficient_ph_hd_constant_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_constant_prefix_body_value_steps_before. fs_h_ph_hd_constant_prefix_body_value_steps_before + S (ff_previous_ph_hd_constant_prefix_body_value_steps) = S ((S (ff_i_ph_hd_constant_prefix_body_value_steps)) * ff_v_hd_constant_prefix)) /\ exists fs_q_ph_hd_constant_prefix_body_value_steps_before. ff_u_hd_constant_prefix = fs_q_ph_hd_constant_prefix_body_value_steps_before * S ((S (ff_i_ph_hd_constant_prefix_body_value_steps)) * ff_v_hd_constant_prefix) + (ff_previous_ph_hd_constant_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_constant_prefix_body_value_steps_after. fs_h_ph_hd_constant_prefix_body_value_steps_after + S (ff_current_ph_hd_constant_prefix_body_value_steps) = S ((S (S ff_i_ph_hd_constant_prefix_body_value_steps)) * ff_v_hd_constant_prefix)) /\ exists fs_q_ph_hd_constant_prefix_body_value_steps_after. ff_u_hd_constant_prefix = fs_q_ph_hd_constant_prefix_body_value_steps_after * S ((S (S ff_i_ph_hd_constant_prefix_body_value_steps)) * ff_v_hd_constant_prefix) + (ff_current_ph_hd_constant_prefix_body_value_steps))) /\ ff_current_ph_hd_constant_prefix_body_value_steps = ff_previous_ph_hd_constant_prefix_body_value_steps * t + ff_coefficient_ph_hd_constant_prefix_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_constant_prefix_body_derivative_start. fs_h_ph_hd_constant_prefix_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_constant_prefix)) /\ exists fs_q_ph_hd_constant_prefix_body_derivative_start. ff_d_hd_constant_prefix = fs_q_ph_hd_constant_prefix_body_derivative_start * S ((S (0)) * ff_e_hd_constant_prefix) + (0))) /\ ((((exists fs_h_ph_hd_constant_prefix_body_derivative_terminal. fs_h_ph_hd_constant_prefix_body_derivative_terminal + S (q) = S ((S (0)) * ff_e_hd_constant_prefix)) /\ exists fs_q_ph_hd_constant_prefix_body_derivative_terminal. ff_d_hd_constant_prefix = fs_q_ph_hd_constant_prefix_body_derivative_terminal * S ((S (0)) * ff_e_hd_constant_prefix) + (q))) /\ forall ff_i_ph_hd_constant_prefix_body_derivative_steps. (exists ph_bound_hd_constant_prefix_body_derivative_steps. ph_bound_hd_constant_prefix_body_derivative_steps + S ff_i_ph_hd_constant_prefix_body_derivative_steps = 0) -> exists ff_coefficient_ph_hd_constant_prefix_body_derivative_steps ff_previous_ph_hd_constant_prefix_body_derivative_steps ff_current_ph_hd_constant_prefix_body_derivative_steps. ((((exists fs_h_ph_hd_constant_prefix_body_derivative_steps_coefficient. fs_h_ph_hd_constant_prefix_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_constant_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_constant_prefix_body_derivative_steps)) * ff_v_hd_constant_prefix)) /\ exists fs_q_ph_hd_constant_prefix_body_derivative_steps_coefficient. ff_u_hd_constant_prefix = fs_q_ph_hd_constant_prefix_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_constant_prefix_body_derivative_steps)) * ff_v_hd_constant_prefix) + (ff_coefficient_ph_hd_constant_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_constant_prefix_body_derivative_steps_before. fs_h_ph_hd_constant_prefix_body_derivative_steps_before + S (ff_previous_ph_hd_constant_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_constant_prefix_body_derivative_steps)) * ff_e_hd_constant_prefix)) /\ exists fs_q_ph_hd_constant_prefix_body_derivative_steps_before. ff_d_hd_constant_prefix = fs_q_ph_hd_constant_prefix_body_derivative_steps_before * S ((S (ff_i_ph_hd_constant_prefix_body_derivative_steps)) * ff_e_hd_constant_prefix) + (ff_previous_ph_hd_constant_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_constant_prefix_body_derivative_steps_after. fs_h_ph_hd_constant_prefix_body_derivative_steps_after + S (ff_current_ph_hd_constant_prefix_body_derivative_steps) = S ((S (S ff_i_ph_hd_constant_prefix_body_derivative_steps)) * ff_e_hd_constant_prefix)) /\ exists fs_q_ph_hd_constant_prefix_body_derivative_steps_after. ff_d_hd_constant_prefix = fs_q_ph_hd_constant_prefix_body_derivative_steps_after * S ((S (S ff_i_ph_hd_constant_prefix_body_derivative_steps)) * ff_e_hd_constant_prefix) + (ff_current_ph_hd_constant_prefix_body_derivative_steps))) /\ ff_current_ph_hd_constant_prefix_body_derivative_steps = ff_previous_ph_hd_constant_prefix_body_derivative_steps * t + ff_coefficient_ph_hd_constant_prefix_body_derivative_steps)))))))) /\ ((n = r * t + a) /\ z = q * t + r)))
  8. 0008specialize beta_horner_derivative_successor_decompose b
  9. 0009specialize beta_horner_derivative_successor_decompose c
  10. 0010specialize beta_horner_derivative_successor_decompose t
  11. 0011specialize beta_horner_derivative_successor_decompose 0
  12. 0012specialize beta_horner_derivative_successor_decompose n
  13. 0013specialize beta_horner_derivative_successor_decompose z
  14. 0014apply beta_horner_derivative_successor_decompose
  15. 0015exact hpair
  16. 0016cases hdecomposition
  17. 0017cases hdecomposition_witness
  18. 0018cases hdecomposition_witness_witness
  19. 0019cases hdecomposition_witness_witness_witness
  20. 0020cases hdecomposition_witness_witness_witness_right
  21. 0021cases hdecomposition_witness_witness_witness_right_right
  22. 0022have hzero : (x1 = 0 /\ x2 = 0)
  23. 0023specialize beta_horner_derivative_empty b
  24. 0024specialize beta_horner_derivative_empty c
  25. 0025specialize beta_horner_derivative_empty t
  26. 0026specialize beta_horner_derivative_empty x1
  27. 0027specialize beta_horner_derivative_empty x2
  28. 0028apply beta_horner_derivative_empty
  29. 0029exact hdecomposition_witness_witness_witness_right_left
  30. 0030cases hzero
  31. 0031exists x
  32. 0032split
  33. 0033exact hdecomposition_witness_witness_witness_left
  34. 0034split
  35. 0035trans x1 * t + x
  36. 0036exact hdecomposition_witness_witness_witness_right_right_left
  37. 0037rewrite hzero_left
  38. 0038specialize mul_zero_left t
  39. 0039rewrite mul_zero_left
  40. 0040specialize zero_add x
  41. 0041exact zero_add
  42. 0042trans x2 * t + x1
  43. 0043exact hdecomposition_witness_witness_witness_right_right_right
  44. 0044rewrite hzero_right
  45. 0045rewrite hzero_left
  46. 0046specialize mul_zero_left t
  47. 0047rewrite mul_zero_left
  48. 0048specialize zero_add 0
  49. 0049exact zero_add