BT00W9

bertrand_scaled_budget_root_33

Alpha body-checked · checked-use disabled

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

Exact expanded PA statement

exists bqb_le_gap_hj32_scaled_budget_root_33. bqb_le_gap_hj32_scaled_budget_root_33 + (6 * (13 * 13 + 8)) = (33 * 33)

Structural proof guide

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

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

Proof neighborhood

Direct dependencies

BT00W7 linear_square_budget BT000B add_mul BT0007 mul_add BT0003 add_assoc

Direct dependents

BT00WQ bertrand_h_root_33_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 33
  4. 0004specialize linear_square_budget 3
  5. 0005specialize linear_square_budget 12
  6. 0006specialize linear_square_budget (13 * 13 + 8)
  7. 0007specialize linear_square_budget (27)
  8. 0008apply linear_square_budget
  9. 0009norm_num
  10. 0010have hk_split : 13 * 13 = 9 * 13 + 4 * 13
  11. 0011have hk_thirteen : 13 = 9 + 4
  12. 0012norm_num
  13. 0013rewrite hk_thirteen
  14. 0014specialize add_mul 9
  15. 0015specialize add_mul 4
  16. 0016specialize add_mul 13
  17. 0017apply add_mul
  18. 0018rewrite hk_split
  19. 0019have hk_bridge : 9 * 13 = 5 * 21 + 12
  20. 0020norm_num
  21. 0021rewrite hk_bridge
  22. 0022have hk_assoc_one : (5 * 21 + 12) + 4 * 13 = 5 * 21 + (12 + 4 * 13)
  23. 0023specialize add_assoc (5 * 21)
  24. 0024specialize add_assoc 12
  25. 0025specialize add_assoc (4 * 13)
  26. 0026apply add_assoc
  27. 0027rewrite hk_assoc_one
  28. 0028have hk_assoc_two : (5 * 21 + (12 + 4 * 13)) + 8 = 5 * 21 + ((12 + 4 * 13) + 8)
  29. 0029specialize add_assoc (5 * 21)
  30. 0030specialize add_assoc (12 + 4 * 13)
  31. 0031specialize add_assoc 8
  32. 0032apply add_assoc
  33. 0033rewrite hk_assoc_two
  34. 0034have hk_remainder : (12 + 4 * 13) + 8 = 5 * 12 + 12
  35. 0035norm_num
  36. 0036rewrite hk_remainder
  37. 0037have hk_assoc_three : 5 * 21 + (5 * 12 + 12) = (5 * 21 + 5 * 12) + 12
  38. 0038symm
  39. 0039specialize add_assoc (5 * 21)
  40. 0040specialize add_assoc (5 * 12)
  41. 0041specialize add_assoc 12
  42. 0042apply add_assoc
  43. 0043rewrite hk_assoc_three
  44. 0044have hk_factor : 5 * (21 + 12) = 5 * 21 + 5 * 12
  45. 0045specialize mul_add 5
  46. 0046specialize mul_add 21
  47. 0047specialize mul_add 12
  48. 0048apply mul_add
  49. 0049rewrite <- hk_factor
  50. 0050have hk_root : 21 + 12 = 33
  51. 0051norm_num
  52. 0052rewrite hk_root
  53. 0053refl
  54. 0054norm_num