BT00WD

bertrand_scaled_budget_root_37

Alpha body-checked · checked-use disabled

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

Exact expanded 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)

Structural proof guide

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

Direct prerequisites: linear_square_budget, mul_add, mul_assoc, mul_comm, add_mul, add_assoc, add_comm. The authored body proceeds by intermediate claims (28), equality transport (27), closed numeral normalization (15).

Proof neighborhood

Direct dependencies

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

Direct dependents

BT00WU bertrand_h_root_37_from_total

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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