HD0007

beta_horner_derivative_empty

The empty beta-coded polynomial and its exact formal derivative both evaluate to 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,0,n,z) → n = 0 ∧ z = 0

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_eval_empty · checked external prerequisite
Original expanded first-order statement 
forall b c t n z. (exists ff_u_hd_empty ff_v_hd_empty ff_d_hd_empty ff_e_hd_empty. ((((((exists fs_h_ph_hd_empty_body_value_start. fs_h_ph_hd_empty_body_value_start + S (0) = S ((S (0)) * ff_v_hd_empty)) /\ exists fs_q_ph_hd_empty_body_value_start. ff_u_hd_empty = fs_q_ph_hd_empty_body_value_start * S ((S (0)) * ff_v_hd_empty) + (0))) /\ ((((exists fs_h_ph_hd_empty_body_value_terminal. fs_h_ph_hd_empty_body_value_terminal + S (n) = S ((S (0)) * ff_v_hd_empty)) /\ exists fs_q_ph_hd_empty_body_value_terminal. ff_u_hd_empty = fs_q_ph_hd_empty_body_value_terminal * S ((S (0)) * ff_v_hd_empty) + (n))) /\ forall ff_i_ph_hd_empty_body_value_steps. (exists ph_bound_hd_empty_body_value_steps. ph_bound_hd_empty_body_value_steps + S ff_i_ph_hd_empty_body_value_steps = 0) -> exists ff_coefficient_ph_hd_empty_body_value_steps ff_previous_ph_hd_empty_body_value_steps ff_current_ph_hd_empty_body_value_steps. ((((exists fs_h_ph_hd_empty_body_value_steps_coefficient. fs_h_ph_hd_empty_body_value_steps_coefficient + S (ff_coefficient_ph_hd_empty_body_value_steps) = S ((S (ff_i_ph_hd_empty_body_value_steps)) * c)) /\ exists fs_q_ph_hd_empty_body_value_steps_coefficient. b = fs_q_ph_hd_empty_body_value_steps_coefficient * S ((S (ff_i_ph_hd_empty_body_value_steps)) * c) + (ff_coefficient_ph_hd_empty_body_value_steps))) /\ ((((exists fs_h_ph_hd_empty_body_value_steps_before. fs_h_ph_hd_empty_body_value_steps_before + S (ff_previous_ph_hd_empty_body_value_steps) = S ((S (ff_i_ph_hd_empty_body_value_steps)) * ff_v_hd_empty)) /\ exists fs_q_ph_hd_empty_body_value_steps_before. ff_u_hd_empty = fs_q_ph_hd_empty_body_value_steps_before * S ((S (ff_i_ph_hd_empty_body_value_steps)) * ff_v_hd_empty) + (ff_previous_ph_hd_empty_body_value_steps))) /\ ((((exists fs_h_ph_hd_empty_body_value_steps_after. fs_h_ph_hd_empty_body_value_steps_after + S (ff_current_ph_hd_empty_body_value_steps) = S ((S (S ff_i_ph_hd_empty_body_value_steps)) * ff_v_hd_empty)) /\ exists fs_q_ph_hd_empty_body_value_steps_after. ff_u_hd_empty = fs_q_ph_hd_empty_body_value_steps_after * S ((S (S ff_i_ph_hd_empty_body_value_steps)) * ff_v_hd_empty) + (ff_current_ph_hd_empty_body_value_steps))) /\ ff_current_ph_hd_empty_body_value_steps = ff_previous_ph_hd_empty_body_value_steps * t + ff_coefficient_ph_hd_empty_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_empty_body_derivative_start. fs_h_ph_hd_empty_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_empty)) /\ exists fs_q_ph_hd_empty_body_derivative_start. ff_d_hd_empty = fs_q_ph_hd_empty_body_derivative_start * S ((S (0)) * ff_e_hd_empty) + (0))) /\ ((((exists fs_h_ph_hd_empty_body_derivative_terminal. fs_h_ph_hd_empty_body_derivative_terminal + S (z) = S ((S (0)) * ff_e_hd_empty)) /\ exists fs_q_ph_hd_empty_body_derivative_terminal. ff_d_hd_empty = fs_q_ph_hd_empty_body_derivative_terminal * S ((S (0)) * ff_e_hd_empty) + (z))) /\ forall ff_i_ph_hd_empty_body_derivative_steps. (exists ph_bound_hd_empty_body_derivative_steps. ph_bound_hd_empty_body_derivative_steps + S ff_i_ph_hd_empty_body_derivative_steps = 0) -> exists ff_coefficient_ph_hd_empty_body_derivative_steps ff_previous_ph_hd_empty_body_derivative_steps ff_current_ph_hd_empty_body_derivative_steps. ((((exists fs_h_ph_hd_empty_body_derivative_steps_coefficient. fs_h_ph_hd_empty_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_empty_body_derivative_steps) = S ((S (ff_i_ph_hd_empty_body_derivative_steps)) * ff_v_hd_empty)) /\ exists fs_q_ph_hd_empty_body_derivative_steps_coefficient. ff_u_hd_empty = fs_q_ph_hd_empty_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_empty_body_derivative_steps)) * ff_v_hd_empty) + (ff_coefficient_ph_hd_empty_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_empty_body_derivative_steps_before. fs_h_ph_hd_empty_body_derivative_steps_before + S (ff_previous_ph_hd_empty_body_derivative_steps) = S ((S (ff_i_ph_hd_empty_body_derivative_steps)) * ff_e_hd_empty)) /\ exists fs_q_ph_hd_empty_body_derivative_steps_before. ff_d_hd_empty = fs_q_ph_hd_empty_body_derivative_steps_before * S ((S (ff_i_ph_hd_empty_body_derivative_steps)) * ff_e_hd_empty) + (ff_previous_ph_hd_empty_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_empty_body_derivative_steps_after. fs_h_ph_hd_empty_body_derivative_steps_after + S (ff_current_ph_hd_empty_body_derivative_steps) = S ((S (S ff_i_ph_hd_empty_body_derivative_steps)) * ff_e_hd_empty)) /\ exists fs_q_ph_hd_empty_body_derivative_steps_after. ff_d_hd_empty = fs_q_ph_hd_empty_body_derivative_steps_after * S ((S (S ff_i_ph_hd_empty_body_derivative_steps)) * ff_e_hd_empty) + (ff_current_ph_hd_empty_body_derivative_steps))) /\ ff_current_ph_hd_empty_body_derivative_steps = ff_previous_ph_hd_empty_body_derivative_steps * t + ff_coefficient_ph_hd_empty_body_derivative_steps)))))))) -> (n = 0 /\ z = 0)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

