EL0004

lte_twice_correction_polynomial

The doubled correction recurrence has an ordinary polynomial certificate with explicit coefficient carriers.

Alpha v34 checked-use · first admitted v29 · 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.

All displayed hypotheses are required. Powers and positive differences are actual existential outputs. The proof constructs second-order correction identities and iterates the prime step; no binomial expansion or LTE oracle is assumed. The 2-adic variants remain separate open targets.

Exact theorem in conservative defined notation

∀ b. ∀ d. ∀ n. ∀ m. ∀ T. ∀ C. ∀ Q. ∀ H. Q = n · (b · T) + d · C → 2 · C = m · T + d · H → 2 · (b · C + Q) = (m + 2 · n) · (b · T) + d · (b · H + 2 · C)

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 prerequisitefour_square_add_swap_right_tail · checked external prerequisitenatural_mul_swap_right_tail · checked external prerequisitemul_succ_left · checked external prerequisitemul_zero_left · checked external prerequisitezero_add · checked external prerequisiteone_mul · checked external prerequisitemul_one · checked external prerequisite
Original expanded first-order statement 
forall b d n m T C Q H. Q = n * (b * T) + d * C -> 2 * C = m * T + d * H -> 2 * (b * C + Q) = (m + 2 * n) * (b * T) + d * (b * H + 2 * C)

Complete tactic proof in conservative notation

All 197 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

197 script commands · 52 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–10

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

  1. L1
    intro b
  2. L2
    intro d
  3. L3
    intro n
  4. L4
    intro m
  5. L5
    intro T
  6. L6
    intro C
  7. L7
    intro Q
  8. L8
    intro H
  9. L9
    intro hQ
  10. L10
    intro hC
02Calculate and transport equalitiesL11–16

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

  1. L11
    trans b * (2 * C) + 2 * Q
  2. L12
    trans ((((b) * (C))) + ((((b) * (C))) + ((Q) + (Q))))
  3. L13
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  4. L14
    trans ((((C) * (b))) + ((((C) * (b))) + ((Q) + (Q))))
  5. L15
    congr
  6. L16
    trans ((C) * (b))
03Use earlier factsL17–17

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

  1. L17
    apply mul_comm
04Calculate and transport equalitiesL18–22

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

  1. L18
    congr
  2. L19
    refl
  3. L20
    refl
  4. L21
    congr
  5. L22
    trans ((C) * (b))
05Use earlier factsL23–23

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

  1. L23
    apply mul_comm
06Calculate and transport equalitiesL24–33

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

  1. L24
    congr
  2. L25
    refl
  3. L26
    refl
  4. L27
    congr
  5. L28
    refl
  6. L29
    refl
  7. L30
    trans ((((C) * (b))) + ((((C) * (b))) + ((Q) + (Q))))
  8. L31
    refl
  9. L32
    trans ((((b) * (C))) + ((((b) * (C))) + ((Q) + (Q))))
  10. L33
    symm
07Calculate and transport equalitiesL34–35

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

  1. L34
    congr
  2. L35
    trans ((C) * (b))
08Use earlier factsL36–36

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

  1. L36
    apply mul_comm
09Calculate and transport equalitiesL37–41

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

  1. L37
    congr
  2. L38
    refl
  3. L39
    refl
  4. L40
    congr
  5. L41
    trans ((C) * (b))
10Use earlier factsL42–42

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

  1. L42
    apply mul_comm
11Calculate and transport equalitiesL43–52

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

  1. L43
    congr
  2. L44
    refl
  3. L45
    refl
  4. L46
    congr
  5. L47
    refl
  6. L48
    refl
  7. L49
    symm
  8. L50
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  9. L51
    rewrite hC
  10. L52
    rewrite hQ
