BT00U0 · Bertrand theorem

four_power_central_recurrence_step

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

A weighted central recurrence equation advances the strict four-power lower 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. ∀ q. ∀ c. ∀ d. Lt(q,n · c) → S n · d = 2 · S (n + n) · c → Lt(q · 4,S n · d)

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

PD0002 Lt

2 occurrences

In local proof propositions

PD0002 Lt

4 occurrences

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

Proof neighborhood

Direct theorem prerequisites

BT000L add_eq_zero_right BT0002 add_comm BT0006 mul_comm BT0008 mul_assoc BT0007 mul_add BT000B add_mul BT00TY mul_lt_mul_right_nonzero BT001F lt_trans

Direct theorem dependents

BT00U4 four_pow_lt_mul_central_binom

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

75 script commands · 27 reading checkpoints · 7 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 (8)
add eq zero rightadd commmul commmul assocmul addadd mulmul lt mul right nonzerolt trans
01Fix variables and assumptionsL1–6

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

  1. L1
    intro n
  2. L2
    intro q
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro hstrict
  6. L6
    intro hrecurrence
02Establish hcL7–8

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

  1. L7
    have hc : ~(c = 0)
  2. L8
    intro hc_zero
03Separate the logical casesL9–9

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    cases hstrict
04Use earlier factsL10–13

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

  1. L10
    apply PA1
  2. L11
    specialize add_eq_zero_right x
  3. L12
    specialize add_eq_zero_right (S q)
  4. L13
    apply add_eq_zero_right
05Calculate and transport equalitiesL14–14

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

  1. L14
    trans n * c
06Use earlier factsL15–15

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

  1. L15
    exact hstrict_witness
07Calculate and transport equalitiesL16–16

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

  1. L16
    rewrite hc_zero
08Use earlier factsL17–17

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

  1. L17
    apply PA5
09Establish hscaledL18–26

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

  1. L18
    have hscaled : Lt(q · 4,n · c · 4)Definitions: Lt(q · 4,n · c · 4)Original native command in the exact edition
  2. L19
    specialize mul_lt_mul_right_nonzero q
  3. L20
    specialize mul_lt_mul_right_nonzero (n * c)
  4. L21
    specialize mul_lt_mul_right_nonzero 4
  5. L22
    apply mul_lt_mul_right_nonzero
  6. L23
    exact hstrict
  7. L24
    intro hfour_zero
  8. L25
    apply PA1
  9. L26
    exact hfour_zero
10Establish hfourL27–32

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

  1. L27
    have hfour : 4 * n = 2 * n + 2 * n
  2. L28
    trans (2 + 2) * n
  3. L29
    congr
  4. L30
    norm_num
  5. L31
    refl
  6. L32
    apply add_mul
11Establish hcoefficientL33–33

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

  1. L33
    have hcoefficient : Lt(4 · n,2 · S (n + n))Definitions: Lt(4 · n,2 · S (n + n))Original native command in the exact edition
12Construct an explicit witnessL34–34

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

  1. L34
    exists 1
13Calculate and transport equalitiesL35–35

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

  1. L35
    trans S (1 + 4 * n)
14Use earlier factsL36–36

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

  1. L36
    apply PA4
15Calculate and transport equalitiesL37–38

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

  1. L37
    trans S (4 * n + 1)
  2. L38
    congr
16Use earlier factsL39–39

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

  1. L39
    apply add_comm
17Calculate and transport equalitiesL40–41

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

  1. L40
    trans 4 * n + 2
  2. L41
    symm
18Use earlier factsL42–42

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

  1. L42
    apply PA4
19Calculate and transport equalitiesL43–44

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

  1. L43
    trans (2 * n + 2 * n) + 2
  2. L44
    congr
20Use earlier factsL45–45

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

  1. L45
    exact hfour
21Calculate and transport equalitiesL46–49

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

  1. L46
    refl
  2. L47
    trans 2 * (n + n) + 2
  3. L48
    congr
  4. L49
    symm
22Use earlier factsL50–50

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

  1. L50
    apply mul_add
23Calculate and transport equalitiesL51–52

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

  1. L51
    refl
  2. L52
    symm
24Use earlier factsL53–53

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

  1. L53
    apply PA6
25Establish hcoefficient_productL54–60

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

  1. L54
    have hcoefficient_product : Lt(4 · n · c,2 · S (n + n) · c)Definitions: Lt(4 · n · c,2 · S (n + n) · c)Original native command in the exact edition
  2. L55
    specialize mul_lt_mul_right_nonzero (4 * n)
  3. L56
    specialize mul_lt_mul_right_nonzero (2 * S (n + n))
  4. L57
    specialize mul_lt_mul_right_nonzero c
  5. L58
    apply mul_lt_mul_right_nonzero
  6. L59
    exact hcoefficient
  7. L60
    exact hc
