BT00WD · Bertrand theorem

bertrand_scaled_budget_root_37

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

The factorized RFC-v1 H budget at root 37 lies below its square.

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.

Statement with defined notation

Le(6 · (2 · 38 + 7 · 19),37 · 37)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
exists bqb_le_gap_hj32_scaled_budget_root_37. bqb_le_gap_hj32_scaled_budget_root_37 + (6 * (2 * 38 + 7 * 19)) = (37 * 37)

Proof neighborhood

Direct theorem prerequisites

BT00W7 linear_square_budget BT0007 mul_add BT0008 mul_assoc BT0006 mul_comm BT000B add_mul BT0003 add_assoc BT0002 add_comm

Direct theorem dependents

BT00WU bertrand_h_root_37_from_total

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

167 script commands · 37 reading checkpoints · 28 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 (7)
linear square budgetmul addmul assocmul commadd muladd assocadd comm
01Use earlier factsL1–8

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

  1. L1
    specialize linear_square_budget 6
  2. L2
    specialize linear_square_budget 5
  3. L3
    specialize linear_square_budget 37
  4. L4
    specialize linear_square_budget 7
  5. L5
    specialize linear_square_budget 24
  6. L6
    specialize linear_square_budget (2 * 38 + 7 * 19)
  7. L7
    specialize linear_square_budget (3 * 37 + 4)
  8. L8
    apply linear_square_budget
02Calculate and transport equalitiesL9–9

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

  1. L9
    norm_num
03Establish hk_firstL10–12

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

  1. L10
    have hk_first : 2 * 38 = 5 * 10 + 26
  2. L11
    norm_num
  3. L12
    rewrite hk_first
04Establish hk_secondL13–13

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

  1. L13
    have hk_second : 7 * 19 = 5 * 20 + 33
05Establish hk_sevenL14–21

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

  1. L14
    have hk_seven : 7 = 5 + 2
  2. L15
    norm_num
  3. L16
    rewrite hk_seven
  4. L17
    trans 5 * 19 + 2 * 19
  5. L18
    specialize add_mul 5
  6. L19
    specialize add_mul 2
  7. L20
    specialize add_mul 19
  8. L21
    apply add_mul
06Establish hk_two_nineteenL22–24

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

  1. L22
    have hk_two_nineteen : 2 * 19 = 38
  2. L23
    norm_num
  3. L24
    rewrite hk_two_nineteen
07Establish hk_rightL25–25

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

  1. L25
    have hk_right : 5 * 20 + 33 = 5 * 19 + 38
08Establish hk_stepL26–26

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

  1. L26
    have hk_step : 5 * 20 = 5 * 19 + 5
09Establish hk_twentyL27–36

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

  1. L27
    have hk_twenty : 20 = 19 + 1
  2. L28
    norm_num
  3. L29
    rewrite hk_twenty
  4. L30
    trans 5 * 19 + 5 * 1
  5. L31
    specialize mul_add 5
  6. L32
    specialize mul_add 19
  7. L33
    specialize mul_add 1
  8. L34
    apply mul_add
  9. L35
    congr
  10. L36
    refl
10Calculate and transport equalitiesL37–38

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

  1. L37
    norm_num
  2. L38
    rewrite hk_step
11Establish hk_assoc_stepL39–44

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

  1. L39
    have hk_assoc_step : (5 * 19 + 5) + 33 = 5 * 19 + (5 + 33)
  2. L40
    specialize add_assoc (5 * 19)
  3. L41
    specialize add_assoc 5
  4. L42
    specialize add_assoc 33
  5. L43
    apply add_assoc
  6. L44
    rewrite hk_assoc_step
12Establish hk_thirty_eightL45–51

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

  1. L45
    have hk_thirty_eight : 5 + 33 = 38
  2. L46
    norm_num
  3. L47
    rewrite hk_thirty_eight
  4. L48
    refl
  5. L49
    symm
  6. L50
    exact hk_right
  7. L51
    rewrite hk_second
