BT00WB · Bertrand theorem

bertrand_scaled_budget_root_35

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

The factorized RFC-v1 H budget at root 35 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 + 6),35 · 35)

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_35. bqb_le_gap_hj32_scaled_budget_root_35 + (6 * (13 * 14 + 6)) = (35 * 35)

Proof neighborhood

Direct theorem prerequisites

BT00W7 linear_square_budget BT0007 mul_add BT000B add_mul BT0003 add_assoc

Direct theorem dependents

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

86 script commands · 18 reading checkpoints · 15 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 budgetmul addadd muladd 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 35
  4. L4
    specialize linear_square_budget 5
  5. L5
    specialize linear_square_budget 13
  6. L6
    specialize linear_square_budget (13 * 14 + 6)
  7. L7
    specialize linear_square_budget (2 * 35 + 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 * 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_assoc_oneL22–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_one : 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_one
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_thirty_fourL35–37

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

  1. L35
    have hk_thirty_four : 14 + 20 = 34
  2. L36
    norm_num
  3. L37
    rewrite hk_thirty_four
09Establish hk_assoc_twoL38–43

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

  1. L38
    have hk_assoc_two : (5 * 34 + 12) + 6 = 5 * 34 + (12 + 6)
  2. L39
    specialize add_assoc (5 * 34)
  3. L40
    specialize add_assoc 12
  4. L41
    specialize add_assoc 6
  5. L42
    apply add_assoc
  6. L43
    rewrite hk_assoc_two
10Establish hk_remainderL44–46

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

  1. L44
    have hk_remainder : 12 + 6 = 5 + 13
  2. L45
    norm_num
  3. L46
    rewrite hk_remainder
11Establish hk_assoc_threeL47–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_three : 5 * 34 + (5 + 13) = (5 * 34 + 5) + 13
  2. L48
    symm
  3. L49
    specialize add_assoc (5 * 34)
  4. L50
    specialize add_assoc 5
  5. L51
    specialize add_assoc 13
  6. L52
    apply add_assoc
  7. L53
    rewrite hk_assoc_three
12Establish hk_stepL54–54

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

  1. L54
    have hk_step : 5 * 35 = 5 * 34 + 5
13Establish hk_thirty_fiveL55–64

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

  1. L55
    have hk_thirty_five : 35 = 34 + 1
  2. L56
    norm_num
  3. L57
    rewrite hk_thirty_five
  4. L58
    trans 5 * 34 + 5 * 1
  5. L59
    specialize mul_add 5
  6. L60
    specialize mul_add 34
  7. L61
    specialize mul_add 1
  8. L62
    apply mul_add
  9. L63
    congr
  10. L64
    refl
14Calculate and transport equalitiesL65–67

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

  1. L65
    norm_num
  2. L66
    rewrite <- hk_step
  3. L67
    refl
15Establish hd_assocL68–73

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

  1. L68
    have hd_assoc : (2 * 35 + 27) + 6 * 13 = 2 * 35 + (27 + 6 * 13)
  2. L69
    specialize add_assoc (2 * 35)
  3. L70
    specialize add_assoc 27
  4. L71
    specialize add_assoc (6 * 13)
  5. L72
    apply add_assoc
  6. L73
    rewrite hd_assoc
16Establish hd_bridgeL74–76

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

  1. L74
    have hd_bridge : 27 + 6 * 13 = 3 * 35
  2. L75
    norm_num
  3. L76
    rewrite hd_bridge
17Establish hd_factorL77–82

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

  1. L77
    have hd_factor : (2 + 3) * 35 = 2 * 35 + 3 * 35
  2. L78
    specialize add_mul 2
  3. L79
    specialize add_mul 3
  4. L80
    specialize add_mul 35
  5. L81
    apply add_mul
  6. L82
    rewrite <- hd_factor
18Establish hd_fiveL83–86

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

  1. L83
    have hd_five : 2 + 3 = 5
  2. L84
    norm_num
  3. L85
    rewrite hd_five
  4. L86
    refl

Library-wide reading audit

Original defined command ledger · 86 lines
  1. 0001specialize linear_square_budget 6
  2. 0002specialize linear_square_budget 5
  3. 0003specialize linear_square_budget 35
  4. 0004specialize linear_square_budget 5
  5. 0005specialize linear_square_budget 13
  6. 0006specialize linear_square_budget (13 * 14 + 6)
  7. 0007specialize linear_square_budget (2 * 35 + 27)
  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_one : 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_one
  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_thirty_four : 14 + 20 = 34
  36. 0036norm_num
  37. 0037rewrite hk_thirty_four
  38. 0038have hk_assoc_two : (5 * 34 + 12) + 6 = 5 * 34 + (12 + 6)
  39. 0039specialize add_assoc (5 * 34)
  40. 0040specialize add_assoc 12
  41. 0041specialize add_assoc 6
  42. 0042apply add_assoc
  43. 0043rewrite hk_assoc_two
  44. 0044have hk_remainder : 12 + 6 = 5 + 13
  45. 0045norm_num
  46. 0046rewrite hk_remainder
  47. 0047have hk_assoc_three : 5 * 34 + (5 + 13) = (5 * 34 + 5) + 13
  48. 0048symm
  49. 0049specialize add_assoc (5 * 34)
  50. 0050specialize add_assoc 5
  51. 0051specialize add_assoc 13
  52. 0052apply add_assoc
  53. 0053rewrite hk_assoc_three
  54. 0054have hk_step : 5 * 35 = 5 * 34 + 5
  55. 0055have hk_thirty_five : 35 = 34 + 1
  56. 0056norm_num
  57. 0057rewrite hk_thirty_five
  58. 0058trans 5 * 34 + 5 * 1
  59. 0059specialize mul_add 5
  60. 0060specialize mul_add 34
  61. 0061specialize mul_add 1
  62. 0062apply mul_add
  63. 0063congr
  64. 0064refl
  65. 0065norm_num
  66. 0066rewrite <- hk_step
  67. 0067refl
  68. 0068have hd_assoc : (2 * 35 + 27) + 6 * 13 = 2 * 35 + (27 + 6 * 13)
  69. 0069specialize add_assoc (2 * 35)
  70. 0070specialize add_assoc 27
  71. 0071specialize add_assoc (6 * 13)
  72. 0072apply add_assoc
  73. 0073rewrite hd_assoc
  74. 0074have hd_bridge : 27 + 6 * 13 = 3 * 35
  75. 0075norm_num
  76. 0076rewrite hd_bridge
  77. 0077have hd_factor : (2 + 3) * 35 = 2 * 35 + 3 * 35
  78. 0078specialize add_mul 2
  79. 0079specialize add_mul 3
  80. 0080specialize add_mul 35
  81. 0081apply add_mul
  82. 0082rewrite <- hd_factor
  83. 0083have hd_five : 2 + 3 = 5
  84. 0084norm_num
  85. 0085rewrite hd_five
  86. 0086refl