12Calculate and transport equalitiesL53–60

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

  1. L53
    trans ((((b) * (((m) * (T))))) + ((((b) * (((d) * (H))))) + ((((n) * (((b) * (T))))) + ((((n) * (((b) * (T))))) + ((((d) * (C))) + (((d) * (C))))))))
  2. L54
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  3. L55
    trans ((((T) * (((b) * (m))))) + ((((H) * (((b) * (d))))) + ((((T) * (((b) * (n))))) + ((((T) * (((b) * (n))))) + ((((C) * (d))) + (((C) * (d))))))))
  4. L56
    congr
  5. L57
    trans ((T) * (((b) * (m))))
  6. L58
    trans ((b) * (((T) * (m))))
  7. L59
    congr
  8. L60
    refl
13Use earlier factsL61–62

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

  1. L61
    apply mul_comm
  2. L62
    apply natural_mul_swap_right_tail
14Calculate and transport equalitiesL63–70

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

  1. L63
    congr
  2. L64
    refl
  3. L65
    refl
  4. L66
    congr
  5. L67
    trans ((H) * (((b) * (d))))
  6. L68
    trans ((b) * (((H) * (d))))
  7. L69
    congr
  8. L70
    refl
15Use earlier factsL71–72

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

  1. L71
    apply mul_comm
  2. L72
    apply natural_mul_swap_right_tail
16Calculate and transport equalitiesL73–80

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

  1. L73
    congr
  2. L74
    refl
  3. L75
    refl
  4. L76
    congr
  5. L77
    trans ((T) * (((n) * (b))))
  6. L78
    trans ((n) * (((T) * (b))))
  7. L79
    congr
  8. L80
    refl
17Use earlier factsL81–82

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

  1. L81
    apply mul_comm
  2. L82
    apply natural_mul_swap_right_tail
18Calculate and transport equalitiesL83–85

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

  1. L83
    congr
  2. L84
    refl
  3. L85
    trans ((b) * (n))
19Use earlier factsL86–86

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

  1. L86
    apply mul_comm
20Calculate and transport equalitiesL87–94

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

  1. L87
    congr
  2. L88
    refl
  3. L89
    refl
  4. L90
    congr
  5. L91
    trans ((T) * (((n) * (b))))
  6. L92
    trans ((n) * (((T) * (b))))
  7. L93
    congr
  8. L94
    refl
21Use earlier factsL95–96

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

  1. L95
    apply mul_comm
  2. L96
    apply natural_mul_swap_right_tail
22Calculate and transport equalitiesL97–99

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

  1. L97
    congr
  2. L98
    refl
  3. L99
    trans ((b) * (n))
23Use earlier factsL100–100

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

  1. L100
    apply mul_comm
24Calculate and transport equalitiesL101–105

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

  1. L101
    congr
  2. L102
    refl
  3. L103
    refl
  4. L104
    congr
  5. L105
    trans ((C) * (d))
25Use earlier factsL106–106

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

  1. L106
    apply mul_comm
26Calculate and transport equalitiesL107–110

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

  1. L107
    congr
  2. L108
    refl
  3. L109
    refl
  4. L110
    trans ((C) * (d))
27Use earlier factsL111–111

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

  1. L111
    apply mul_comm
28Calculate and transport equalitiesL112–118

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

  1. L112
    congr
  2. L113
    refl
  3. L114
    refl
  4. L115
    trans ((((T) * (((b) * (m))))) + ((((T) * (((b) * (n))))) + ((((T) * (((b) * (n))))) + ((((H) * (((b) * (d))))) + ((((C) * (d))) + (((C) * (d))))))))
  5. L116
    congr
  6. L117
    refl
  7. L118
    trans ((((T) * (((b) * (n))))) + ((((H) * (((b) * (d))))) + ((((T) * (((b) * (n))))) + ((((C) * (d))) + (((C) * (d)))))))
29Use earlier factsL119–119

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

  1. L119
    apply four_square_add_swap_right_tail
