PE000A

initial_prime_chain_terminal_is_prime

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

Every decoded terminal entry of an initial-prime chain is genuinely prime, including the first entry two.

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 p. ((((exists fs_h_pen_terminal_source_initial. fs_h_pen_terminal_source_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_terminal_source_initial. b = fs_q_pen_terminal_source_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_terminal_source. (exists pc_lt_pen_terminal_source_bound. pc_lt_pen_terminal_source_bound + S (pen_index_terminal_source) = (k)) -> exists pen_previous_terminal_source pen_following_terminal_source. (((exists fs_h_pen_terminal_source_previous. fs_h_pen_terminal_source_previous + S (pen_previous_terminal_source) = S ((S (pen_index_terminal_source)) * c)) /\ exists fs_q_pen_terminal_source_previous. b = fs_q_pen_terminal_source_previous * S ((S (pen_index_terminal_source)) * c) + (pen_previous_terminal_source))) /\ ((((exists fs_h_pen_terminal_source_following. fs_h_pen_terminal_source_following + S (pen_following_terminal_source) = S ((S (S pen_index_terminal_source)) * c)) /\ exists fs_q_pen_terminal_source_following. b = fs_q_pen_terminal_source_following * S ((S (S pen_index_terminal_source)) * c) + (pen_following_terminal_source))) /\ (((~(pen_following_terminal_source = 1) /\ forall bpr_left_pc_pen_terminal_source_next_prime bpr_right_pc_pen_terminal_source_next_prime. pen_following_terminal_source = bpr_left_pc_pen_terminal_source_next_prime * bpr_right_pc_pen_terminal_source_next_prime -> bpr_left_pc_pen_terminal_source_next_prime = 1 \/ bpr_right_pc_pen_terminal_source_next_prime = 1)) /\ ((exists pc_lt_pen_terminal_source_next_greater. pc_lt_pen_terminal_source_next_greater + S (pen_previous_terminal_source) = (pen_following_terminal_source)) /\ forall pen_comparison_terminal_source_next. ((~(pen_comparison_terminal_source_next = 1) /\ forall bpr_left_pc_pen_terminal_source_next_comparison bpr_right_pc_pen_terminal_source_next_comparison. pen_comparison_terminal_source_next = bpr_left_pc_pen_terminal_source_next_comparison * bpr_right_pc_pen_terminal_source_next_comparison -> bpr_left_pc_pen_terminal_source_next_comparison = 1 \/ bpr_right_pc_pen_terminal_source_next_comparison = 1)) -> (exists pc_lt_pen_terminal_source_next_above. pc_lt_pen_terminal_source_next_above + S (pen_previous_terminal_source) = (pen_comparison_terminal_source_next)) -> (exists pc_le_pen_terminal_source_next_minimal. pc_le_pen_terminal_source_next_minimal + (pen_following_terminal_source) = (pen_comparison_terminal_source_next)))))) -> (((exists fs_h_pen_terminal_entry. fs_h_pen_terminal_entry + S (p) = S ((S (k)) * c)) /\ exists fs_q_pen_terminal_entry. b = fs_q_pen_terminal_entry * S ((S (k)) * c) + (p))) -> ((~(p = 1) /\ forall bpr_left_pc_pen_terminal_prime bpr_right_pc_pen_terminal_prime. p = bpr_left_pc_pen_terminal_prime * bpr_right_pc_pen_terminal_prime -> bpr_left_pc_pen_terminal_prime = 1 \/ bpr_right_pc_pen_terminal_prime = 1))

Constructive proof overview

Generated structural guide

Every decoded terminal entry of an initial-prime chain is genuinely prime, including the first entry two.

The unchanged tactic script uses 3 declared prerequisites and contains 45 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized prime_two Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized

Direct dependents

PE000B initial_prime_chain_bounded_exists PE0010 prime_list_every_entry_is_prime

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

45 script commands · 13 reading checkpoints · 3 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on kL3–6

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction k
  2. L4
    intro p
  3. L5
    intro hc
  4. L6
    intro hp
03Separate the logical casesL7–7

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

  1. L7
    cases hc
04Establish hp2L8–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L8
    have hp2 : p = 2
  2. L9
    specialize beta_at_unique b
  3. L10
    specialize beta_at_unique c
  4. L11
    specialize beta_at_unique 0
  5. L12
    specialize beta_at_unique p
  6. L13
    specialize beta_at_unique 2
  7. L14
    apply beta_at_unique
  8. L15
    exact hp
  9. L16
    exact hc_left
  10. L17
    rewrite hp2
05Calculate and transport equalitiesL18–18

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

  1. L18
    rewrite hp2
06Use earlier factsL19–19

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

  1. L19
    exact prime_two
07Fix variables and assumptionsL20–22

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

  1. L20
    intro p
  2. L21
    intro hc
  3. L22
    intro hp
08Separate the logical casesL23–23

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

  1. L23
    cases hc
09Establish heL24–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hc right.

  1. L24
    have he : ∃ a. ∃ q. BetaAt(b,c,k,a) ∧ (BetaAt(b,c,S k,q) ∧ NextPrime(a,q))Definitions: NextPrimeBetaAt
  2. L25
    specialize hc_right k
  3. L26
    apply hc_right
  4. L27
    specialize le_refl (S k)
  5. L28
    apply le_refl
10Separate the logical casesL29–33

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

  1. L29
    cases he
  2. L30
    cases he_witness
  3. L31
    cases he_witness_witness
  4. L32
    cases he_witness_witness_right
  5. L33
    cases he_witness_witness_right_right
11Establish heqL34–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L34
    have heq : p = x1
  2. L35
    specialize beta_at_unique b
  3. L36
    specialize beta_at_unique c
  4. L37
    specialize beta_at_unique (S k)
  5. L38
    specialize beta_at_unique p
  6. L39
    specialize beta_at_unique x1
  7. L40
    apply beta_at_unique
  8. L41
    exact hp
  9. L42
    exact he_witness_witness_right_left
  10. L43
    rewrite heq
12Calculate and transport equalitiesL44–44

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

  1. L44
    rewrite heq
13Use earlier factsL45–45

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

  1. L45
    exact he_witness_witness_right_right_left

Library-wide reading audit

Original exact command ledger · 45 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction k
  4. 0004intro p
  5. 0005intro hc
  6. 0006intro hp
  7. 0007cases hc
  8. 0008have hp2 : p = 2
  9. 0009specialize beta_at_unique b
  10. 0010specialize beta_at_unique c
  11. 0011specialize beta_at_unique 0
  12. 0012specialize beta_at_unique p
  13. 0013specialize beta_at_unique 2
  14. 0014apply beta_at_unique
  15. 0015exact hp
  16. 0016exact hc_left
  17. 0017rewrite hp2
  18. 0018rewrite hp2
  19. 0019exact prime_two
  20. 0020intro p
  21. 0021intro hc
  22. 0022intro hp
  23. 0023cases hc
  24. 0024have he : exists a q. (((exists fs_h_pen_terminal_previous. fs_h_pen_terminal_previous + S (a) = S ((S (k)) * c)) /\ exists fs_q_pen_terminal_previous. b = fs_q_pen_terminal_previous * S ((S (k)) * c) + (a))) /\ ((((exists fs_h_pen_terminal_last. fs_h_pen_terminal_last + S (q) = S ((S (S k)) * c)) /\ exists fs_q_pen_terminal_last. b = fs_q_pen_terminal_last * S ((S (S k)) * c) + (q))) /\ (((~(q = 1) /\ forall bpr_left_pc_pen_terminal_next_prime bpr_right_pc_pen_terminal_next_prime. q = bpr_left_pc_pen_terminal_next_prime * bpr_right_pc_pen_terminal_next_prime -> bpr_left_pc_pen_terminal_next_prime = 1 \/ bpr_right_pc_pen_terminal_next_prime = 1)) /\ ((exists pc_lt_pen_terminal_next_greater. pc_lt_pen_terminal_next_greater + S (a) = (q)) /\ forall pen_comparison_terminal_next. ((~(pen_comparison_terminal_next = 1) /\ forall bpr_left_pc_pen_terminal_next_comparison bpr_right_pc_pen_terminal_next_comparison. pen_comparison_terminal_next = bpr_left_pc_pen_terminal_next_comparison * bpr_right_pc_pen_terminal_next_comparison -> bpr_left_pc_pen_terminal_next_comparison = 1 \/ bpr_right_pc_pen_terminal_next_comparison = 1)) -> (exists pc_lt_pen_terminal_next_above. pc_lt_pen_terminal_next_above + S (a) = (pen_comparison_terminal_next)) -> (exists pc_le_pen_terminal_next_minimal. pc_le_pen_terminal_next_minimal + (q) = (pen_comparison_terminal_next)))))
  25. 0025specialize hc_right k
  26. 0026apply hc_right
  27. 0027specialize le_refl (S k)
  28. 0028apply le_refl
  29. 0029cases he
  30. 0030cases he_witness
  31. 0031cases he_witness_witness
  32. 0032cases he_witness_witness_right
  33. 0033cases he_witness_witness_right_right
  34. 0034have heq : p = x1
  35. 0035specialize beta_at_unique b
  36. 0036specialize beta_at_unique c
  37. 0037specialize beta_at_unique (S k)
  38. 0038specialize beta_at_unique p
  39. 0039specialize beta_at_unique x1
  40. 0040apply beta_at_unique
  41. 0041exact hp
  42. 0042exact he_witness_witness_right_left
  43. 0043rewrite heq
  44. 0044rewrite heq
  45. 0045exact he_witness_witness_right_right_left