BT00WC · Bertrand theorem

bertrand_scaled_budget_root_36

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

The factorized RFC-v1 H budget at root 36 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 · (2 · 37 + 2 · (5 · 13)),36 · 36)

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_36. bqb_le_gap_hj32_scaled_budget_root_36 + (6 * (2 * 37 + 2 * (5 * 13))) = (36 * 36)

Proof neighborhood

Direct theorem prerequisites

BT00W7 linear_square_budget BT0007 mul_add BT0008 mul_assoc BT0006 mul_comm BT000B add_mul BT0003 add_assoc BT0002 add_comm

Direct theorem dependents

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

99 script commands · 22 reading checkpoints · 13 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 (7)
linear square budgetmul addmul assocmul commadd muladd assocadd comm
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 36
  4. L4
    specialize linear_square_budget 6
  5. L5
    specialize linear_square_budget 24
  6. L6
    specialize linear_square_budget (2 * 37 + 2 * (5 * 13))
  7. L7
    specialize linear_square_budget (2 * 36)
  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_firstL10–12

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

  1. L10
    have hk_first : 2 * 37 = 5 * 10 + 24
  2. L11
    norm_num
  3. L12
    rewrite hk_first
04Establish hk_secondL13–22

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

  1. L13
    have hk_second : 2 * (5 * 13) = 5 * 26
  2. L14
    trans (2 * 5) * 13
  3. L15
    symm
  4. L16
    specialize mul_assoc 2
  5. L17
    specialize mul_assoc 5
  6. L18
    specialize mul_assoc 13
  7. L19
    apply mul_assoc
  8. L20
    trans (5 * 2) * 13
  9. L21
    congr
  10. L22
    specialize mul_comm 2
05Use earlier factsL23–24

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

  1. L23
    specialize mul_comm 5
  2. L24
    apply mul_comm
06Calculate and transport equalitiesL25–26

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

  1. L25
    refl
  2. L26
    trans 5 * (2 * 13)
07Use earlier factsL27–30

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

  1. L27
    specialize mul_assoc 5
  2. L28
    specialize mul_assoc 2
  3. L29
    specialize mul_assoc 13
  4. L30
    apply mul_assoc
08Establish hk_twenty_sixL31–35

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

  1. L31
    have hk_twenty_six : 2 * 13 = 26
  2. L32
    norm_num
  3. L33
    rewrite hk_twenty_six
  4. L34
    refl
  5. L35
    rewrite hk_second
09Establish hk_assoc_oneL36–41

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

  1. L36
    have hk_assoc_one : (5 * 10 + 24) + 5 * 26 = 5 * 10 + (24 + 5 * 26)
  2. L37
    specialize add_assoc (5 * 10)
  3. L38
    specialize add_assoc 24
  4. L39
    specialize add_assoc (5 * 26)
  5. L40
    apply add_assoc
  6. L41
    rewrite hk_assoc_one
10Establish hk_commL42–46

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

  1. L42
    have hk_comm : 24 + 5 * 26 = 5 * 26 + 24
  2. L43
    specialize add_comm 24
  3. L44
    specialize add_comm (5 * 26)
  4. L45
    apply add_comm
  5. L46
    rewrite hk_comm
11Establish hk_assoc_twoL47–53

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

  1. L47
    have hk_assoc_two : 5 * 10 + (5 * 26 + 24) = (5 * 10 + 5 * 26) + 24
  2. L48
    symm
  3. L49
    specialize add_assoc (5 * 10)
  4. L50
    specialize add_assoc (5 * 26)
  5. L51
    specialize add_assoc 24
  6. L52
    apply add_assoc
  7. L53
    rewrite hk_assoc_two
12Establish hk_factorL54–59

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

  1. L54
    have hk_factor : 5 * (10 + 26) = 5 * 10 + 5 * 26
  2. L55
    specialize mul_add 5
  3. L56
    specialize mul_add 10
  4. L57
    specialize mul_add 26
  5. L58
    apply mul_add
  6. L59
    rewrite <- hk_factor
13Establish hk_rootL60–63

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

  1. L60
    have hk_root : 10 + 26 = 36
  2. L61
    norm_num
  3. L62
    rewrite hk_root
  4. L63
    refl
14Establish hd_bridgeL64–64

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

  1. L64
    have hd_bridge : 6 * 24 = 4 * 36
15Establish hd_twenty_fourL65–74

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

  1. L65
    have hd_twenty_four : 24 = 4 * 6
  2. L66
    norm_num
  3. L67
    rewrite hd_twenty_four
  4. L68
    trans (6 * 4) * 6
  5. L69
    symm
  6. L70
    specialize mul_assoc 6
  7. L71
    specialize mul_assoc 4
  8. L72
    specialize mul_assoc 6
  9. L73
    apply mul_assoc
  10. L74
    trans (4 * 6) * 6
16Calculate and transport equalitiesL75–75

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

  1. L75
    congr
17Use earlier factsL76–78

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

  1. L76
    specialize mul_comm 6
  2. L77
    specialize mul_comm 4
  3. L78
    apply mul_comm
18Calculate and transport equalitiesL79–80

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

  1. L79
    refl
  2. L80
    trans 4 * (6 * 6)
19Use earlier factsL81–84

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

  1. L81
    specialize mul_assoc 4
  2. L82
    specialize mul_assoc 6
  3. L83
    specialize mul_assoc 6
  4. L84
    apply mul_assoc
