TH0007

horner_taylor_successor_identity

The successor Horner transition has an exact subtraction-free quadratic Taylor remainder.

Alpha v34 checked-use · first admitted v25 · 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 exact natural polynomial Taylor remainders, bounded corrections, and one-step divisibility lifts. G095 is now closed in the separate Alpha-v27 hensel-lifting branch for integer polynomials, unrestricted input roots, unique canonical representatives, and every positive prime power. Full G095 proof · Alpha v27

Exact theorem in conservative defined notation

∀ r. ∀ d. ∀ h. ∀ q. ∀ t. ∀ a. (r + h · d + h · h · q) · (t + h) + a = r · t + a + h · (d · t + r) + h · h · (q · (t + h) + d)

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

Definition DAG

none

Actual proof prerequisites

add_mul · checked external prerequisitemul_add · checked external prerequisitemul_assoc · checked external prerequisitemul_comm · checked external prerequisiteadd_assoc · checked external prerequisiteadd_comm · checked external prerequisitehensel_add_swap_nested
Original expanded first-order statement 
forall r d h q t a. (((r + h * d) + (h * h) * q) * (t + h) + a) = ((r * t + a) + h * (d * t + r)) + (h * h) * (q * (t + h) + d)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

68 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 (1)
hensel add swap nested
01Fix variables and assumptionsL1–6

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

  1. L1
    intro r
  2. L2
    intro d
  3. L3
    intro h
  4. L4
    intro q
  5. L5
    intro t
  6. L6
    intro a
02Calculate and transport equalitiesL7–7

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

  1. L7
    simp [add_mul, mul_add, mul_assoc, add_assoc]
03Establish hrhL8–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L8
    have hrh : r * h = h * r
  2. L9
    apply mul_comm
04Establish hdhL10–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L10
    have hdh : d * h = h * d
  2. L11
    apply mul_comm
  3. L12
    rewrite hrh
  4. L13
    rewrite hdh
  5. L14
    congr
  6. L15
    refl
  7. L16
    trans (h * r + (h * (d * t) + (h * (h * d) + (h * (h * (q * t)) + (a + h * (h * (q * h)))))))
  8. L17
    congr
  9. L18
    refl
  10. L19
    congr
05Calculate and transport equalitiesL20–24

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

  1. L20
    refl
  2. L21
    congr
  3. L22
    refl
  4. L23
    congr
  5. L24
    refl
06Use earlier factsL25–25

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

  1. L25
    apply add_comm
07Calculate and transport equalitiesL26–32

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

  1. L26
    trans (h * r + (h * (d * t) + (h * (h * d) + (a + (h * (h * (q * t)) + h * (h * (q * h)))))))
  2. L27
    congr
  3. L28
    refl
  4. L29
    congr
  5. L30
    refl
  6. L31
    congr
  7. L32
    refl
08Use earlier factsL33–33

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

  1. L33
    apply hensel_add_swap_nested
09Calculate and transport equalitiesL34–38

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

  1. L34
    trans (h * r + (h * (d * t) + (a + (h * (h * d) + (h * (h * (q * t)) + h * (h * (q * h)))))))
  2. L35
    congr
  3. L36
    refl
  4. L37
    congr
  5. L38
    refl
10Use earlier factsL39–39

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

  1. L39
    apply hensel_add_swap_nested
11Calculate and transport equalitiesL40–42

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

  1. L40
    trans (h * r + (a + (h * (d * t) + (h * (h * d) + (h * (h * (q * t)) + h * (h * (q * h)))))))
  2. L41
    congr
  3. L42
    refl
12Use earlier factsL43–43

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

  1. L43
    apply hensel_add_swap_nested
13Calculate and transport equalitiesL44–44

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

  1. L44
    trans (a + (h * r + (h * (d * t) + (h * (h * d) + (h * (h * (q * t)) + h * (h * (q * h)))))))
14Use earlier factsL45–45

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

  1. L45
    apply hensel_add_swap_nested
15Calculate and transport equalitiesL46–48

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

  1. L46
    trans (a + (h * (d * t) + (h * r + (h * (h * d) + (h * (h * (q * t)) + h * (h * (q * h)))))))
  2. L47
    congr
  3. L48
    refl
