BT00W8

bertrand_scaled_budget_root_32

Alpha body-checked · checked-use disabled

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

Exact expanded PA statement

exists bqb_le_gap_hj32_scaled_budget_root_32. bqb_le_gap_hj32_scaled_budget_root_32 + (6 * ((4 * 13 + 1) + 4 * 29)) = (32 * 32)

Structural proof guide

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

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

Proof neighborhood

Direct dependencies

BT00W7 linear_square_budget BT0007 mul_add BT0003 add_assoc BT0002 add_comm

Direct dependents

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