20Establish hd_thirty_sixL85–89

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

  1. L85
    have hd_thirty_six : 36 = 6 * 6
  2. L86
    norm_num
  3. L87
    rewrite <- hd_thirty_six
  4. L88
    refl
  5. L89
    rewrite hd_bridge
21Establish hd_factorL90–95

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

  1. L90
    have hd_factor : (2 + 4) * 36 = 2 * 36 + 4 * 36
  2. L91
    specialize add_mul 2
  3. L92
    specialize add_mul 4
  4. L93
    specialize add_mul 36
  5. L94
    apply add_mul
  6. L95
    rewrite <- hd_factor
22Establish hd_sixL96–99

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

  1. L96
    have hd_six : 2 + 4 = 6
  2. L97
    norm_num
  3. L98
    rewrite hd_six
  4. L99
    refl

Library-wide reading audit

Original defined command ledger · 99 lines
  1. 0001specialize linear_square_budget 6
  2. 0002specialize linear_square_budget 5
  3. 0003specialize linear_square_budget 36
  4. 0004specialize linear_square_budget 6
  5. 0005specialize linear_square_budget 24
  6. 0006specialize linear_square_budget (2 * 37 + 2 * (5 * 13))
  7. 0007specialize linear_square_budget (2 * 36)
  8. 0008apply linear_square_budget
  9. 0009norm_num
  10. 0010have hk_first : 2 * 37 = 5 * 10 + 24
  11. 0011norm_num
  12. 0012rewrite hk_first
  13. 0013have hk_second : 2 * (5 * 13) = 5 * 26
  14. 0014trans (2 * 5) * 13
  15. 0015symm
  16. 0016specialize mul_assoc 2
  17. 0017specialize mul_assoc 5
  18. 0018specialize mul_assoc 13
  19. 0019apply mul_assoc
  20. 0020trans (5 * 2) * 13
  21. 0021congr
  22. 0022specialize mul_comm 2
  23. 0023specialize mul_comm 5
  24. 0024apply mul_comm
  25. 0025refl
  26. 0026trans 5 * (2 * 13)
  27. 0027specialize mul_assoc 5
  28. 0028specialize mul_assoc 2
  29. 0029specialize mul_assoc 13
  30. 0030apply mul_assoc
  31. 0031have hk_twenty_six : 2 * 13 = 26
  32. 0032norm_num
  33. 0033rewrite hk_twenty_six
  34. 0034refl
  35. 0035rewrite hk_second
  36. 0036have hk_assoc_one : (5 * 10 + 24) + 5 * 26 = 5 * 10 + (24 + 5 * 26)
  37. 0037specialize add_assoc (5 * 10)
  38. 0038specialize add_assoc 24
  39. 0039specialize add_assoc (5 * 26)
  40. 0040apply add_assoc
  41. 0041rewrite hk_assoc_one
  42. 0042have hk_comm : 24 + 5 * 26 = 5 * 26 + 24
  43. 0043specialize add_comm 24
  44. 0044specialize add_comm (5 * 26)
  45. 0045apply add_comm
  46. 0046rewrite hk_comm
  47. 0047have hk_assoc_two : 5 * 10 + (5 * 26 + 24) = (5 * 10 + 5 * 26) + 24
  48. 0048symm
  49. 0049specialize add_assoc (5 * 10)
  50. 0050specialize add_assoc (5 * 26)
  51. 0051specialize add_assoc 24
  52. 0052apply add_assoc
  53. 0053rewrite hk_assoc_two
  54. 0054have hk_factor : 5 * (10 + 26) = 5 * 10 + 5 * 26
  55. 0055specialize mul_add 5
  56. 0056specialize mul_add 10
  57. 0057specialize mul_add 26
  58. 0058apply mul_add
  59. 0059rewrite <- hk_factor
  60. 0060have hk_root : 10 + 26 = 36
  61. 0061norm_num
  62. 0062rewrite hk_root
  63. 0063refl
  64. 0064have hd_bridge : 6 * 24 = 4 * 36
  65. 0065have hd_twenty_four : 24 = 4 * 6
  66. 0066norm_num
  67. 0067rewrite hd_twenty_four
  68. 0068trans (6 * 4) * 6
  69. 0069symm
  70. 0070specialize mul_assoc 6
  71. 0071specialize mul_assoc 4
  72. 0072specialize mul_assoc 6
  73. 0073apply mul_assoc
  74. 0074trans (4 * 6) * 6
  75. 0075congr
  76. 0076specialize mul_comm 6
  77. 0077specialize mul_comm 4
  78. 0078apply mul_comm
  79. 0079refl
  80. 0080trans 4 * (6 * 6)
  81. 0081specialize mul_assoc 4
  82. 0082specialize mul_assoc 6
  83. 0083specialize mul_assoc 6
  84. 0084apply mul_assoc
  85. 0085have hd_thirty_six : 36 = 6 * 6
  86. 0086norm_num
  87. 0087rewrite <- hd_thirty_six
  88. 0088refl
  89. 0089rewrite hd_bridge
  90. 0090have hd_factor : (2 + 4) * 36 = 2 * 36 + 4 * 36
  91. 0091specialize add_mul 2
  92. 0092specialize add_mul 4
  93. 0093specialize add_mul 36
  94. 0094apply add_mul
  95. 0095rewrite <- hd_factor
  96. 0096have hd_six : 2 + 4 = 6
  97. 0097norm_num
  98. 0098rewrite hd_six
  99. 0099refl