28 script commands · 7 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.

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
02Separate the logical casesL7–12

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

  1. L7
    cases hpair
  2. L8
    cases hpair_witness
  3. L9
    cases hpair_witness_witness
  4. L10
    cases hpair_witness_witness_witness
  5. L11
    cases hpair_witness_witness_witness_witness
  6. L12
    split
03Use earlier factsL13–17

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

  1. L13
    specialize beta_horner_eval_empty b
  2. L14
    specialize beta_horner_eval_empty c
  3. L15
    specialize beta_horner_eval_empty t
  4. L16
    specialize beta_horner_eval_empty n
  5. L17
    apply beta_horner_eval_empty
04Construct an explicit witnessL18–19

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

  1. L18
    exists x
  2. L19
    exists x1
05Use earlier factsL20–25

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

  1. L20
    exact hpair_witness_witness_witness_witness_left
  2. L21
    specialize beta_horner_eval_empty x
  3. L22
    specialize beta_horner_eval_empty x1
  4. L23
    specialize beta_horner_eval_empty t
  5. L24
    specialize beta_horner_eval_empty z
  6. L25
    apply beta_horner_eval_empty
06Construct an explicit witnessL26–27

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

  1. L26
    exists x2
  2. L27
    exists x3
07Use earlier factsL28–28

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

  1. L28
    exact hpair_witness_witness_witness_witness_right

Library-wide reading audit

Original defined command ledger · 28 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro n
  5. 0005intro z
  6. 0006intro hpair
  7. 0007cases hpair
  8. 0008cases hpair_witness
  9. 0009cases hpair_witness_witness
  10. 0010cases hpair_witness_witness_witness
  11. 0011cases hpair_witness_witness_witness_witness
  12. 0012split
  13. 0013specialize beta_horner_eval_empty b
  14. 0014specialize beta_horner_eval_empty c
  15. 0015specialize beta_horner_eval_empty t
  16. 0016specialize beta_horner_eval_empty n
  17. 0017apply beta_horner_eval_empty
  18. 0018exists x
  19. 0019exists x1
  20. 0020exact hpair_witness_witness_witness_witness_left
  21. 0021specialize beta_horner_eval_empty x
  22. 0022specialize beta_horner_eval_empty x1
  23. 0023specialize beta_horner_eval_empty t
  24. 0024specialize beta_horner_eval_empty z
  25. 0025apply beta_horner_eval_empty
  26. 0026exists x2
  27. 0027exists x3
  28. 0028exact hpair_witness_witness_witness_witness_right