PE0011

prime_list_omits_no_smaller_prime

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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.

Exact expanded first-order arithmetic 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)))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 42 exact native proof lines.

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

Proof neighborhood

Direct dependencies

lt_not_le Stable theorem; checked-use authorized zero_le Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized PE0009 initial_prime_chain_prefix_restrict PE000E initial_prime_chain_exhausts_primes

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (2)
initial prime chain prefix restrictinitial prime chain exhausts primes
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 exact 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