PE0011

prime_list_omits_no_smaller_prime

The first-prime list is exhaustive below each of its entries, with an explicit bounded index witnessing every smaller prime.

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

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

Definition DAG

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

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_exhausts_primes
Original expanded first-order statement 
forall b c k i p q. ((k = 0 \/ exists pen_last_index_list_complete_source. k = S pen_last_index_list_complete_source /\ ((((exists fs_h_pen_list_complete_source_chain_initial. fs_h_pen_list_complete_source_chain_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_list_complete_source_chain_initial. b = fs_q_pen_list_complete_source_chain_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_list_complete_source_chain. (exists pc_lt_pen_list_complete_source_chain_bound. pc_lt_pen_list_complete_source_chain_bound + S (pen_index_list_complete_source_chain) = (pen_last_index_list_complete_source)) -> exists pen_previous_list_complete_source_chain pen_following_list_complete_source_chain. (((exists fs_h_pen_list_complete_source_chain_previous. fs_h_pen_list_complete_source_chain_previous + S (pen_previous_list_complete_source_chain) = S ((S (pen_index_list_complete_source_chain)) * c)) /\ exists fs_q_pen_list_complete_source_chain_previous. b = fs_q_pen_list_complete_source_chain_previous * S ((S (pen_index_list_complete_source_chain)) * c) + (pen_previous_list_complete_source_chain))) /\ ((((exists fs_h_pen_list_complete_source_chain_following. fs_h_pen_list_complete_source_chain_following + S (pen_following_list_complete_source_chain) = S ((S (S pen_index_list_complete_source_chain)) * c)) /\ exists fs_q_pen_list_complete_source_chain_following. b = fs_q_pen_list_complete_source_chain_following * S ((S (S pen_index_list_complete_source_chain)) * c) + (pen_following_list_complete_source_chain))) /\ (((~(pen_following_list_complete_source_chain = 1) /\ forall bpr_left_pc_pen_list_complete_source_chain_next_prime bpr_right_pc_pen_list_complete_source_chain_next_prime. pen_following_list_complete_source_chain = bpr_left_pc_pen_list_complete_source_chain_next_prime * bpr_right_pc_pen_list_complete_source_chain_next_prime -> bpr_left_pc_pen_list_complete_source_chain_next_prime = 1 \/ bpr_right_pc_pen_list_complete_source_chain_next_prime = 1)) /\ ((exists pc_lt_pen_list_complete_source_chain_next_greater. pc_lt_pen_list_complete_source_chain_next_greater + S (pen_previous_list_complete_source_chain) = (pen_following_list_complete_source_chain)) /\ forall pen_comparison_list_complete_source_chain_next. ((~(pen_comparison_list_complete_source_chain_next = 1) /\ forall bpr_left_pc_pen_list_complete_source_chain_next_comparison bpr_right_pc_pen_list_complete_source_chain_next_comparison. pen_comparison_list_complete_source_chain_next = bpr_left_pc_pen_list_complete_source_chain_next_comparison * bpr_right_pc_pen_list_complete_source_chain_next_comparison -> bpr_left_pc_pen_list_complete_source_chain_next_comparison = 1 \/ bpr_right_pc_pen_list_complete_source_chain_next_comparison = 1)) -> (exists pc_lt_pen_list_complete_source_chain_next_above. pc_lt_pen_list_complete_source_chain_next_above + S (pen_previous_list_complete_source_chain) = (pen_comparison_list_complete_source_chain_next)) -> (exists pc_le_pen_list_complete_source_chain_next_minimal. pc_le_pen_list_complete_source_chain_next_minimal + (pen_following_list_complete_source_chain) = (pen_comparison_list_complete_source_chain_next)))))))) -> (exists pc_lt_pen_list_complete_index. pc_lt_pen_list_complete_index + S (i) = (k)) -> (((exists fs_h_pen_list_complete_value. fs_h_pen_list_complete_value + S (p) = S ((S (i)) * c)) /\ exists fs_q_pen_list_complete_value. b = fs_q_pen_list_complete_value * S ((S (i)) * c) + (p))) -> ((~(q = 1) /\ forall bpr_left_pc_pen_list_complete_prime bpr_right_pc_pen_list_complete_prime. q = bpr_left_pc_pen_list_complete_prime * bpr_right_pc_pen_list_complete_prime -> bpr_left_pc_pen_list_complete_prime = 1 \/ bpr_right_pc_pen_list_complete_prime = 1)) -> (exists pc_le_pen_list_complete_bound. pc_le_pen_list_complete_bound + (q) = (p)) -> exists j. (exists pc_le_pen_list_complete_position. pc_le_pen_list_complete_position + (j) = (i)) /\ (((exists fs_h_pen_list_complete_found. fs_h_pen_list_complete_found + S (q) = S ((S (j)) * c)) /\ exists fs_q_pen_list_complete_found. b = fs_q_pen_list_complete_found * S ((S (j)) * c) + (q)))

Complete tactic proof in conservative notation

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

42 script commands · 10 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 exhausts primesinitial prime chain prefix restrict
01Fix variables and assumptionsL1–10

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 q
  7. L7
    intro hl
  8. L8
    intro hi
  9. L9
    intro hp
  10. L10
    intro hq
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hqp
03Separate the logical casesL12–13

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

  1. L12
    cases hl
  2. L13
    exfalso
04Calculate and transport equalitiesL14–14

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

  1. L14
    rewrite hl_left at hi
05Use earlier factsL15–20

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

  1. L15
    specialize lt_not_le i
  2. L16
    specialize lt_not_le 0
  3. L17
    apply lt_not_le
  4. L18
    exact hi
  5. L19
    specialize zero_le i
  6. L20
    apply zero_le
06Separate the logical casesL21–22

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

  1. L21
    cases hl_right
  2. L22
    cases hl_right_witness
07Use earlier factsL23–32

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

  1. L23
    specialize initial_prime_chain_exhausts_primes b
  2. L24
    specialize initial_prime_chain_exhausts_primes c
  3. L25
    specialize initial_prime_chain_exhausts_primes i
  4. L26
    specialize initial_prime_chain_exhausts_primes p
  5. L27
    specialize initial_prime_chain_exhausts_primes q
  6. L28
    apply initial_prime_chain_exhausts_primes
  7. L29
    specialize initial_prime_chain_prefix_restrict b
  8. L30
    specialize initial_prime_chain_prefix_restrict c
  9. L31
    specialize initial_prime_chain_prefix_restrict x
  10. L32
    specialize initial_prime_chain_prefix_restrict i
08Use earlier factsL33–36

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

  1. L33
    apply initial_prime_chain_prefix_restrict
  2. L34
    specialize le_of_succ_le_succ i
  3. L35
    specialize le_of_succ_le_succ x
  4. L36
    apply le_of_succ_le_succ
09Calculate and transport equalitiesL37–37

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

  1. L37
    rewrite hl_right_witness_left at hi
10Use earlier factsL38–42

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

  1. L38
    exact hi
  2. L39
    exact hl_right_witness_right
  3. L40
    exact hp
  4. L41
    exact hq
  5. L42
    exact hqp

Library-wide reading audit

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