30Calculate and transport equalitiesL120–122

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

  1. L120
    congr
  2. L121
    refl
  3. L122
    trans ((((T) * (((b) * (n))))) + ((((H) * (((b) * (d))))) + ((((C) * (d))) + (((C) * (d))))))
31Use earlier factsL123–123

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

  1. L123
    apply four_square_add_swap_right_tail
32Calculate and transport equalitiesL124–133

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

  1. L124
    congr
  2. L125
    refl
  3. L126
    refl
  4. L127
    trans ((((m) * (((b) * (T))))) + ((((n) * (((b) * (T))))) + ((((n) * (((b) * (T))))) + ((((d) * (((b) * (H))))) + ((((d) * (C))) + (((d) * (C))))))))
  5. L128
    symm
  6. L129
    congr
  7. L130
    trans ((T) * (((m) * (b))))
  8. L131
    trans ((m) * (((T) * (b))))
  9. L132
    congr
  10. L133
    refl
33Use earlier factsL134–135

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

  1. L134
    apply mul_comm
  2. L135
    apply natural_mul_swap_right_tail
34Calculate and transport equalitiesL136–138

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

  1. L136
    congr
  2. L137
    refl
  3. L138
    trans ((b) * (m))
35Use earlier factsL139–139

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

  1. L139
    apply mul_comm
36Calculate and transport equalitiesL140–147

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

  1. L140
    congr
  2. L141
    refl
  3. L142
    refl
  4. L143
    congr
  5. L144
    trans ((T) * (((n) * (b))))
  6. L145
    trans ((n) * (((T) * (b))))
  7. L146
    congr
  8. L147
    refl
37Use earlier factsL148–149

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

  1. L148
    apply mul_comm
  2. L149
    apply natural_mul_swap_right_tail
38Calculate and transport equalitiesL150–152

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

  1. L150
    congr
  2. L151
    refl
  3. L152
    trans ((b) * (n))
39Use earlier factsL153–153

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

  1. L153
    apply mul_comm
40Calculate and transport equalitiesL154–161

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

  1. L154
    congr
  2. L155
    refl
  3. L156
    refl
  4. L157
    congr
  5. L158
    trans ((T) * (((n) * (b))))
  6. L159
    trans ((n) * (((T) * (b))))
  7. L160
    congr
  8. L161
    refl
41Use earlier factsL162–163

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

  1. L162
    apply mul_comm
  2. L163
    apply natural_mul_swap_right_tail
42Calculate and transport equalitiesL164–166

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

  1. L164
    congr
  2. L165
    refl
  3. L166
    trans ((b) * (n))
43Use earlier factsL167–167

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

  1. L167
    apply mul_comm
44Calculate and transport equalitiesL168–175

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

  1. L168
    congr
  2. L169
    refl
  3. L170
    refl
  4. L171
    congr
  5. L172
    trans ((H) * (((d) * (b))))
  6. L173
    trans ((d) * (((H) * (b))))
  7. L174
    congr
  8. L175
    refl
45Use earlier factsL176–177

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

  1. L176
    apply mul_comm
  2. L177
    apply natural_mul_swap_right_tail
46Calculate and transport equalitiesL178–180

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

  1. L178
    congr
  2. L179
    refl
  3. L180
    trans ((b) * (d))
47Use earlier factsL181–181

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

  1. L181
    apply mul_comm
48Calculate and transport equalitiesL182–186

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

  1. L182
    congr
  2. L183
    refl
  3. L184
    refl
  4. L185
    congr
  5. L186
    trans ((C) * (d))
49Use earlier factsL187–187

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

  1. L187
    apply mul_comm
50Calculate and transport equalitiesL188–191

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

  1. L188
    congr
  2. L189
    refl
  3. L190
    refl
  4. L191
    trans ((C) * (d))
51Use earlier factsL192–192

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

  1. L192
    apply mul_comm
