PE0013

first_primes_list_exists

Every finite number of initial primes has a real beta-coded list, including the empty list at zero.

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

∀ k. ∃ b. ∃ c. InitialPrimeList(b,c,k)

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

Definition DAG

PowTwo(e,p) · 2InitialPrimeList(b,c,k) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

eq_decidable · checked external prerequisitefirst_primes_double_exponential_bound
Original expanded first-order statement 
forall k. exists b c. (k = 0 \/ exists pen_last_index_total_list. k = S pen_last_index_total_list /\ ((((exists fs_h_pen_total_list_chain_initial. fs_h_pen_total_list_chain_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_total_list_chain_initial. b = fs_q_pen_total_list_chain_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_total_list_chain. (exists pc_lt_pen_total_list_chain_bound. pc_lt_pen_total_list_chain_bound + S (pen_index_total_list_chain) = (pen_last_index_total_list)) -> exists pen_previous_total_list_chain pen_following_total_list_chain. (((exists fs_h_pen_total_list_chain_previous. fs_h_pen_total_list_chain_previous + S (pen_previous_total_list_chain) = S ((S (pen_index_total_list_chain)) * c)) /\ exists fs_q_pen_total_list_chain_previous. b = fs_q_pen_total_list_chain_previous * S ((S (pen_index_total_list_chain)) * c) + (pen_previous_total_list_chain))) /\ ((((exists fs_h_pen_total_list_chain_following. fs_h_pen_total_list_chain_following + S (pen_following_total_list_chain) = S ((S (S pen_index_total_list_chain)) * c)) /\ exists fs_q_pen_total_list_chain_following. b = fs_q_pen_total_list_chain_following * S ((S (S pen_index_total_list_chain)) * c) + (pen_following_total_list_chain))) /\ (((~(pen_following_total_list_chain = 1) /\ forall bpr_left_pc_pen_total_list_chain_next_prime bpr_right_pc_pen_total_list_chain_next_prime. pen_following_total_list_chain = bpr_left_pc_pen_total_list_chain_next_prime * bpr_right_pc_pen_total_list_chain_next_prime -> bpr_left_pc_pen_total_list_chain_next_prime = 1 \/ bpr_right_pc_pen_total_list_chain_next_prime = 1)) /\ ((exists pc_lt_pen_total_list_chain_next_greater. pc_lt_pen_total_list_chain_next_greater + S (pen_previous_total_list_chain) = (pen_following_total_list_chain)) /\ forall pen_comparison_total_list_chain_next. ((~(pen_comparison_total_list_chain_next = 1) /\ forall bpr_left_pc_pen_total_list_chain_next_comparison bpr_right_pc_pen_total_list_chain_next_comparison. pen_comparison_total_list_chain_next = bpr_left_pc_pen_total_list_chain_next_comparison * bpr_right_pc_pen_total_list_chain_next_comparison -> bpr_left_pc_pen_total_list_chain_next_comparison = 1 \/ bpr_right_pc_pen_total_list_chain_next_comparison = 1)) -> (exists pc_lt_pen_total_list_chain_next_above. pc_lt_pen_total_list_chain_next_above + S (pen_previous_total_list_chain) = (pen_comparison_total_list_chain_next)) -> (exists pc_le_pen_total_list_chain_next_minimal. pc_le_pen_total_list_chain_next_minimal + (pen_following_total_list_chain) = (pen_comparison_total_list_chain_next)))))))

Complete tactic proof in conservative notation

All 25 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

25 script commands · 10 reading checkpoints · 2 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)
first primes double exponential bound
01Fix variables and assumptionsL1–1

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

  1. L1
    intro k
02Establish hzL2–5

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

  1. L2
    have hz : k = 0 \/ ~(k = 0)
  2. L3
    specialize eq_decidable k
  3. L4
    specialize eq_decidable 0
  4. L5
    apply eq_decidable
03Separate the logical casesL6–6

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

  1. L6
    cases hz
04Construct an explicit witnessL7–8

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

  1. L7
    exists 0
  2. L8
    exists 0
05Separate the logical casesL9–9

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

  1. L9
    left
06Use earlier factsL10–11

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

  1. L10
    exact hz_left
  2. L11
    specialize first_primes_double_exponential_bound k
07Establish hpositiveL12–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply first primes double exponential bound.

  1. L12
    have hpositive : ∃ b. ∃ c. ∃ j. ∃ p. ∃ e. ∃ B. k = S j ∧ (InitialPrimeList(b,c,k) ∧ (BetaAt(b,c,j,p) ∧ (PowTwo(k,e) ∧ (PowTwo(e,B) ∧ Lt(p,B)))))Definitions: InitialPrimeList(b,c,k)BetaAt(b,c,j,p)PowTwo(k,e)PowTwo(e,B)Lt(p,B)Original native command in the exact edition
  2. L13
    apply first_primes_double_exponential_bound
  3. L14
    exact hz_right
08Separate the logical casesL15–22

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

  1. L15
    cases hpositive
  2. L16
    cases hpositive_witness
  3. L17
    cases hpositive_witness_witness
  4. L18
    cases hpositive_witness_witness_witness
  5. L19
    cases hpositive_witness_witness_witness_witness
  6. L20
    cases hpositive_witness_witness_witness_witness_witness
  7. L21
    cases hpositive_witness_witness_witness_witness_witness_witness
  8. L22
    cases hpositive_witness_witness_witness_witness_witness_witness_right
09Construct an explicit witnessL23–24

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

  1. L23
    exists x
  2. L24
    exists x1
10Use earlier factsL25–25

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

  1. L25
    exact hpositive_witness_witness_witness_witness_witness_witness_right_left

Library-wide reading audit

Original defined command ledger · 25 lines
  1. 0001intro k
  2. 0002have hz : k = 0 \/ ~(k = 0)
  3. 0003specialize eq_decidable k
  4. 0004specialize eq_decidable 0
  5. 0005apply eq_decidable
  6. 0006cases hz
  7. 0007exists 0
  8. 0008exists 0
  9. 0009left
  10. 0010exact hz_left
  11. 0011specialize first_primes_double_exponential_bound k
  12. 0012have hpositive : ∃ b. ∃ c. ∃ j. ∃ p. ∃ e. ∃ B. k = S j ∧ (InitialPrimeList(b,c,k) ∧ (BetaAt(b,c,j,p) ∧ (PowTwo(k,e) ∧ (PowTwo(e,B) ∧ Lt(p,B)))))
  13. 0013apply first_primes_double_exponential_bound
  14. 0014exact hz_right
  15. 0015cases hpositive
  16. 0016cases hpositive_witness
  17. 0017cases hpositive_witness_witness
  18. 0018cases hpositive_witness_witness_witness
  19. 0019cases hpositive_witness_witness_witness_witness
  20. 0020cases hpositive_witness_witness_witness_witness_witness
  21. 0021cases hpositive_witness_witness_witness_witness_witness_witness
  22. 0022cases hpositive_witness_witness_witness_witness_witness_witness_right
  23. 0023exists x
  24. 0024exists x1
  25. 0025exact hpositive_witness_witness_witness_witness_witness_witness_right_left