BT00WA

bertrand_scaled_budget_root_34

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

The factorized RFC-v1 H budget at root 34 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_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 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 · 12 reading checkpoints · 10 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 34
  4. L4
    specialize linear_square_budget 4
  5. L5
    specialize linear_square_budget 12
  6. L6
    specialize linear_square_budget (13 * 14)
  7. L7
    specialize linear_square_budget (2 * 32)
  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 * 14 = 5 * 14 + 8 * 14
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 = 5 + 8
  2. L12
    norm_num
  3. L13
    rewrite hk_thirteen
  4. L14
    specialize add_mul 5
  5. L15
    specialize add_mul 8
  6. L16
    specialize add_mul 14
  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 : 8 * 14 = 5 * 20 + 12
  2. L20
    norm_num
  3. L21
    rewrite hk_bridge
06Establish hk_assocL22–28

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 : 5 * 14 + (5 * 20 + 12) = (5 * 14 + 5 * 20) + 12
  2. L23
    symm
  3. L24
    specialize add_assoc (5 * 14)
  4. L25
    specialize add_assoc (5 * 20)
  5. L26
    specialize add_assoc 12
  6. L27
    apply add_assoc
  7. L28
    rewrite hk_assoc
07Establish hk_factorL29–34

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

  1. L29
    have hk_factor : 5 * (14 + 20) = 5 * 14 + 5 * 20
  2. L30
    specialize mul_add 5
  3. L31
    specialize mul_add 14
  4. L32
    specialize mul_add 20
  5. L33
    apply mul_add
  6. L34
    rewrite <- hk_factor
08Establish hk_rootL35–38

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

  1. L35
    have hk_root : 14 + 20 = 34
  2. L36
    norm_num
  3. L37
    rewrite hk_root
  4. L38
    refl
09Establish hd_leftL39–41

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

  1. L39
    have hd_left : 2 * 32 = 4 * 16
  2. L40
    norm_num
  3. L41
    rewrite hd_left
10Establish hd_rightL42–44

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

  1. L42
    have hd_right : 6 * 12 = 4 * 18
  2. L43
    norm_num
  3. L44
    rewrite hd_right
11Establish hd_factorL45–50

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

  1. L45
    have hd_factor : 4 * (16 + 18) = 4 * 16 + 4 * 18
  2. L46
    specialize mul_add 4
  3. L47
    specialize mul_add 16
  4. L48
    specialize mul_add 18
  5. L49
    apply mul_add
  6. L50
    rewrite <- hd_factor
12Establish hd_rootL51–54

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

  1. L51
    have hd_root : 16 + 18 = 34
  2. L52
    norm_num
  3. L53
    rewrite hd_root
  4. L54
    refl

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 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