BT00W9 · Bertrand theorem

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.

Statement with defined notation

Le(6 · (13 · 13 + 8),33 · 33)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-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)

Proof neighborhood

Direct theorem prerequisites

BT00W7 linear_square_budget BT000B add_mul BT0007 mul_add BT0003 add_assoc

Direct theorem dependents

BT00WQ bertrand_h_root_33_from_total

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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