PE000A

initial_prime_chain_terminal_is_prime

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

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. ∀ p. InitialPrimeChain(b,c,k) → BetaAt(b,c,k,p) → Prime(p)

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

Definition DAG

NextPrime(a,p) · 1InitialPrimeChain(b,c,k) · 1Prime(p) · 1BetaAt(b,c,i,x) · 3

Actual proof prerequisites

beta_at_unique · checked external prerequisiteprime_two · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order 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))

Complete tactic proof in conservative notation

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

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.

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–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: BetaAt(b,c,k,a)BetaAt(b,c,S k,q)NextPrime(a,q)Original native command in the exact edition
  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 defined 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 : ∃ a. ∃ q. BetaAt(b,c,k,a) ∧ (BetaAt(b,c,S k,q) ∧ NextPrime(a,q))
  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