BT00VK · Bertrand theorem

central_binom_strong_upper_step

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

The weighted recurrence preserves the strong factor-two bound.

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

∀ n. ∀ c. ∀ d. ∀ q. ∀ r. Le(2 · c,q) → S n · d = 2 · S (n + n) · c → r = q · 4 → Le(2 · d,r)

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

2 occurrences

In local proof propositions

PD0001 Le

4 occurrences

Exact expanded native-PA statement
forall n c d q r. (exists bcf_le_gap_bcbsus_source. bcf_le_gap_bcbsus_source + (2 * c) = q) -> S n * d = (2 * S (n + n)) * c -> r = q * 4 -> (exists bcf_le_gap_bcbsus_result. bcf_le_gap_bcbsus_result + (2 * d) = r)

Proof neighborhood

Direct theorem prerequisites

BT0000 zero_add BT0001 add_succ_left BT0003 add_assoc BT0006 mul_comm BT0008 mul_assoc BT00QU two_mul_eq_add_self BT001L mul_le_mul_left BT001M mul_le_mul_right BT000F le_trans BT000C succ_ne_zero BT00RD mul_le_cancel_left_nonzero

Direct theorem dependents

BT00VM central_binom_strong_upper_of_laws

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

94 script commands · 21 reading checkpoints · 11 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 (11)
zero addadd succ leftadd assocmul commmul assoctwo mul eq add selfmul le mul leftmul le mul rightle transsucc ne zeromul le cancel left nonzero
01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro q
  5. L5
    intro r
  6. L6
    intro hsource
  7. L7
    intro hrecurrence
  8. L8
    intro hpower_step
02Establish hsource_scaledL9–14

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

  1. L9
    have hsource_scaled : Le(S (n + n) · (2 · c),S (n + n) · q)Definitions: Le(S (n + n) · (2 · c),S (n + n) · q)Original native command in the exact edition
  2. L10
    specialize mul_le_mul_left (2 * c)
  3. L11
    specialize mul_le_mul_left q
  4. L12
    specialize mul_le_mul_left (S (n + n))
  5. L13
    apply mul_le_mul_left
  6. L14
    exact hsource
03Establish hcombinedL15–24

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

  1. L15
    have hcombined : Le(S (n + n) · (2 · c),2 · S n · q)Definitions: Le(S (n + n) · (2 · c),2 · S n · q)Original native command in the exact edition
  2. L16
    specialize le_trans (S (n + n) * (2 * c))
  3. L17
    specialize le_trans (S (n + n) * q)
  4. L18
    specialize le_trans ((2 * S n) * q)
  5. L19
    apply le_trans
  6. L20
    exact hsource_scaled
  7. L21
    specialize mul_le_mul_right (S (n + n))
  8. L22
    specialize mul_le_mul_right (2 * S n)
  9. L23
    specialize mul_le_mul_right q
  10. L24
    apply mul_le_mul_right
04Construct an explicit witnessL25–25

Supply the displayed value, then prove that it has the required property.

  1. L25
    exists 1
05Use earlier factsL26–26

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

  1. L26
    specialize two_mul_eq_add_self (S n)
06Calculate and transport equalitiesL27–29

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

  1. L27
    rewrite two_mul_eq_add_self
  2. L28
    rewrite PA4
  3. L29
    rewrite PA4
07Use earlier factsL30–32

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

  1. L30
    specialize add_assoc 1
  2. L31
    specialize add_assoc n
  3. L32
    specialize add_assoc n
08Calculate and transport equalitiesL33–33

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

  1. L33
    rewrite <- add_assoc
09Use earlier factsL34–35

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

  1. L34
    specialize add_succ_left 0
  2. L35
    specialize add_succ_left n
10Calculate and transport equalitiesL36–36

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

  1. L36
    rewrite add_succ_left
11Use earlier factsL37–37

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

  1. L37
    specialize zero_add n
12Calculate and transport equalitiesL38–39

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

  1. L38
    rewrite zero_add
  2. L39
    refl