16Use earlier factsL49–49

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

  1. L49
    apply hensel_add_swap_nested
17Calculate and transport equalitiesL50–56

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

  1. L50
    trans (a + (h * (d * t) + (h * r + (h * (h * (q * t)) + (h * (h * d) + h * (h * (q * h)))))))
  2. L51
    congr
  3. L52
    refl
  4. L53
    congr
  5. L54
    refl
  6. L55
    congr
  7. L56
    refl
18Use earlier factsL57–57

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

  1. L57
    apply hensel_add_swap_nested
19Calculate and transport equalitiesL58–66

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

  1. L58
    trans (a + (h * (d * t) + (h * r + (h * (h * (q * t)) + (h * (h * (q * h)) + h * (h * d))))))
  2. L59
    congr
  3. L60
    refl
  4. L61
    congr
  5. L62
    refl
  6. L63
    congr
  7. L64
    refl
  8. L65
    congr
  9. L66
    refl
20Use earlier factsL67–67

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

  1. L67
    apply add_comm
21Calculate and transport equalitiesL68–68

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

  1. L68
    refl

Library-wide reading audit

Original defined command ledger · 68 lines
  1. 0001intro r
  2. 0002intro d
  3. 0003intro h
  4. 0004intro q
  5. 0005intro t
  6. 0006intro a
  7. 0007simp [add_mul, mul_add, mul_assoc, add_assoc]
  8. 0008have hrh : r * h = h * r
  9. 0009apply mul_comm
  10. 0010have hdh : d * h = h * d
  11. 0011apply mul_comm
  12. 0012rewrite hrh
  13. 0013rewrite hdh
  14. 0014congr
  15. 0015refl
  16. 0016trans (h * r + (h * (d * t) + (h * (h * d) + (h * (h * (q * t)) + (a + h * (h * (q * h)))))))
  17. 0017congr
  18. 0018refl
  19. 0019congr
  20. 0020refl
  21. 0021congr
  22. 0022refl
  23. 0023congr
  24. 0024refl
  25. 0025apply add_comm
  26. 0026trans (h * r + (h * (d * t) + (h * (h * d) + (a + (h * (h * (q * t)) + h * (h * (q * h)))))))
  27. 0027congr
  28. 0028refl
  29. 0029congr
  30. 0030refl
  31. 0031congr
  32. 0032refl
  33. 0033apply hensel_add_swap_nested
  34. 0034trans (h * r + (h * (d * t) + (a + (h * (h * d) + (h * (h * (q * t)) + h * (h * (q * h)))))))
  35. 0035congr
  36. 0036refl
  37. 0037congr
  38. 0038refl
  39. 0039apply hensel_add_swap_nested
  40. 0040trans (h * r + (a + (h * (d * t) + (h * (h * d) + (h * (h * (q * t)) + h * (h * (q * h)))))))
  41. 0041congr
  42. 0042refl
  43. 0043apply hensel_add_swap_nested
  44. 0044trans (a + (h * r + (h * (d * t) + (h * (h * d) + (h * (h * (q * t)) + h * (h * (q * h)))))))
  45. 0045apply hensel_add_swap_nested
  46. 0046trans (a + (h * (d * t) + (h * r + (h * (h * d) + (h * (h * (q * t)) + h * (h * (q * h)))))))
  47. 0047congr
  48. 0048refl
  49. 0049apply hensel_add_swap_nested
  50. 0050trans (a + (h * (d * t) + (h * r + (h * (h * (q * t)) + (h * (h * d) + h * (h * (q * h)))))))
  51. 0051congr
  52. 0052refl
  53. 0053congr
  54. 0054refl
  55. 0055congr
  56. 0056refl
  57. 0057apply hensel_add_swap_nested
  58. 0058trans (a + (h * (d * t) + (h * r + (h * (h * (q * t)) + (h * (h * (q * h)) + h * (h * d))))))
  59. 0059congr
  60. 0060refl
  61. 0061congr
  62. 0062refl
  63. 0063congr
  64. 0064refl
  65. 0065congr
  66. 0066refl
  67. 0067apply add_comm
  68. 0068refl