13Establish hk_assoc_oneL52–57

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

  1. L52
    have hk_assoc_one : (5 * 10 + 26) + (5 * 20 + 33) = 5 * 10 + (26 + (5 * 20 + 33))
  2. L53
    specialize add_assoc (5 * 10)
  3. L54
    specialize add_assoc 26
  4. L55
    specialize add_assoc (5 * 20 + 33)
  5. L56
    apply add_assoc
  6. L57
    rewrite hk_assoc_one
14Establish hk_assoc_twoL58–64

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

  1. L58
    have hk_assoc_two : 26 + (5 * 20 + 33) = (26 + 5 * 20) + 33
  2. L59
    symm
  3. L60
    specialize add_assoc 26
  4. L61
    specialize add_assoc (5 * 20)
  5. L62
    specialize add_assoc 33
  6. L63
    apply add_assoc
  7. L64
    rewrite hk_assoc_two
15Establish hk_commL65–69

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

  1. L65
    have hk_comm : 26 + 5 * 20 = 5 * 20 + 26
  2. L66
    specialize add_comm 26
  3. L67
    specialize add_comm (5 * 20)
  4. L68
    apply add_comm
  5. L69
    rewrite hk_comm
16Establish hk_assoc_threeL70–75

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

  1. L70
    have hk_assoc_three : (5 * 20 + 26) + 33 = 5 * 20 + (26 + 33)
  2. L71
    specialize add_assoc (5 * 20)
  3. L72
    specialize add_assoc 26
  4. L73
    specialize add_assoc 33
  5. L74
    apply add_assoc
  6. L75
    rewrite hk_assoc_three
17Establish hk_assoc_fourL76–82

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

  1. L76
    have hk_assoc_four : 5 * 10 + (5 * 20 + (26 + 33)) = (5 * 10 + 5 * 20) + (26 + 33)
  2. L77
    symm
  3. L78
    specialize add_assoc (5 * 10)
  4. L79
    specialize add_assoc (5 * 20)
  5. L80
    specialize add_assoc (26 + 33)
  6. L81
    apply add_assoc
  7. L82
    rewrite hk_assoc_four
18Establish hk_factor_oneL83–88

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

  1. L83
    have hk_factor_one : 5 * (10 + 20) = 5 * 10 + 5 * 20
  2. L84
    specialize mul_add 5
  3. L85
    specialize mul_add 10
  4. L86
    specialize mul_add 20
  5. L87
    apply mul_add
  6. L88
    rewrite <- hk_factor_one
19Establish hk_thirtyL89–91

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

  1. L89
    have hk_thirty : 10 + 20 = 30
  2. L90
    norm_num
  3. L91
    rewrite hk_thirty
20Establish hk_remainderL92–94

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

  1. L92
    have hk_remainder : 26 + 33 = 5 * 7 + 24
  2. L93
    norm_num
  3. L94
    rewrite hk_remainder
21Establish hk_assoc_fiveL95–101

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

  1. L95
    have hk_assoc_five : 5 * 30 + (5 * 7 + 24) = (5 * 30 + 5 * 7) + 24
  2. L96
    symm
  3. L97
    specialize add_assoc (5 * 30)
  4. L98
    specialize add_assoc (5 * 7)
  5. L99
    specialize add_assoc 24
  6. L100
    apply add_assoc
  7. L101
    rewrite hk_assoc_five
22Establish hk_factor_twoL102–107

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

  1. L102
    have hk_factor_two : 5 * (30 + 7) = 5 * 30 + 5 * 7
  2. L103
    specialize mul_add 5
  3. L104
    specialize mul_add 30
  4. L105
    specialize mul_add 7
  5. L106
    apply mul_add
  6. L107
    rewrite <- hk_factor_two
