PE0010

prime_list_every_entry_is_prime

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

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

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. ((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))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 36 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 PE000A initial_prime_chain_terminal_is_prime

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

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.

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