BT00WC

bertrand_scaled_budget_root_36

Alpha body-checked · checked-use disabled

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

Exact expanded PA statement

exists bqb_le_gap_hj32_scaled_budget_root_36. bqb_le_gap_hj32_scaled_budget_root_36 + (6 * (2 * 37 + 2 * (5 * 13))) = (36 * 36)

Structural proof guide

The factorized RFC-v1 H budget at root 36 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 (13), equality transport (13), closed numeral normalization (7).

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

BT00WT bertrand_h_root_36_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 36
  4. 0004specialize linear_square_budget 6
  5. 0005specialize linear_square_budget 24
  6. 0006specialize linear_square_budget (2 * 37 + 2 * (5 * 13))
  7. 0007specialize linear_square_budget (2 * 36)
  8. 0008apply linear_square_budget
  9. 0009norm_num
  10. 0010have hk_first : 2 * 37 = 5 * 10 + 24
  11. 0011norm_num
  12. 0012rewrite hk_first
  13. 0013have hk_second : 2 * (5 * 13) = 5 * 26
  14. 0014trans (2 * 5) * 13
  15. 0015symm
  16. 0016specialize mul_assoc 2
  17. 0017specialize mul_assoc 5
  18. 0018specialize mul_assoc 13
  19. 0019apply mul_assoc
  20. 0020trans (5 * 2) * 13
  21. 0021congr
  22. 0022specialize mul_comm 2
  23. 0023specialize mul_comm 5
  24. 0024apply mul_comm
  25. 0025refl
  26. 0026trans 5 * (2 * 13)
  27. 0027specialize mul_assoc 5
  28. 0028specialize mul_assoc 2
  29. 0029specialize mul_assoc 13
  30. 0030apply mul_assoc
  31. 0031have hk_twenty_six : 2 * 13 = 26
  32. 0032norm_num
  33. 0033rewrite hk_twenty_six
  34. 0034refl
  35. 0035rewrite hk_second
  36. 0036have hk_assoc_one : (5 * 10 + 24) + 5 * 26 = 5 * 10 + (24 + 5 * 26)
  37. 0037specialize add_assoc (5 * 10)
  38. 0038specialize add_assoc 24
  39. 0039specialize add_assoc (5 * 26)
  40. 0040apply add_assoc
  41. 0041rewrite hk_assoc_one
  42. 0042have hk_comm : 24 + 5 * 26 = 5 * 26 + 24
  43. 0043specialize add_comm 24
  44. 0044specialize add_comm (5 * 26)
  45. 0045apply add_comm
  46. 0046rewrite hk_comm
  47. 0047have hk_assoc_two : 5 * 10 + (5 * 26 + 24) = (5 * 10 + 5 * 26) + 24
  48. 0048symm
  49. 0049specialize add_assoc (5 * 10)
  50. 0050specialize add_assoc (5 * 26)
  51. 0051specialize add_assoc 24
  52. 0052apply add_assoc
  53. 0053rewrite hk_assoc_two
  54. 0054have hk_factor : 5 * (10 + 26) = 5 * 10 + 5 * 26
  55. 0055specialize mul_add 5
  56. 0056specialize mul_add 10
  57. 0057specialize mul_add 26
  58. 0058apply mul_add
  59. 0059rewrite <- hk_factor
  60. 0060have hk_root : 10 + 26 = 36
  61. 0061norm_num
  62. 0062rewrite hk_root
  63. 0063refl
  64. 0064have hd_bridge : 6 * 24 = 4 * 36
  65. 0065have hd_twenty_four : 24 = 4 * 6
  66. 0066norm_num
  67. 0067rewrite hd_twenty_four
  68. 0068trans (6 * 4) * 6
  69. 0069symm
  70. 0070specialize mul_assoc 6
  71. 0071specialize mul_assoc 4
  72. 0072specialize mul_assoc 6
  73. 0073apply mul_assoc
  74. 0074trans (4 * 6) * 6
  75. 0075congr
  76. 0076specialize mul_comm 6
  77. 0077specialize mul_comm 4
  78. 0078apply mul_comm
  79. 0079refl
  80. 0080trans 4 * (6 * 6)
  81. 0081specialize mul_assoc 4
  82. 0082specialize mul_assoc 6
  83. 0083specialize mul_assoc 6
  84. 0084apply mul_assoc
  85. 0085have hd_thirty_six : 36 = 6 * 6
  86. 0086norm_num
  87. 0087rewrite <- hd_thirty_six
  88. 0088refl
  89. 0089rewrite hd_bridge
  90. 0090have hd_factor : (2 + 4) * 36 = 2 * 36 + 4 * 36
  91. 0091specialize add_mul 2
  92. 0092specialize add_mul 4
  93. 0093specialize add_mul 36
  94. 0094apply add_mul
  95. 0095rewrite <- hd_factor
  96. 0096have hd_six : 2 + 4 = 6
  97. 0097norm_num
  98. 0098rewrite hd_six
  99. 0099refl