23Establish hk_rootL108–111

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

  1. L108
    have hk_root : 30 + 7 = 37
  2. L109
    norm_num
  3. L110
    rewrite hk_root
  4. L111
    refl
24Establish hd_bridgeL112–112

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

  1. L112
    have hd_bridge : 6 * 24 = 4 * 36
25Establish hd_twenty_fourL113–122

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

  1. L113
    have hd_twenty_four : 24 = 4 * 6
  2. L114
    norm_num
  3. L115
    rewrite hd_twenty_four
  4. L116
    trans (6 * 4) * 6
  5. L117
    symm
  6. L118
    specialize mul_assoc 6
  7. L119
    specialize mul_assoc 4
  8. L120
    specialize mul_assoc 6
  9. L121
    apply mul_assoc
  10. L122
    trans (4 * 6) * 6
26Calculate and transport equalitiesL123–123

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

  1. L123
    congr
27Use earlier factsL124–126

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

  1. L124
    specialize mul_comm 6
  2. L125
    specialize mul_comm 4
  3. L126
    apply mul_comm
28Calculate and transport equalitiesL127–128

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

  1. L127
    refl
  2. L128
    trans 4 * (6 * 6)
29Use earlier factsL129–132

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

  1. L129
    specialize mul_assoc 4
  2. L130
    specialize mul_assoc 6
  3. L131
    specialize mul_assoc 6
  4. L132
    apply mul_assoc
30Establish hd_thirty_sixL133–137

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

  1. L133
    have hd_thirty_six : 36 = 6 * 6
  2. L134
    norm_num
  3. L135
    rewrite <- hd_thirty_six
  4. L136
    refl
  5. L137
    rewrite hd_bridge
31Establish hd_assocL138–143

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

  1. L138
    have hd_assoc : (3 * 37 + 4) + 4 * 36 = 3 * 37 + (4 + 4 * 36)
  2. L139
    specialize add_assoc (3 * 37)
  3. L140
    specialize add_assoc 4
  4. L141
    specialize add_assoc (4 * 36)
  5. L142
    apply add_assoc
  6. L143
    rewrite hd_assoc
32Establish hd_stepL144–144

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

  1. L144
    have hd_step : 4 + 4 * 36 = 4 * 37
33Establish hd_thirty_sevenL145–154

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

  1. L145
    have hd_thirty_seven : 37 = 1 + 36
  2. L146
    norm_num
  3. L147
    rewrite hd_thirty_seven
  4. L148
    trans 4 * 1 + 4 * 36
  5. L149
    congr
  6. L150
    norm_num
  7. L151
    refl
  8. L152
    symm
  9. L153
    specialize mul_add 4
  10. L154
    specialize mul_add 1
34Use earlier factsL155–156

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

  1. L155
    specialize mul_add 36
  2. L156
    apply mul_add
35Calculate and transport equalitiesL157–157

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

  1. L157
    rewrite hd_step
36Establish hd_factorL158–163

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

  1. L158
    have hd_factor : (3 + 4) * 37 = 3 * 37 + 4 * 37
  2. L159
    specialize add_mul 3
  3. L160
    specialize add_mul 4
  4. L161
    specialize add_mul 37
  5. L162
    apply add_mul
  6. L163
    rewrite <- hd_factor
37Establish hd_sevenL164–167

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

  1. L164
    have hd_seven : 3 + 4 = 7
  2. L165
    norm_num
  3. L166
    rewrite hd_seven
  4. L167
    refl

Library-wide reading audit

