PE0009

initial_prime_chain_prefix_restrict

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 1 declared prerequisite and contains 19 exact native proof lines.

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

Proof neighborhood

Direct dependencies

lt_of_lt_of_le Stable theorem; checked-use authorized

Direct dependents

PE000D initial_prime_chain_strict_order PE000E initial_prime_chain_exhausts_primes PE0010 prime_list_every_entry_is_prime PE0011 prime_list_omits_no_smaller_prime PE0012 prime_list_strictly_increasing

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

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.

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 exact 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