BT00WA

bertrand_scaled_budget_root_34

Alpha body-checked · checked-use disabled

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

Exact expanded PA statement

exists bqb_le_gap_hj32_scaled_budget_root_34. bqb_le_gap_hj32_scaled_budget_root_34 + (6 * (13 * 14)) = (34 * 34)

Structural proof guide

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

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

Proof neighborhood

Direct dependencies

BT00W7 linear_square_budget BT000B add_mul BT0007 mul_add BT0003 add_assoc

Direct dependents

BT00WR bertrand_h_root_34_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 34
  4. 0004specialize linear_square_budget 4
  5. 0005specialize linear_square_budget 12
  6. 0006specialize linear_square_budget (13 * 14)
  7. 0007specialize linear_square_budget (2 * 32)
  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 : 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
  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_root : 14 + 20 = 34
  36. 0036norm_num
  37. 0037rewrite hk_root
  38. 0038refl
  39. 0039have hd_left : 2 * 32 = 4 * 16
  40. 0040norm_num
  41. 0041rewrite hd_left
  42. 0042have hd_right : 6 * 12 = 4 * 18
  43. 0043norm_num
  44. 0044rewrite hd_right
  45. 0045have hd_factor : 4 * (16 + 18) = 4 * 16 + 4 * 18
  46. 0046specialize mul_add 4
  47. 0047specialize mul_add 16
  48. 0048specialize mul_add 18
  49. 0049apply mul_add
  50. 0050rewrite <- hd_factor
  51. 0051have hd_root : 16 + 18 = 34
  52. 0052norm_num
  53. 0053rewrite hd_root
  54. 0054refl