Original defined command ledger · 167 lines
  1. 0001specialize linear_square_budget 6
  2. 0002specialize linear_square_budget 5
  3. 0003specialize linear_square_budget 37
  4. 0004specialize linear_square_budget 7
  5. 0005specialize linear_square_budget 24
  6. 0006specialize linear_square_budget (2 * 38 + 7 * 19)
  7. 0007specialize linear_square_budget (3 * 37 + 4)
  8. 0008apply linear_square_budget
  9. 0009norm_num
  10. 0010have hk_first : 2 * 38 = 5 * 10 + 26
  11. 0011norm_num
  12. 0012rewrite hk_first
  13. 0013have hk_second : 7 * 19 = 5 * 20 + 33
  14. 0014have hk_seven : 7 = 5 + 2
  15. 0015norm_num
  16. 0016rewrite hk_seven
  17. 0017trans 5 * 19 + 2 * 19
  18. 0018specialize add_mul 5
  19. 0019specialize add_mul 2
  20. 0020specialize add_mul 19
  21. 0021apply add_mul
  22. 0022have hk_two_nineteen : 2 * 19 = 38
  23. 0023norm_num
  24. 0024rewrite hk_two_nineteen
  25. 0025have hk_right : 5 * 20 + 33 = 5 * 19 + 38
  26. 0026have hk_step : 5 * 20 = 5 * 19 + 5
  27. 0027have hk_twenty : 20 = 19 + 1
  28. 0028norm_num
  29. 0029rewrite hk_twenty
  30. 0030trans 5 * 19 + 5 * 1
  31. 0031specialize mul_add 5
  32. 0032specialize mul_add 19
  33. 0033specialize mul_add 1
  34. 0034apply mul_add
  35. 0035congr
  36. 0036refl
  37. 0037norm_num
  38. 0038rewrite hk_step
  39. 0039have hk_assoc_step : (5 * 19 + 5) + 33 = 5 * 19 + (5 + 33)
  40. 0040specialize add_assoc (5 * 19)
  41. 0041specialize add_assoc 5
  42. 0042specialize add_assoc 33
  43. 0043apply add_assoc
  44. 0044rewrite hk_assoc_step
  45. 0045have hk_thirty_eight : 5 + 33 = 38
  46. 0046norm_num
  47. 0047rewrite hk_thirty_eight
  48. 0048refl
  49. 0049symm
  50. 0050exact hk_right
  51. 0051rewrite hk_second
  52. 0052have hk_assoc_one : (5 * 10 + 26) + (5 * 20 + 33) = 5 * 10 + (26 + (5 * 20 + 33))
  53. 0053specialize add_assoc (5 * 10)
  54. 0054specialize add_assoc 26
  55. 0055specialize add_assoc (5 * 20 + 33)
  56. 0056apply add_assoc
  57. 0057rewrite hk_assoc_one
  58. 0058have hk_assoc_two : 26 + (5 * 20 + 33) = (26 + 5 * 20) + 33
  59. 0059symm
  60. 0060specialize add_assoc 26
  61. 0061specialize add_assoc (5 * 20)
  62. 0062specialize add_assoc 33
  63. 0063apply add_assoc
  64. 0064rewrite hk_assoc_two
  65. 0065have hk_comm : 26 + 5 * 20 = 5 * 20 + 26
  66. 0066specialize add_comm 26
  67. 0067specialize add_comm (5 * 20)
  68. 0068apply add_comm
  69. 0069rewrite hk_comm
  70. 0070have hk_assoc_three : (5 * 20 + 26) + 33 = 5 * 20 + (26 + 33)
  71. 0071specialize add_assoc (5 * 20)
  72. 0072specialize add_assoc 26
  73. 0073specialize add_assoc 33
  74. 0074apply add_assoc
  75. 0075rewrite hk_assoc_three
  76. 0076have hk_assoc_four : 5 * 10 + (5 * 20 + (26 + 33)) = (5 * 10 + 5 * 20) + (26 + 33)
  77. 0077symm
  78. 0078specialize add_assoc (5 * 10)
  79. 0079specialize add_assoc (5 * 20)
  80. 0080specialize add_assoc (26 + 33)
  81. 0081apply add_assoc
  82. 0082rewrite hk_assoc_four
  83. 0083have hk_factor_one : 5 * (10 + 20) = 5 * 10 + 5 * 20
  84. 0084specialize mul_add 5
  85. 0085specialize mul_add 10
  86. 0086specialize mul_add 20
  87. 0087apply mul_add
  88. 0088rewrite <- hk_factor_one
  89. 0089have hk_thirty : 10 + 20 = 30
  90. 0090norm_num
  91. 0091rewrite hk_thirty
  92. 0092have hk_remainder : 26 + 33 = 5 * 7 + 24
  93. 0093norm_num
  94. 0094rewrite hk_remainder
  95. 0095have hk_assoc_five : 5 * 30 + (5 * 7 + 24) = (5 * 30 + 5 * 7) + 24
  96. 0096symm
  97. 0097specialize add_assoc (5 * 30)
  98. 0098specialize add_assoc (5 * 7)
  99. 0099specialize add_assoc 24
  100. 0100apply add_assoc
  101. 0101rewrite hk_assoc_five
  102. 0102have hk_factor_two : 5 * (30 + 7) = 5 * 30 + 5 * 7
  103. 0103specialize mul_add 5
  104. 0104specialize mul_add 30
  105. 0105specialize mul_add 7
  106. 0106apply mul_add
  107. 0107rewrite <- hk_factor_two
  108. 0108have hk_root : 30 + 7 = 37
  109. 0109norm_num
  110. 0110rewrite hk_root
  111. 0111refl
  112. 0112have hd_bridge : 6 * 24 = 4 * 36
  113. 0113have hd_twenty_four : 24 = 4 * 6
  114. 0114norm_num
  115. 0115rewrite hd_twenty_four
  116. 0116trans (6 * 4) * 6
  117. 0117symm
  118. 0118specialize mul_assoc 6
  119. 0119specialize mul_assoc 4
  120. 0120specialize mul_assoc 6
  121. 0121apply mul_assoc
  122. 0122trans (4 * 6) * 6
  123. 0123congr
  124. 0124specialize mul_comm 6
  125. 0125specialize mul_comm 4
  126. 0126apply mul_comm
  127. 0127refl
  128. 0128trans 4 * (6 * 6)
  129. 0129specialize mul_assoc 4
  130. 0130specialize mul_assoc 6
  131. 0131specialize mul_assoc 6
  132. 0132apply mul_assoc
  133. 0133have hd_thirty_six : 36 = 6 * 6
  134. 0134norm_num
  135. 0135rewrite <- hd_thirty_six
  136. 0136refl
  137. 0137rewrite hd_bridge
  138. 0138have hd_assoc : (3 * 37 + 4) + 4 * 36 = 3 * 37 + (4 + 4 * 36)
  139. 0139specialize add_assoc (3 * 37)
  140. 0140specialize add_assoc 4
  141. 0141specialize add_assoc (4 * 36)
  142. 0142apply add_assoc
  143. 0143rewrite hd_assoc
  144. 0144have hd_step : 4 + 4 * 36 = 4 * 37
  145. 0145have hd_thirty_seven : 37 = 1 + 36
  146. 0146norm_num
  147. 0147rewrite hd_thirty_seven
  148. 0148trans 4 * 1 + 4 * 36
  149. 0149congr
  150. 0150norm_num
  151. 0151refl
  152. 0152symm
  153. 0153specialize mul_add 4
  154. 0154specialize mul_add 1
  155. 0155specialize mul_add 36
  156. 0156apply mul_add
  157. 0157rewrite hd_step
  158. 0158have hd_factor : (3 + 4) * 37 = 3 * 37 + 4 * 37
  159. 0159specialize add_mul 3
  160. 0160specialize add_mul 4
  161. 0161specialize add_mul 37
  162. 0162apply add_mul
  163. 0163rewrite <- hd_factor
  164. 0164have hd_seven : 3 + 4 = 7
  165. 0165norm_num
  166. 0166rewrite hd_seven
  167. 0167refl