BT00WA · Bertrand theorem

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.

Statement with defined notation

Le(6 · (13 · 14),34 · 34)

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_34. bqb_le_gap_hj32_scaled_budget_root_34 + (6 * (13 * 14)) = (34 * 34)

Proof neighborhood

Direct theorem prerequisites

BT00W7 linear_square_budget BT000B add_mul BT0007 mul_add BT0003 add_assoc

Direct theorem dependents

BT00WR bertrand_h_root_34_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 · 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.

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