PE0012

prime_list_strictly_increasing

Every first-prime list is strictly increasing at all valid index pairs, not merely at its last transition.

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

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

Definition DAG

InitialPrimeList(b,c,k) · 1Lt(a,b) · 3BetaAt(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_strict_order
Original expanded first-order statement 
forall b c k i j p q. ((k = 0 \/ exists pen_last_index_list_order_source. k = S pen_last_index_list_order_source /\ ((((exists fs_h_pen_list_order_source_chain_initial. fs_h_pen_list_order_source_chain_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_list_order_source_chain_initial. b = fs_q_pen_list_order_source_chain_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_list_order_source_chain. (exists pc_lt_pen_list_order_source_chain_bound. pc_lt_pen_list_order_source_chain_bound + S (pen_index_list_order_source_chain) = (pen_last_index_list_order_source)) -> exists pen_previous_list_order_source_chain pen_following_list_order_source_chain. (((exists fs_h_pen_list_order_source_chain_previous. fs_h_pen_list_order_source_chain_previous + S (pen_previous_list_order_source_chain) = S ((S (pen_index_list_order_source_chain)) * c)) /\ exists fs_q_pen_list_order_source_chain_previous. b = fs_q_pen_list_order_source_chain_previous * S ((S (pen_index_list_order_source_chain)) * c) + (pen_previous_list_order_source_chain))) /\ ((((exists fs_h_pen_list_order_source_chain_following. fs_h_pen_list_order_source_chain_following + S (pen_following_list_order_source_chain) = S ((S (S pen_index_list_order_source_chain)) * c)) /\ exists fs_q_pen_list_order_source_chain_following. b = fs_q_pen_list_order_source_chain_following * S ((S (S pen_index_list_order_source_chain)) * c) + (pen_following_list_order_source_chain))) /\ (((~(pen_following_list_order_source_chain = 1) /\ forall bpr_left_pc_pen_list_order_source_chain_next_prime bpr_right_pc_pen_list_order_source_chain_next_prime. pen_following_list_order_source_chain = bpr_left_pc_pen_list_order_source_chain_next_prime * bpr_right_pc_pen_list_order_source_chain_next_prime -> bpr_left_pc_pen_list_order_source_chain_next_prime = 1 \/ bpr_right_pc_pen_list_order_source_chain_next_prime = 1)) /\ ((exists pc_lt_pen_list_order_source_chain_next_greater. pc_lt_pen_list_order_source_chain_next_greater + S (pen_previous_list_order_source_chain) = (pen_following_list_order_source_chain)) /\ forall pen_comparison_list_order_source_chain_next. ((~(pen_comparison_list_order_source_chain_next = 1) /\ forall bpr_left_pc_pen_list_order_source_chain_next_comparison bpr_right_pc_pen_list_order_source_chain_next_comparison. pen_comparison_list_order_source_chain_next = bpr_left_pc_pen_list_order_source_chain_next_comparison * bpr_right_pc_pen_list_order_source_chain_next_comparison -> bpr_left_pc_pen_list_order_source_chain_next_comparison = 1 \/ bpr_right_pc_pen_list_order_source_chain_next_comparison = 1)) -> (exists pc_lt_pen_list_order_source_chain_next_above. pc_lt_pen_list_order_source_chain_next_above + S (pen_previous_list_order_source_chain) = (pen_comparison_list_order_source_chain_next)) -> (exists pc_le_pen_list_order_source_chain_next_minimal. pc_le_pen_list_order_source_chain_next_minimal + (pen_following_list_order_source_chain) = (pen_comparison_list_order_source_chain_next)))))))) -> (exists pc_lt_pen_list_order_indices. pc_lt_pen_list_order_indices + S (i) = (j)) -> (exists pc_lt_pen_list_order_bound. pc_lt_pen_list_order_bound + S (j) = (k)) -> (((exists fs_h_pen_list_order_first. fs_h_pen_list_order_first + S (p) = S ((S (i)) * c)) /\ exists fs_q_pen_list_order_first. b = fs_q_pen_list_order_first * S ((S (i)) * c) + (p))) -> (((exists fs_h_pen_list_order_last. fs_h_pen_list_order_last + S (q) = S ((S (j)) * c)) /\ exists fs_q_pen_list_order_last. b = fs_q_pen_list_order_last * S ((S (j)) * c) + (q))) -> (exists pc_lt_pen_list_order_values. pc_lt_pen_list_order_values + S (p) = (q))

Complete tactic proof in conservative notation

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

44 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 strict orderinitial 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 j
  6. L6
    intro p
  7. L7
    intro q
  8. L8
    intro hl
  9. L9
    intro hij
  10. L10
    intro hj
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hp
  2. L12
    intro hq
03Separate the logical casesL13–14

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

  1. L13
    cases hl
  2. L14
    exfalso
04Calculate and transport equalitiesL15–15

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

  1. L15
    rewrite hl_left at hj
05Use earlier factsL16–21

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

  1. L16
    specialize lt_not_le j
  2. L17
    specialize lt_not_le 0
  3. L18
    apply lt_not_le
  4. L19
    exact hj
  5. L20
    specialize zero_le j
  6. L21
    apply zero_le
06Separate the logical casesL22–23

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

  1. L22
    cases hl_right
  2. L23
    cases hl_right_witness
07Use earlier factsL24–33

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

  1. L24
    specialize initial_prime_chain_strict_order b
  2. L25
    specialize initial_prime_chain_strict_order c
  3. L26
    specialize initial_prime_chain_strict_order j
  4. L27
    specialize initial_prime_chain_strict_order i
  5. L28
    specialize initial_prime_chain_strict_order p
  6. L29
    specialize initial_prime_chain_strict_order q
  7. L30
    apply initial_prime_chain_strict_order
  8. L31
    specialize initial_prime_chain_prefix_restrict b
  9. L32
    specialize initial_prime_chain_prefix_restrict c
  10. L33
    specialize initial_prime_chain_prefix_restrict x
08Use earlier factsL34–38

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

  1. L34
    specialize initial_prime_chain_prefix_restrict j
  2. L35
    apply initial_prime_chain_prefix_restrict
  3. L36
    specialize le_of_succ_le_succ j
  4. L37
    specialize le_of_succ_le_succ x
  5. L38
    apply le_of_succ_le_succ
09Calculate and transport equalitiesL39–39

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

  1. L39
    rewrite hl_right_witness_left at hj
10Use earlier factsL40–44

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

  1. L40
    exact hj
  2. L41
    exact hl_right_witness_right
  3. L42
    exact hij
  4. L43
    exact hp
  5. L44
    exact hq

Library-wide reading audit

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