BT00WB

bertrand_scaled_budget_root_35

Alpha body-checked · checked-use disabled

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

Exact expanded PA statement

exists bqb_le_gap_hj32_scaled_budget_root_35. bqb_le_gap_hj32_scaled_budget_root_35 + (6 * (13 * 14 + 6)) = (35 * 35)

Structural proof guide

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

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

Proof neighborhood

Direct dependencies

BT00W7 linear_square_budget BT0007 mul_add BT000B add_mul BT0003 add_assoc

Direct dependents

BT00WS bertrand_h_root_35_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 35
  4. 0004specialize linear_square_budget 5
  5. 0005specialize linear_square_budget 13
  6. 0006specialize linear_square_budget (13 * 14 + 6)
  7. 0007specialize linear_square_budget (2 * 35 + 27)
  8. 0008apply linear_square_budget
  9. 0009norm_num
  10. 0010have hk_split : 13 * 14 = 5 * 14 + 8 * 14
  11. 0011have hk_thirteen : 13 = 5 + 8
  12. 0012norm_num
  13. 0013rewrite hk_thirteen
  14. 0014specialize add_mul 5
  15. 0015specialize add_mul 8
  16. 0016specialize add_mul 14
  17. 0017apply add_mul
  18. 0018rewrite hk_split
  19. 0019have hk_bridge : 8 * 14 = 5 * 20 + 12
  20. 0020norm_num
  21. 0021rewrite hk_bridge
  22. 0022have hk_assoc_one : 5 * 14 + (5 * 20 + 12) = (5 * 14 + 5 * 20) + 12
  23. 0023symm
  24. 0024specialize add_assoc (5 * 14)
  25. 0025specialize add_assoc (5 * 20)
  26. 0026specialize add_assoc 12
  27. 0027apply add_assoc
  28. 0028rewrite hk_assoc_one
  29. 0029have hk_factor : 5 * (14 + 20) = 5 * 14 + 5 * 20
  30. 0030specialize mul_add 5
  31. 0031specialize mul_add 14
  32. 0032specialize mul_add 20
  33. 0033apply mul_add
  34. 0034rewrite <- hk_factor
  35. 0035have hk_thirty_four : 14 + 20 = 34
  36. 0036norm_num
  37. 0037rewrite hk_thirty_four
  38. 0038have hk_assoc_two : (5 * 34 + 12) + 6 = 5 * 34 + (12 + 6)
  39. 0039specialize add_assoc (5 * 34)
  40. 0040specialize add_assoc 12
  41. 0041specialize add_assoc 6
  42. 0042apply add_assoc
  43. 0043rewrite hk_assoc_two
  44. 0044have hk_remainder : 12 + 6 = 5 + 13
  45. 0045norm_num
  46. 0046rewrite hk_remainder
  47. 0047have hk_assoc_three : 5 * 34 + (5 + 13) = (5 * 34 + 5) + 13
  48. 0048symm
  49. 0049specialize add_assoc (5 * 34)
  50. 0050specialize add_assoc 5
  51. 0051specialize add_assoc 13
  52. 0052apply add_assoc
  53. 0053rewrite hk_assoc_three
  54. 0054have hk_step : 5 * 35 = 5 * 34 + 5
  55. 0055have hk_thirty_five : 35 = 34 + 1
  56. 0056norm_num
  57. 0057rewrite hk_thirty_five
  58. 0058trans 5 * 34 + 5 * 1
  59. 0059specialize mul_add 5
  60. 0060specialize mul_add 34
  61. 0061specialize mul_add 1
  62. 0062apply mul_add
  63. 0063congr
  64. 0064refl
  65. 0065norm_num
  66. 0066rewrite <- hk_step
  67. 0067refl
  68. 0068have hd_assoc : (2 * 35 + 27) + 6 * 13 = 2 * 35 + (27 + 6 * 13)
  69. 0069specialize add_assoc (2 * 35)
  70. 0070specialize add_assoc 27
  71. 0071specialize add_assoc (6 * 13)
  72. 0072apply add_assoc
  73. 0073rewrite hd_assoc
  74. 0074have hd_bridge : 27 + 6 * 13 = 3 * 35
  75. 0075norm_num
  76. 0076rewrite hd_bridge
  77. 0077have hd_factor : (2 + 3) * 35 = 2 * 35 + 3 * 35
  78. 0078specialize add_mul 2
  79. 0079specialize add_mul 3
  80. 0080specialize add_mul 35
  81. 0081apply add_mul
  82. 0082rewrite <- hd_factor
  83. 0083have hd_five : 2 + 3 = 5
  84. 0084norm_num
  85. 0085rewrite hd_five
  86. 0086refl