BT00W9

bertrand_scaled_budget_root_33

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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 the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

54 script commands · 11 reading checkpoints · 9 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (4)
linear square budgetadd mulmul addadd assoc
01Use earlier factsL1–8

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L1
    specialize linear_square_budget 6
  2. L2
    specialize linear_square_budget 5
  3. L3
    specialize linear_square_budget 33
  4. L4
    specialize linear_square_budget 3
  5. L5
    specialize linear_square_budget 12
  6. L6
    specialize linear_square_budget (13 * 13 + 8)
  7. L7
    specialize linear_square_budget (27)
  8. L8
    apply linear_square_budget
02Calculate and transport equalitiesL9–9

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L9
    norm_num
03Establish hk_splitL10–10

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have hk_split : 13 * 13 = 9 * 13 + 4 * 13
04Establish hk_thirteenL11–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add mul.

  1. L11
    have hk_thirteen : 13 = 9 + 4
  2. L12
    norm_num
  3. L13
    rewrite hk_thirteen
  4. L14
    specialize add_mul 9
  5. L15
    specialize add_mul 4
  6. L16
    specialize add_mul 13
  7. L17
    apply add_mul
  8. L18
    rewrite hk_split
05Establish hk_bridgeL19–21

Establish this local claim before using it. It is not an additional assumption.

  1. L19
    have hk_bridge : 9 * 13 = 5 * 21 + 12
  2. L20
    norm_num
  3. L21
    rewrite hk_bridge
06Establish hk_assoc_oneL22–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add assoc.

  1. L22
    have hk_assoc_one : (5 * 21 + 12) + 4 * 13 = 5 * 21 + (12 + 4 * 13)
  2. L23
    specialize add_assoc (5 * 21)
  3. L24
    specialize add_assoc 12
  4. L25
    specialize add_assoc (4 * 13)
  5. L26
    apply add_assoc
  6. L27
    rewrite hk_assoc_one
07Establish hk_assoc_twoL28–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add assoc.

  1. L28
    have hk_assoc_two : (5 * 21 + (12 + 4 * 13)) + 8 = 5 * 21 + ((12 + 4 * 13) + 8)
  2. L29
    specialize add_assoc (5 * 21)
  3. L30
    specialize add_assoc (12 + 4 * 13)
  4. L31
    specialize add_assoc 8
  5. L32
    apply add_assoc
  6. L33
    rewrite hk_assoc_two
08Establish hk_remainderL34–36

Establish this local claim before using it. It is not an additional assumption.

  1. L34
    have hk_remainder : (12 + 4 * 13) + 8 = 5 * 12 + 12
  2. L35
    norm_num
  3. L36
    rewrite hk_remainder
09Establish hk_assoc_threeL37–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add assoc.

  1. L37
    have hk_assoc_three : 5 * 21 + (5 * 12 + 12) = (5 * 21 + 5 * 12) + 12
  2. L38
    symm
  3. L39
    specialize add_assoc (5 * 21)
  4. L40
    specialize add_assoc (5 * 12)
  5. L41
    specialize add_assoc 12
  6. L42
    apply add_assoc
  7. L43
    rewrite hk_assoc_three
10Establish hk_factorL44–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul add.

  1. L44
    have hk_factor : 5 * (21 + 12) = 5 * 21 + 5 * 12
  2. L45
    specialize mul_add 5
  3. L46
    specialize mul_add 21
  4. L47
    specialize mul_add 12
  5. L48
    apply mul_add
  6. L49
    rewrite <- hk_factor
11Establish hk_rootL50–54

Establish this local claim before using it. It is not an additional assumption.

  1. L50
    have hk_root : 21 + 12 = 33
  2. L51
    norm_num
  3. L52
    rewrite hk_root
  4. L53
    refl
  5. L54
    norm_num

Library-wide reading audit

Original exact command ledger · 54 lines
  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