13Establish hleft_alignL40–46

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

  1. L40
    have hleft_align : (2 * S (n + n)) * c = S (n + n) * (2 * c)
  2. L41
    trans 2 * (S (n + n) * c)
  3. L42
    apply mul_assoc
  4. L43
    trans (S (n + n) * c) * 2
  5. L44
    apply mul_comm
  6. L45
    trans S (n + n) * (c * 2)
  7. L46
    apply mul_assoc
14Establish hcomm_c_twoL47–50

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

  1. L47
    have hcomm_c_two : c * 2 = 2 * c
  2. L48
    apply mul_comm
  3. L49
    rewrite hcomm_c_two
  4. L50
    refl
15Establish hrecurrence_alignedL51–54

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

  1. L51
    have hrecurrence_aligned : S n * d = S (n + n) * (2 * c)
  2. L52
    trans (2 * S (n + n)) * c
  3. L53
    exact hrecurrence
  4. L54
    exact hleft_align
16Establish hright_alignL55–61

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

  1. L55
    have hright_align : (2 * S n) * q = S n * (2 * q)
  2. L56
    trans 2 * (S n * q)
  3. L57
    apply mul_assoc
  4. L58
    trans (S n * q) * 2
  5. L59
    apply mul_comm
  6. L60
    trans S n * (q * 2)
  7. L61
    apply mul_assoc
17Establish hcomm_q_twoL62–67

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

  1. L62
    have hcomm_q_two : q * 2 = 2 * q
  2. L63
    apply mul_comm
  3. L64
    rewrite hcomm_q_two
  4. L65
    refl
  5. L66
    rewrite <- hrecurrence_aligned at hcombined
  6. L67
    rewrite hright_align at hcombined
18Establish hhalfL68–75

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

  1. L68
    have hhalf : Le(d,2 · q)Definitions: Le(d,2 · q)Original native command in the exact edition
  2. L69
    specialize mul_le_cancel_left_nonzero (S n)
  3. L70
    specialize mul_le_cancel_left_nonzero d
  4. L71
    specialize mul_le_cancel_left_nonzero (2 * q)
  5. L72
    apply mul_le_cancel_left_nonzero
  6. L73
    specialize succ_ne_zero n
  7. L74
    exact succ_ne_zero
  8. L75
    exact hcombined
19Establish hdoubleL76–81

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

  1. L76
    have hdouble : Le(2 · d,2 · (2 · q))Definitions: Le(2 · d,2 · (2 · q))Original native command in the exact edition
  2. L77
    specialize mul_le_mul_left d
  3. L78
    specialize mul_le_mul_left (2 * q)
  4. L79
    specialize mul_le_mul_left 2
  5. L80
    apply mul_le_mul_left
  6. L81
    exact hhalf
20Establish hfourL82–86

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

  1. L82
    have hfour : 2 * (2 * q) = q * 4
  2. L83
    trans (2 * 2) * q
  3. L84
    symm
  4. L85
    apply mul_assoc
  5. L86
    trans 4 * q
21Establish htwo_twoL87–94

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

  1. L87
    have htwo_two : 2 * 2 = 4
  2. L88
    norm_num
  3. L89
    rewrite htwo_two
  4. L90
    refl
  5. L91
    apply mul_comm
  6. L92
    rewrite hfour at hdouble
  7. L93
    rewrite hpower_step
  8. L94
    exact hdouble

Library-wide reading audit