52Calculate and transport equalitiesL193–197

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

  1. L193
    congr
  2. L194
    refl
  3. L195
    refl
  4. L196
    symm
  5. L197
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]

Library-wide reading audit

Original defined command ledger · 197 lines
  1. 0001intro b
  2. 0002intro d
  3. 0003intro n
  4. 0004intro m
  5. 0005intro T
  6. 0006intro C
  7. 0007intro Q
  8. 0008intro H
  9. 0009intro hQ
  10. 0010intro hC
  11. 0011trans b * (2 * C) + 2 * Q
  12. 0012trans ((((b) * (C))) + ((((b) * (C))) + ((Q) + (Q))))
  13. 0013simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  14. 0014trans ((((C) * (b))) + ((((C) * (b))) + ((Q) + (Q))))
  15. 0015congr
  16. 0016trans ((C) * (b))
  17. 0017apply mul_comm
  18. 0018congr
  19. 0019refl
  20. 0020refl
  21. 0021congr
  22. 0022trans ((C) * (b))
  23. 0023apply mul_comm
  24. 0024congr
  25. 0025refl
  26. 0026refl
  27. 0027congr
  28. 0028refl
  29. 0029refl
  30. 0030trans ((((C) * (b))) + ((((C) * (b))) + ((Q) + (Q))))
  31. 0031refl
  32. 0032trans ((((b) * (C))) + ((((b) * (C))) + ((Q) + (Q))))
  33. 0033symm
  34. 0034congr
  35. 0035trans ((C) * (b))
  36. 0036apply mul_comm
  37. 0037congr
  38. 0038refl
  39. 0039refl
  40. 0040congr
  41. 0041trans ((C) * (b))
  42. 0042apply mul_comm
  43. 0043congr
  44. 0044refl
  45. 0045refl
  46. 0046congr
  47. 0047refl
  48. 0048refl
  49. 0049symm
  50. 0050simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  51. 0051rewrite hC
  52. 0052rewrite hQ
  53. 0053trans ((((b) * (((m) * (T))))) + ((((b) * (((d) * (H))))) + ((((n) * (((b) * (T))))) + ((((n) * (((b) * (T))))) + ((((d) * (C))) + (((d) * (C))))))))
  54. 0054simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  55. 0055trans ((((T) * (((b) * (m))))) + ((((H) * (((b) * (d))))) + ((((T) * (((b) * (n))))) + ((((T) * (((b) * (n))))) + ((((C) * (d))) + (((C) * (d))))))))
  56. 0056congr
  57. 0057trans ((T) * (((b) * (m))))
  58. 0058trans ((b) * (((T) * (m))))
  59. 0059congr
  60. 0060refl
  61. 0061apply mul_comm
  62. 0062apply natural_mul_swap_right_tail
  63. 0063congr
  64. 0064refl
  65. 0065refl
  66. 0066congr
  67. 0067trans ((H) * (((b) * (d))))
  68. 0068trans ((b) * (((H) * (d))))
  69. 0069congr
  70. 0070refl
  71. 0071apply mul_comm
  72. 0072apply natural_mul_swap_right_tail
  73. 0073congr
  74. 0074refl
  75. 0075refl
  76. 0076congr
  77. 0077trans ((T) * (((n) * (b))))
  78. 0078trans ((n) * (((T) * (b))))
  79. 0079congr
  80. 0080refl
  81. 0081apply mul_comm
  82. 0082apply natural_mul_swap_right_tail
  83. 0083congr
  84. 0084refl
  85. 0085trans ((b) * (n))
  86. 0086apply mul_comm
  87. 0087congr
  88. 0088refl
  89. 0089refl
  90. 0090congr
  91. 0091trans ((T) * (((n) * (b))))
  92. 0092trans ((n) * (((T) * (b))))
  93. 0093congr
  94. 0094refl
  95. 0095apply mul_comm
  96. 0096apply natural_mul_swap_right_tail
  97. 0097congr
  98. 0098refl
  99. 0099trans ((b) * (n))
  100. 0100apply mul_comm
  101. 0101congr
  102. 0102refl
  103. 0103refl
  104. 0104congr
  105. 0105trans ((C) * (d))
  106. 0106apply mul_comm
  107. 0107congr
  108. 0108refl
  109. 0109refl
  110. 0110trans ((C) * (d))
  111. 0111apply mul_comm
  112. 0112congr
  113. 0113refl
  114. 0114refl
  115. 0115trans ((((T) * (((b) * (m))))) + ((((T) * (((b) * (n))))) + ((((T) * (((b) * (n))))) + ((((H) * (((b) * (d))))) + ((((C) * (d))) + (((C) * (d))))))))
  116. 0116congr
  117. 0117refl
  118. 0118trans ((((T) * (((b) * (n))))) + ((((H) * (((b) * (d))))) + ((((T) * (((b) * (n))))) + ((((C) * (d))) + (((C) * (d)))))))
  119. 0119apply four_square_add_swap_right_tail
  120. 0120congr
  121. 0121refl
  122. 0122trans ((((T) * (((b) * (n))))) + ((((H) * (((b) * (d))))) + ((((C) * (d))) + (((C) * (d))))))
  123. 0123apply four_square_add_swap_right_tail
  124. 0124congr
  125. 0125refl
  126. 0126refl
  127. 0127trans ((((m) * (((b) * (T))))) + ((((n) * (((b) * (T))))) + ((((n) * (((b) * (T))))) + ((((d) * (((b) * (H))))) + ((((d) * (C))) + (((d) * (C))))))))
  128. 0128symm
  129. 0129congr
  130. 0130trans ((T) * (((m) * (b))))
  131. 0131trans ((m) * (((T) * (b))))
  132. 0132congr
  133. 0133refl
  134. 0134apply mul_comm
  135. 0135apply natural_mul_swap_right_tail
  136. 0136congr
  137. 0137refl
  138. 0138trans ((b) * (m))
  139. 0139apply mul_comm
  140. 0140congr
  141. 0141refl
  142. 0142refl
  143. 0143congr
  144. 0144trans ((T) * (((n) * (b))))
  145. 0145trans ((n) * (((T) * (b))))
  146. 0146congr
  147. 0147refl
  148. 0148apply mul_comm
  149. 0149apply natural_mul_swap_right_tail
  150. 0150congr
  151. 0151refl
  152. 0152trans ((b) * (n))
  153. 0153apply mul_comm
  154. 0154congr
  155. 0155refl
  156. 0156refl
  157. 0157congr
  158. 0158trans ((T) * (((n) * (b))))
  159. 0159trans ((n) * (((T) * (b))))
  160. 0160congr
  161. 0161refl
  162. 0162apply mul_comm
  163. 0163apply natural_mul_swap_right_tail
  164. 0164congr
  165. 0165refl
  166. 0166trans ((b) * (n))
  167. 0167apply mul_comm
  168. 0168congr
  169. 0169refl
  170. 0170refl
  171. 0171congr
  172. 0172trans ((H) * (((d) * (b))))
  173. 0173trans ((d) * (((H) * (b))))
  174. 0174congr
  175. 0175refl
  176. 0176apply mul_comm
  177. 0177apply natural_mul_swap_right_tail
  178. 0178congr
  179. 0179refl
  180. 0180trans ((b) * (d))
  181. 0181apply mul_comm
  182. 0182congr
  183. 0183refl
  184. 0184refl
  185. 0185congr
  186. 0186trans ((C) * (d))
  187. 0187apply mul_comm
  188. 0188congr
  189. 0189refl
  190. 0190refl
  191. 0191trans ((C) * (d))
  192. 0192apply mul_comm
  193. 0193congr
  194. 0194refl
  195. 0195refl
  196. 0196symm
  197. 0197simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]