PE0009

initial_prime_chain_prefix_restrict

Every initial segment retains the same genuine least-prime transitions.

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. Le(i,k) → InitialPrimeChain(b,c,k) → InitialPrimeChain(b,c,i)

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

Definition DAG

InitialPrimeChain(b,c,k) · 2Le(a,b) · 1

Actual proof prerequisites

lt_of_lt_of_le · checked external prerequisite
Original expanded first-order statement 
forall b c k i. (exists pc_le_pen_restrict_bound. pc_le_pen_restrict_bound + (i) = (k)) -> ((((exists fs_h_pen_restrict_source_initial. fs_h_pen_restrict_source_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_restrict_source_initial. b = fs_q_pen_restrict_source_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_restrict_source. (exists pc_lt_pen_restrict_source_bound. pc_lt_pen_restrict_source_bound + S (pen_index_restrict_source) = (k)) -> exists pen_previous_restrict_source pen_following_restrict_source. (((exists fs_h_pen_restrict_source_previous. fs_h_pen_restrict_source_previous + S (pen_previous_restrict_source) = S ((S (pen_index_restrict_source)) * c)) /\ exists fs_q_pen_restrict_source_previous. b = fs_q_pen_restrict_source_previous * S ((S (pen_index_restrict_source)) * c) + (pen_previous_restrict_source))) /\ ((((exists fs_h_pen_restrict_source_following. fs_h_pen_restrict_source_following + S (pen_following_restrict_source) = S ((S (S pen_index_restrict_source)) * c)) /\ exists fs_q_pen_restrict_source_following. b = fs_q_pen_restrict_source_following * S ((S (S pen_index_restrict_source)) * c) + (pen_following_restrict_source))) /\ (((~(pen_following_restrict_source = 1) /\ forall bpr_left_pc_pen_restrict_source_next_prime bpr_right_pc_pen_restrict_source_next_prime. pen_following_restrict_source = bpr_left_pc_pen_restrict_source_next_prime * bpr_right_pc_pen_restrict_source_next_prime -> bpr_left_pc_pen_restrict_source_next_prime = 1 \/ bpr_right_pc_pen_restrict_source_next_prime = 1)) /\ ((exists pc_lt_pen_restrict_source_next_greater. pc_lt_pen_restrict_source_next_greater + S (pen_previous_restrict_source) = (pen_following_restrict_source)) /\ forall pen_comparison_restrict_source_next. ((~(pen_comparison_restrict_source_next = 1) /\ forall bpr_left_pc_pen_restrict_source_next_comparison bpr_right_pc_pen_restrict_source_next_comparison. pen_comparison_restrict_source_next = bpr_left_pc_pen_restrict_source_next_comparison * bpr_right_pc_pen_restrict_source_next_comparison -> bpr_left_pc_pen_restrict_source_next_comparison = 1 \/ bpr_right_pc_pen_restrict_source_next_comparison = 1)) -> (exists pc_lt_pen_restrict_source_next_above. pc_lt_pen_restrict_source_next_above + S (pen_previous_restrict_source) = (pen_comparison_restrict_source_next)) -> (exists pc_le_pen_restrict_source_next_minimal. pc_le_pen_restrict_source_next_minimal + (pen_following_restrict_source) = (pen_comparison_restrict_source_next)))))) -> ((((exists fs_h_pen_restrict_result_initial. fs_h_pen_restrict_result_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_restrict_result_initial. b = fs_q_pen_restrict_result_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_restrict_result. (exists pc_lt_pen_restrict_result_bound. pc_lt_pen_restrict_result_bound + S (pen_index_restrict_result) = (i)) -> exists pen_previous_restrict_result pen_following_restrict_result. (((exists fs_h_pen_restrict_result_previous. fs_h_pen_restrict_result_previous + S (pen_previous_restrict_result) = S ((S (pen_index_restrict_result)) * c)) /\ exists fs_q_pen_restrict_result_previous. b = fs_q_pen_restrict_result_previous * S ((S (pen_index_restrict_result)) * c) + (pen_previous_restrict_result))) /\ ((((exists fs_h_pen_restrict_result_following. fs_h_pen_restrict_result_following + S (pen_following_restrict_result) = S ((S (S pen_index_restrict_result)) * c)) /\ exists fs_q_pen_restrict_result_following. b = fs_q_pen_restrict_result_following * S ((S (S pen_index_restrict_result)) * c) + (pen_following_restrict_result))) /\ (((~(pen_following_restrict_result = 1) /\ forall bpr_left_pc_pen_restrict_result_next_prime bpr_right_pc_pen_restrict_result_next_prime. pen_following_restrict_result = bpr_left_pc_pen_restrict_result_next_prime * bpr_right_pc_pen_restrict_result_next_prime -> bpr_left_pc_pen_restrict_result_next_prime = 1 \/ bpr_right_pc_pen_restrict_result_next_prime = 1)) /\ ((exists pc_lt_pen_restrict_result_next_greater. pc_lt_pen_restrict_result_next_greater + S (pen_previous_restrict_result) = (pen_following_restrict_result)) /\ forall pen_comparison_restrict_result_next. ((~(pen_comparison_restrict_result_next = 1) /\ forall bpr_left_pc_pen_restrict_result_next_comparison bpr_right_pc_pen_restrict_result_next_comparison. pen_comparison_restrict_result_next = bpr_left_pc_pen_restrict_result_next_comparison * bpr_right_pc_pen_restrict_result_next_comparison -> bpr_left_pc_pen_restrict_result_next_comparison = 1 \/ bpr_right_pc_pen_restrict_result_next_comparison = 1)) -> (exists pc_lt_pen_restrict_result_next_above. pc_lt_pen_restrict_result_next_above + S (pen_previous_restrict_result) = (pen_comparison_restrict_result_next)) -> (exists pc_le_pen_restrict_result_next_minimal. pc_le_pen_restrict_result_next_minimal + (pen_following_restrict_result) = (pen_comparison_restrict_result_next))))))

Complete tactic proof in conservative notation

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

19 script commands · 5 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.

01Fix variables and assumptionsL1–6

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 hi
  6. L6
    intro hc
02Separate the logical casesL7–8

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

  1. L7
    cases hc
  2. L8
    split
03Use earlier factsL9–9

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

  1. L9
    exact hc_left
04Fix variables and assumptionsL10–11

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

  1. L10
    intro j
  2. L11
    intro hj
05Use earlier factsL12–19

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

  1. L12
    specialize hc_right j
  2. L13
    apply hc_right
  3. L14
    specialize lt_of_lt_of_le j
  4. L15
    specialize lt_of_lt_of_le i
  5. L16
    specialize lt_of_lt_of_le k
  6. L17
    apply lt_of_lt_of_le
  7. L18
    exact hj
  8. L19
    exact hi

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro k
  4. 0004intro i
  5. 0005intro hi
  6. 0006intro hc
  7. 0007cases hc
  8. 0008split
  9. 0009exact hc_left
  10. 0010intro j
  11. 0011intro hj
  12. 0012specialize hc_right j
  13. 0013apply hc_right
  14. 0014specialize lt_of_lt_of_le j
  15. 0015specialize lt_of_lt_of_le i
  16. 0016specialize lt_of_lt_of_le k
  17. 0017apply lt_of_lt_of_le
  18. 0018exact hj
  19. 0019exact hi