Original defined command ledger · 94 lines
  1. 0001intro n
  2. 0002intro c
  3. 0003intro d
  4. 0004intro q
  5. 0005intro r
  6. 0006intro hsource
  7. 0007intro hrecurrence
  8. 0008intro hpower_step
  9. 0009have hsource_scaled : Le(S (n + n) · (2 · c),S (n + n) · q)
    Exact native replay linehave hsource_scaled : exists k. k + S (n + n) * (2 * c) = S (n + n) * q
  10. 0010specialize mul_le_mul_left (2 * c)
  11. 0011specialize mul_le_mul_left q
  12. 0012specialize mul_le_mul_left (S (n + n))
  13. 0013apply mul_le_mul_left
  14. 0014exact hsource
  15. 0015have hcombined : Le(S (n + n) · (2 · c),2 · S n · q)
    Exact native replay linehave hcombined : exists k. k + S (n + n) * (2 * c) = (2 * S n) * q
  16. 0016specialize le_trans (S (n + n) * (2 * c))
  17. 0017specialize le_trans (S (n + n) * q)
  18. 0018specialize le_trans ((2 * S n) * q)
  19. 0019apply le_trans
  20. 0020exact hsource_scaled
  21. 0021specialize mul_le_mul_right (S (n + n))
  22. 0022specialize mul_le_mul_right (2 * S n)
  23. 0023specialize mul_le_mul_right q
  24. 0024apply mul_le_mul_right
  25. 0025exists 1
  26. 0026specialize two_mul_eq_add_self (S n)
  27. 0027rewrite two_mul_eq_add_self
  28. 0028rewrite PA4
  29. 0029rewrite PA4
  30. 0030specialize add_assoc 1
  31. 0031specialize add_assoc n
  32. 0032specialize add_assoc n
  33. 0033rewrite <- add_assoc
  34. 0034specialize add_succ_left 0
  35. 0035specialize add_succ_left n
  36. 0036rewrite add_succ_left
  37. 0037specialize zero_add n
  38. 0038rewrite zero_add
  39. 0039refl
  40. 0040have hleft_align : (2 * S (n + n)) * c = S (n + n) * (2 * c)
  41. 0041trans 2 * (S (n + n) * c)
  42. 0042apply mul_assoc
  43. 0043trans (S (n + n) * c) * 2
  44. 0044apply mul_comm
  45. 0045trans S (n + n) * (c * 2)
  46. 0046apply mul_assoc
  47. 0047have hcomm_c_two : c * 2 = 2 * c
  48. 0048apply mul_comm
  49. 0049rewrite hcomm_c_two
  50. 0050refl
  51. 0051have hrecurrence_aligned : S n * d = S (n + n) * (2 * c)
  52. 0052trans (2 * S (n + n)) * c
  53. 0053exact hrecurrence
  54. 0054exact hleft_align
  55. 0055have hright_align : (2 * S n) * q = S n * (2 * q)
  56. 0056trans 2 * (S n * q)
  57. 0057apply mul_assoc
  58. 0058trans (S n * q) * 2
  59. 0059apply mul_comm
  60. 0060trans S n * (q * 2)
  61. 0061apply mul_assoc
  62. 0062have hcomm_q_two : q * 2 = 2 * q
  63. 0063apply mul_comm
  64. 0064rewrite hcomm_q_two
  65. 0065refl
  66. 0066rewrite <- hrecurrence_aligned at hcombined
  67. 0067rewrite hright_align at hcombined
  68. 0068have hhalf : Le(d,2 · q)
    Exact native replay linehave hhalf : exists k. k + d = 2 * q
  69. 0069specialize mul_le_cancel_left_nonzero (S n)
  70. 0070specialize mul_le_cancel_left_nonzero d
  71. 0071specialize mul_le_cancel_left_nonzero (2 * q)
  72. 0072apply mul_le_cancel_left_nonzero
  73. 0073specialize succ_ne_zero n
  74. 0074exact succ_ne_zero
  75. 0075exact hcombined
  76. 0076have hdouble : Le(2 · d,2 · (2 · q))
    Exact native replay linehave hdouble : exists k. k + 2 * d = 2 * (2 * q)
  77. 0077specialize mul_le_mul_left d
  78. 0078specialize mul_le_mul_left (2 * q)
  79. 0079specialize mul_le_mul_left 2
  80. 0080apply mul_le_mul_left
  81. 0081exact hhalf
  82. 0082have hfour : 2 * (2 * q) = q * 4
  83. 0083trans (2 * 2) * q
  84. 0084symm
  85. 0085apply mul_assoc
  86. 0086trans 4 * q
  87. 0087have htwo_two : 2 * 2 = 4
  88. 0088norm_num
  89. 0089rewrite htwo_two
  90. 0090refl
  91. 0091apply mul_comm
  92. 0092rewrite hfour at hdouble
  93. 0093rewrite hpower_step
  94. 0094exact hdouble