26Establish hshuffleL61–65

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

  1. L61
    have hshuffle : (n * c) * 4 = (4 * n) * c
  2. L62
    trans 4 * (n * c)
  3. L63
    apply mul_comm
  4. L64
    symm
  5. L65
    apply mul_assoc
27Establish hgapL66–75

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

  1. L66
    have hgap : Lt(n · c · 4,S n · d)Definitions: Lt(n · c · 4,S n · d)Original native command in the exact edition
  2. L67
    rewrite hshuffle
  3. L68
    rewrite hrecurrence
  4. L69
    exact hcoefficient_product
  5. L70
    specialize lt_trans (q * 4)
  6. L71
    specialize lt_trans ((n * c) * 4)
  7. L72
    specialize lt_trans (S n * d)
  8. L73
    apply lt_trans
  9. L74
    exact hscaled
  10. L75
    exact hgap

Library-wide reading audit

Original defined command ledger · 75 lines
  1. 0001intro n
  2. 0002intro q
  3. 0003intro c
  4. 0004intro d
  5. 0005intro hstrict
  6. 0006intro hrecurrence
  7. 0007have hc : ~(c = 0)
  8. 0008intro hc_zero
  9. 0009cases hstrict
  10. 0010apply PA1
  11. 0011specialize add_eq_zero_right x
  12. 0012specialize add_eq_zero_right (S q)
  13. 0013apply add_eq_zero_right
  14. 0014trans n * c
  15. 0015exact hstrict_witness
  16. 0016rewrite hc_zero
  17. 0017apply PA5
  18. 0018have hscaled : Lt(q · 4,n · c · 4)
    Exact native replay linehave hscaled : exists bcf_lt_gap_bfpcrs_scaled. bcf_lt_gap_bfpcrs_scaled + S (q * 4) = (n * c) * 4
  19. 0019specialize mul_lt_mul_right_nonzero q
  20. 0020specialize mul_lt_mul_right_nonzero (n * c)
  21. 0021specialize mul_lt_mul_right_nonzero 4
  22. 0022apply mul_lt_mul_right_nonzero
  23. 0023exact hstrict
  24. 0024intro hfour_zero
  25. 0025apply PA1
  26. 0026exact hfour_zero
  27. 0027have hfour : 4 * n = 2 * n + 2 * n
  28. 0028trans (2 + 2) * n
  29. 0029congr
  30. 0030norm_num
  31. 0031refl
  32. 0032apply add_mul
  33. 0033have hcoefficient : Lt(4 · n,2 · S (n + n))
    Exact native replay linehave hcoefficient : exists bcf_lt_gap_bfpcrs_coefficient. bcf_lt_gap_bfpcrs_coefficient + S (4 * n) = 2 * S (n + n)
  34. 0034exists 1
  35. 0035trans S (1 + 4 * n)
  36. 0036apply PA4
  37. 0037trans S (4 * n + 1)
  38. 0038congr
  39. 0039apply add_comm
  40. 0040trans 4 * n + 2
  41. 0041symm
  42. 0042apply PA4
  43. 0043trans (2 * n + 2 * n) + 2
  44. 0044congr
  45. 0045exact hfour
  46. 0046refl
  47. 0047trans 2 * (n + n) + 2
  48. 0048congr
  49. 0049symm
  50. 0050apply mul_add
  51. 0051refl
  52. 0052symm
  53. 0053apply PA6
  54. 0054have hcoefficient_product : Lt(4 · n · c,2 · S (n + n) · c)
    Exact native replay linehave hcoefficient_product : exists bcf_lt_gap_bfpcrs_coefficient_product. bcf_lt_gap_bfpcrs_coefficient_product + S ((4 * n) * c) = (2 * S (n + n)) * c
  55. 0055specialize mul_lt_mul_right_nonzero (4 * n)
  56. 0056specialize mul_lt_mul_right_nonzero (2 * S (n + n))
  57. 0057specialize mul_lt_mul_right_nonzero c
  58. 0058apply mul_lt_mul_right_nonzero
  59. 0059exact hcoefficient
  60. 0060exact hc
  61. 0061have hshuffle : (n * c) * 4 = (4 * n) * c
  62. 0062trans 4 * (n * c)
  63. 0063apply mul_comm
  64. 0064symm
  65. 0065apply mul_assoc
  66. 0066have hgap : Lt(n · c · 4,S n · d)
    Exact native replay linehave hgap : exists bcf_lt_gap_bfpcrs_gap. bcf_lt_gap_bfpcrs_gap + S ((n * c) * 4) = S n * d
  67. 0067rewrite hshuffle
  68. 0068rewrite hrecurrence
  69. 0069exact hcoefficient_product
  70. 0070specialize lt_trans (q * 4)
  71. 0071specialize lt_trans ((n * c) * 4)
  72. 0072specialize lt_trans (S n * d)
  73. 0073apply lt_trans
  74. 0074exact hscaled
  75. 0075exact hgap