PE0010

prime_list_every_entry_is_prime

Every entry of every first-prime list is prime, with the empty-list boundary proved vacuously.

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. ∀ i. ∀ p. InitialPrimeList(b,c,k) → Lt(i,k) → BetaAt(b,c,i,p) → Prime(p)

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

Definition DAG

InitialPrimeList(b,c,k) · 1Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

lt_not_le · checked external prerequisitezero_le · checked external prerequisitele_of_succ_le_succ · checked external prerequisiteinitial_prime_chain_prefix_restrictinitial_prime_chain_terminal_is_prime
Original expanded first-order statement 
forall b c k i p. ((k = 0 \/ exists pen_last_index_entries_list. k = S pen_last_index_entries_list /\ ((((exists fs_h_pen_entries_list_chain_initial. fs_h_pen_entries_list_chain_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_entries_list_chain_initial. b = fs_q_pen_entries_list_chain_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_entries_list_chain. (exists pc_lt_pen_entries_list_chain_bound. pc_lt_pen_entries_list_chain_bound + S (pen_index_entries_list_chain) = (pen_last_index_entries_list)) -> exists pen_previous_entries_list_chain pen_following_entries_list_chain. (((exists fs_h_pen_entries_list_chain_previous. fs_h_pen_entries_list_chain_previous + S (pen_previous_entries_list_chain) = S ((S (pen_index_entries_list_chain)) * c)) /\ exists fs_q_pen_entries_list_chain_previous. b = fs_q_pen_entries_list_chain_previous * S ((S (pen_index_entries_list_chain)) * c) + (pen_previous_entries_list_chain))) /\ ((((exists fs_h_pen_entries_list_chain_following. fs_h_pen_entries_list_chain_following + S (pen_following_entries_list_chain) = S ((S (S pen_index_entries_list_chain)) * c)) /\ exists fs_q_pen_entries_list_chain_following. b = fs_q_pen_entries_list_chain_following * S ((S (S pen_index_entries_list_chain)) * c) + (pen_following_entries_list_chain))) /\ (((~(pen_following_entries_list_chain = 1) /\ forall bpr_left_pc_pen_entries_list_chain_next_prime bpr_right_pc_pen_entries_list_chain_next_prime. pen_following_entries_list_chain = bpr_left_pc_pen_entries_list_chain_next_prime * bpr_right_pc_pen_entries_list_chain_next_prime -> bpr_left_pc_pen_entries_list_chain_next_prime = 1 \/ bpr_right_pc_pen_entries_list_chain_next_prime = 1)) /\ ((exists pc_lt_pen_entries_list_chain_next_greater. pc_lt_pen_entries_list_chain_next_greater + S (pen_previous_entries_list_chain) = (pen_following_entries_list_chain)) /\ forall pen_comparison_entries_list_chain_next. ((~(pen_comparison_entries_list_chain_next = 1) /\ forall bpr_left_pc_pen_entries_list_chain_next_comparison bpr_right_pc_pen_entries_list_chain_next_comparison. pen_comparison_entries_list_chain_next = bpr_left_pc_pen_entries_list_chain_next_comparison * bpr_right_pc_pen_entries_list_chain_next_comparison -> bpr_left_pc_pen_entries_list_chain_next_comparison = 1 \/ bpr_right_pc_pen_entries_list_chain_next_comparison = 1)) -> (exists pc_lt_pen_entries_list_chain_next_above. pc_lt_pen_entries_list_chain_next_above + S (pen_previous_entries_list_chain) = (pen_comparison_entries_list_chain_next)) -> (exists pc_le_pen_entries_list_chain_next_minimal. pc_le_pen_entries_list_chain_next_minimal + (pen_following_entries_list_chain) = (pen_comparison_entries_list_chain_next)))))))) -> (exists pc_lt_pen_entries_index. pc_lt_pen_entries_index + S (i) = (k)) -> (((exists fs_h_pen_entries_value. fs_h_pen_entries_value + S (p) = S ((S (i)) * c)) /\ exists fs_q_pen_entries_value. b = fs_q_pen_entries_value * S ((S (i)) * c) + (p))) -> ((~(p = 1) /\ forall bpr_left_pc_pen_entries_prime bpr_right_pc_pen_entries_prime. p = bpr_left_pc_pen_entries_prime * bpr_right_pc_pen_entries_prime -> bpr_left_pc_pen_entries_prime = 1 \/ bpr_right_pc_pen_entries_prime = 1))

Complete tactic proof in conservative notation

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

36 script commands · 9 reading checkpoints · 0 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 (2)
initial prime chain terminal is primeinitial prime chain prefix restrict
01Fix variables and assumptionsL1–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro k
  4. L4
    intro i
  5. L5
    intro p
  6. L6
    intro hl
  7. L7
    intro hi
  8. L8
    intro hp
02Separate the logical casesL9–10

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

  1. L9
    cases hl
  2. L10
    exfalso
03Calculate and transport equalitiesL11–11

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

  1. L11
    rewrite hl_left at hi
04Use earlier factsL12–17

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

  1. L12
    specialize lt_not_le i
  2. L13
    specialize lt_not_le 0
  3. L14
    apply lt_not_le
  4. L15
    exact hi
  5. L16
    specialize zero_le i
  6. L17
    apply zero_le
05Separate the logical casesL18–19

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

  1. L18
    cases hl_right
  2. L19
    cases hl_right_witness
06Use earlier factsL20–29

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

  1. L20
    specialize initial_prime_chain_terminal_is_prime b
  2. L21
    specialize initial_prime_chain_terminal_is_prime c
  3. L22
    specialize initial_prime_chain_terminal_is_prime i
  4. L23
    specialize initial_prime_chain_terminal_is_prime p
  5. L24
    apply initial_prime_chain_terminal_is_prime
  6. L25
    specialize initial_prime_chain_prefix_restrict b
  7. L26
    specialize initial_prime_chain_prefix_restrict c
  8. L27
    specialize initial_prime_chain_prefix_restrict x
  9. L28
    specialize initial_prime_chain_prefix_restrict i
  10. L29
    apply initial_prime_chain_prefix_restrict
07Use earlier factsL30–32

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

  1. L30
    specialize le_of_succ_le_succ i
  2. L31
    specialize le_of_succ_le_succ x
  3. L32
    apply le_of_succ_le_succ
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 hl_right_witness_left at hi
09Use earlier factsL34–36

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

  1. L34
    exact hi
  2. L35
    exact hl_right_witness_right
  3. L36
    exact hp

Library-wide reading audit

Original defined command ledger · 36 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro k
  4. 0004intro i
  5. 0005intro p
  6. 0006intro hl
  7. 0007intro hi
  8. 0008intro hp
  9. 0009cases hl
  10. 0010exfalso
  11. 0011rewrite hl_left at hi
  12. 0012specialize lt_not_le i
  13. 0013specialize lt_not_le 0
  14. 0014apply lt_not_le
  15. 0015exact hi
  16. 0016specialize zero_le i
  17. 0017apply zero_le
  18. 0018cases hl_right
  19. 0019cases hl_right_witness
  20. 0020specialize initial_prime_chain_terminal_is_prime b
  21. 0021specialize initial_prime_chain_terminal_is_prime c
  22. 0022specialize initial_prime_chain_terminal_is_prime i
  23. 0023specialize initial_prime_chain_terminal_is_prime p
  24. 0024apply initial_prime_chain_terminal_is_prime
  25. 0025specialize initial_prime_chain_prefix_restrict b
  26. 0026specialize initial_prime_chain_prefix_restrict c
  27. 0027specialize initial_prime_chain_prefix_restrict x
  28. 0028specialize initial_prime_chain_prefix_restrict i
  29. 0029apply initial_prime_chain_prefix_restrict
  30. 0030specialize le_of_succ_le_succ i
  31. 0031specialize le_of_succ_le_succ x
  32. 0032apply le_of_succ_le_succ
  33. 0033rewrite hl_right_witness_left at hi
  34. 0034exact hi
  35. 0035exact hl_right_witness_right
  36. 0036exact hp