PE000E

initial_prime_chain_exhausts_primes

Every prime no larger than a decoded terminal prime occurs in the actual prefix; no smaller prime is omitted.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

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.

Every successor is the globally least prime above its predecessor. This is not a sparse Bertrand chain. The bound theorem constructs the list and both power witnesses from k≠0 alone; the separate total-list theorem includes k=0.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ k. ∀ p. ∀ q. InitialPrimeChain(b,c,k) → BetaAt(b,c,k,p) → Prime(q) → Le(q,p) → ∃ x. Le(x,k) ∧ BetaAt(b,c,x,q)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

NextPrime(a,p) · 1InitialPrimeChain(b,c,k) · 2Le(a,b) · 4Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 5

Actual proof prerequisites

beta_at_unique · checked external prerequisitele_antisymm · checked external prerequisiteprime_two_le · checked external prerequisitele_refl · checked external prerequisiteinitial_prime_chain_prefix_restrictle_succ_self · checked external prerequisitele_or_lt · checked external prerequisitele_succ · checked external prerequisite
Original expanded first-order statement 
forall b c k p q. ((((exists fs_h_pen_complete_chain_initial. fs_h_pen_complete_chain_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_complete_chain_initial. b = fs_q_pen_complete_chain_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_complete_chain. (exists pc_lt_pen_complete_chain_bound. pc_lt_pen_complete_chain_bound + S (pen_index_complete_chain) = (k)) -> exists pen_previous_complete_chain pen_following_complete_chain. (((exists fs_h_pen_complete_chain_previous. fs_h_pen_complete_chain_previous + S (pen_previous_complete_chain) = S ((S (pen_index_complete_chain)) * c)) /\ exists fs_q_pen_complete_chain_previous. b = fs_q_pen_complete_chain_previous * S ((S (pen_index_complete_chain)) * c) + (pen_previous_complete_chain))) /\ ((((exists fs_h_pen_complete_chain_following. fs_h_pen_complete_chain_following + S (pen_following_complete_chain) = S ((S (S pen_index_complete_chain)) * c)) /\ exists fs_q_pen_complete_chain_following. b = fs_q_pen_complete_chain_following * S ((S (S pen_index_complete_chain)) * c) + (pen_following_complete_chain))) /\ (((~(pen_following_complete_chain = 1) /\ forall bpr_left_pc_pen_complete_chain_next_prime bpr_right_pc_pen_complete_chain_next_prime. pen_following_complete_chain = bpr_left_pc_pen_complete_chain_next_prime * bpr_right_pc_pen_complete_chain_next_prime -> bpr_left_pc_pen_complete_chain_next_prime = 1 \/ bpr_right_pc_pen_complete_chain_next_prime = 1)) /\ ((exists pc_lt_pen_complete_chain_next_greater. pc_lt_pen_complete_chain_next_greater + S (pen_previous_complete_chain) = (pen_following_complete_chain)) /\ forall pen_comparison_complete_chain_next. ((~(pen_comparison_complete_chain_next = 1) /\ forall bpr_left_pc_pen_complete_chain_next_comparison bpr_right_pc_pen_complete_chain_next_comparison. pen_comparison_complete_chain_next = bpr_left_pc_pen_complete_chain_next_comparison * bpr_right_pc_pen_complete_chain_next_comparison -> bpr_left_pc_pen_complete_chain_next_comparison = 1 \/ bpr_right_pc_pen_complete_chain_next_comparison = 1)) -> (exists pc_lt_pen_complete_chain_next_above. pc_lt_pen_complete_chain_next_above + S (pen_previous_complete_chain) = (pen_comparison_complete_chain_next)) -> (exists pc_le_pen_complete_chain_next_minimal. pc_le_pen_complete_chain_next_minimal + (pen_following_complete_chain) = (pen_comparison_complete_chain_next)))))) -> (((exists fs_h_pen_complete_terminal. fs_h_pen_complete_terminal + S (p) = S ((S (k)) * c)) /\ exists fs_q_pen_complete_terminal. b = fs_q_pen_complete_terminal * S ((S (k)) * c) + (p))) -> ((~(q = 1) /\ forall bpr_left_pc_pen_complete_prime bpr_right_pc_pen_complete_prime. q = bpr_left_pc_pen_complete_prime * bpr_right_pc_pen_complete_prime -> bpr_left_pc_pen_complete_prime = 1 \/ bpr_right_pc_pen_complete_prime = 1)) -> (exists pc_le_pen_complete_value_bound. pc_le_pen_complete_value_bound + (q) = (p)) -> exists i. (exists pc_le_pen_complete_index. pc_le_pen_complete_index + (i) = (k)) /\ (((exists fs_h_pen_complete_found. fs_h_pen_complete_found + S (q) = S ((S (i)) * c)) /\ exists fs_q_pen_complete_found. b = fs_q_pen_complete_found * S ((S (i)) * c) + (q)))

Complete tactic proof in conservative notation

All 110 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

110 script commands · 29 reading checkpoints · 8 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 (1)
initial prime chain prefix restrict
01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on kL3–9

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction k
  2. L4
    intro p
  3. L5
    intro q
  4. L6
    intro hc
  5. L7
    intro hp
  6. L8
    intro hq
  7. L9
    intro hqp
03Separate the logical casesL10–10

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

  1. L10
    cases hc
04Establish hp2L11–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L11
    have hp2 : p = 2
  2. L12
    specialize beta_at_unique b
  3. L13
    specialize beta_at_unique c
  4. L14
    specialize beta_at_unique 0
  5. L15
    specialize beta_at_unique p
  6. L16
    specialize beta_at_unique 2
  7. L17
    apply beta_at_unique
  8. L18
    exact hp
  9. L19
    exact hc_left
05Establish hq2L20–28

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

  1. L20
    have hq2 : q = 2
  2. L21
    specialize le_antisymm q
  3. L22
    specialize le_antisymm 2
  4. L23
    apply le_antisymm
  5. L24
    rewrite hp2 at hqp
  6. L25
    exact hqp
  7. L26
    specialize prime_two_le q
  8. L27
    apply prime_two_le
  9. L28
    exact hq
06Construct an explicit witnessL29–29

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

  1. L29
    exists 0
07Separate the logical casesL30–30

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

  1. L30
    split
08Use earlier factsL31–32

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

  1. L31
    specialize le_refl 0
  2. L32
    apply le_refl
09Calculate and transport equalitiesL33–34

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

  1. L33
    rewrite hq2
  2. L34
    rewrite hq2
10Use earlier factsL35–35

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

  1. L35
    exact hc_left
11Fix variables and assumptionsL36–41

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

  1. L36
    intro p
  2. L37
    intro q
  3. L38
    intro hc
  4. L39
    intro hp
  5. L40
    intro hq
  6. L41
    intro hqp
12Establish hrL42–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply initial prime chain prefix restrict.

  1. L42
    have hr : InitialPrimeChain(b,c,k)Definitions: InitialPrimeChain(b,c,k)Original native command in the exact edition
  2. L43
    specialize initial_prime_chain_prefix_restrict b
  3. L44
    specialize initial_prime_chain_prefix_restrict c
  4. L45
    specialize initial_prime_chain_prefix_restrict (S k)
  5. L46
    specialize initial_prime_chain_prefix_restrict k
  6. L47
    apply initial_prime_chain_prefix_restrict
  7. L48
    specialize le_succ_self k
  8. L49
    apply le_succ_self
  9. L50
    exact hc
13Separate the logical casesL51–51

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

  1. L51
    cases hc
14Establish heL52–56

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

  1. L52
    have he : ∃ a. ∃ t. BetaAt(b,c,k,a) ∧ (BetaAt(b,c,S k,t) ∧ NextPrime(a,t))Definitions: BetaAt(b,c,k,a)BetaAt(b,c,S k,t)NextPrime(a,t)Original native command in the exact edition
  2. L53
    specialize hc_right k
  3. L54
    apply hc_right
  4. L55
    specialize le_refl (S k)
  5. L56
    apply le_refl
15Separate the logical casesL57–62

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

  1. L57
    cases he
  2. L58
    cases he_witness
  3. L59
    cases he_witness_witness
  4. L60
    cases he_witness_witness_right
  5. L61
    cases he_witness_witness_right_right
  6. L62
    cases he_witness_witness_right_right_right
16Establish hpeqL63–71

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L63
    have hpeq : p = x1
  2. L64
    specialize beta_at_unique b
  3. L65
    specialize beta_at_unique c
  4. L66
    specialize beta_at_unique (S k)
  5. L67
    specialize beta_at_unique p
  6. L68
    specialize beta_at_unique x1
  7. L69
    apply beta_at_unique
  8. L70
    exact hp
  9. L71
    exact he_witness_witness_right_left
17Establish hsL72–75

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

  1. L72
    have hs : Le(q,x) ∨ Lt(x,q)Definitions: Le(q,x)Lt(x,q)Original native command in the exact edition
  2. L73
    specialize le_or_lt q
  3. L74
    specialize le_or_lt x
  4. L75
    apply le_or_lt
18Separate the logical casesL76–76

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

  1. L76
    cases hs
19Establish hoL77–84

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

  1. L77
    have ho : ∃ i. Le(i,k) ∧ BetaAt(b,c,i,q)Definitions: Le(i,k)BetaAt(b,c,i,q)Original native command in the exact edition
  2. L78
    specialize IH x
  3. L79
    specialize IH q
  4. L80
    apply IH
  5. L81
    exact hr
  6. L82
    exact he_witness_witness_left
  7. L83
    exact hq
  8. L84
    exact hs_left
20Separate the logical casesL85–86

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

  1. L85
    cases ho
  2. L86
    cases ho_witness
21Construct an explicit witnessL87–87

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

  1. L87
    exists x2
22Separate the logical casesL88–88

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

  1. L88
    split
23Use earlier factsL89–93

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

  1. L89
    specialize le_succ x2
  2. L90
    specialize le_succ k
  3. L91
    apply le_succ
  4. L92
    exact ho_witness_left
  5. L93
    exact ho_witness_right
24Establish hqp_eqL94–103

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

  1. L94
    have hqp_eq : q = p
  2. L95
    specialize le_antisymm q
  3. L96
    specialize le_antisymm p
  4. L97
    apply le_antisymm
  5. L98
    exact hqp
  6. L99
    rewrite hpeq
  7. L100
    specialize he_witness_witness_right_right_right_right q
  8. L101
    apply he_witness_witness_right_right_right_right
  9. L102
    exact hq
  10. L103
    exact hs_right
25Construct an explicit witnessL104–104

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

  1. L104
    exists S k
26Separate the logical casesL105–105

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

  1. L105
    split
27Use earlier factsL106–107

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

  1. L106
    specialize le_refl (S k)
  2. L107
    apply le_refl
28Calculate and transport equalitiesL108–109

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

  1. L108
    rewrite hqp_eq
  2. L109
    rewrite hqp_eq
29Use earlier factsL110–110

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

  1. L110
    exact hp

Library-wide reading audit

Original defined command ledger · 110 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction k
  4. 0004intro p
  5. 0005intro q
  6. 0006intro hc
  7. 0007intro hp
  8. 0008intro hq
  9. 0009intro hqp
  10. 0010cases hc
  11. 0011have hp2 : p = 2
  12. 0012specialize beta_at_unique b
  13. 0013specialize beta_at_unique c
  14. 0014specialize beta_at_unique 0
  15. 0015specialize beta_at_unique p
  16. 0016specialize beta_at_unique 2
  17. 0017apply beta_at_unique
  18. 0018exact hp
  19. 0019exact hc_left
  20. 0020have hq2 : q = 2
  21. 0021specialize le_antisymm q
  22. 0022specialize le_antisymm 2
  23. 0023apply le_antisymm
  24. 0024rewrite hp2 at hqp
  25. 0025exact hqp
  26. 0026specialize prime_two_le q
  27. 0027apply prime_two_le
  28. 0028exact hq
  29. 0029exists 0
  30. 0030split
  31. 0031specialize le_refl 0
  32. 0032apply le_refl
  33. 0033rewrite hq2
  34. 0034rewrite hq2
  35. 0035exact hc_left
  36. 0036intro p
  37. 0037intro q
  38. 0038intro hc
  39. 0039intro hp
  40. 0040intro hq
  41. 0041intro hqp
  42. 0042have hr : InitialPrimeChain(b,c,k)
  43. 0043specialize initial_prime_chain_prefix_restrict b
  44. 0044specialize initial_prime_chain_prefix_restrict c
  45. 0045specialize initial_prime_chain_prefix_restrict (S k)
  46. 0046specialize initial_prime_chain_prefix_restrict k
  47. 0047apply initial_prime_chain_prefix_restrict
  48. 0048specialize le_succ_self k
  49. 0049apply le_succ_self
  50. 0050exact hc
  51. 0051cases hc
  52. 0052have he : ∃ a. ∃ t. BetaAt(b,c,k,a) ∧ (BetaAt(b,c,S k,t) ∧ NextPrime(a,t))
  53. 0053specialize hc_right k
  54. 0054apply hc_right
  55. 0055specialize le_refl (S k)
  56. 0056apply le_refl
  57. 0057cases he
  58. 0058cases he_witness
  59. 0059cases he_witness_witness
  60. 0060cases he_witness_witness_right
  61. 0061cases he_witness_witness_right_right
  62. 0062cases he_witness_witness_right_right_right
  63. 0063have hpeq : p = x1
  64. 0064specialize beta_at_unique b
  65. 0065specialize beta_at_unique c
  66. 0066specialize beta_at_unique (S k)
  67. 0067specialize beta_at_unique p
  68. 0068specialize beta_at_unique x1
  69. 0069apply beta_at_unique
  70. 0070exact hp
  71. 0071exact he_witness_witness_right_left
  72. 0072have hs : Le(q,x) ∨ Lt(x,q)
  73. 0073specialize le_or_lt q
  74. 0074specialize le_or_lt x
  75. 0075apply le_or_lt
  76. 0076cases hs
  77. 0077have ho : ∃ i. Le(i,k) ∧ BetaAt(b,c,i,q)
  78. 0078specialize IH x
  79. 0079specialize IH q
  80. 0080apply IH
  81. 0081exact hr
  82. 0082exact he_witness_witness_left
  83. 0083exact hq
  84. 0084exact hs_left
  85. 0085cases ho
  86. 0086cases ho_witness
  87. 0087exists x2
  88. 0088split
  89. 0089specialize le_succ x2
  90. 0090specialize le_succ k
  91. 0091apply le_succ
  92. 0092exact ho_witness_left
  93. 0093exact ho_witness_right
  94. 0094have hqp_eq : q = p
  95. 0095specialize le_antisymm q
  96. 0096specialize le_antisymm p
  97. 0097apply le_antisymm
  98. 0098exact hqp
  99. 0099rewrite hpeq
  100. 0100specialize he_witness_witness_right_right_right_right q
  101. 0101apply he_witness_witness_right_right_right_right
  102. 0102exact hq
  103. 0103exact hs_right
  104. 0104exists S k
  105. 0105split
  106. 0106specialize le_refl (S k)
  107. 0107apply le_refl
  108. 0108rewrite hqp_eq
  109. 0109rewrite hqp_eq
  110. 0110exact hp