PE0008

initial_prime_chain_prefix_extend

Appending the actual next prime preserves every old decoded entry and every minimal-successor edge.

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

∀ k. ∀ b. ∀ c. ∀ a. ∀ p. InitialPrimeChain(b,c,k) → BetaAt(b,c,k,a) → NextPrime(a,p) → ∃ x. ∃ y. InitialPrimeChain(x,y,S k) ∧ BetaAt(x,y,S k,p)

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

Definition DAG

NextPrime(a,p) · 2InitialPrimeChain(b,c,k) · 2Lt(a,b) · 2BetaAt(b,c,i,x) · 7

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitezero_le · checked external prerequisitesucc_le_succ · checked external prerequisitele_refl · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall k b c a p. ((((exists fs_h_pen_extend_before_initial. fs_h_pen_extend_before_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_extend_before_initial. b = fs_q_pen_extend_before_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_extend_before. (exists pc_lt_pen_extend_before_bound. pc_lt_pen_extend_before_bound + S (pen_index_extend_before) = (k)) -> exists pen_previous_extend_before pen_following_extend_before. (((exists fs_h_pen_extend_before_previous. fs_h_pen_extend_before_previous + S (pen_previous_extend_before) = S ((S (pen_index_extend_before)) * c)) /\ exists fs_q_pen_extend_before_previous. b = fs_q_pen_extend_before_previous * S ((S (pen_index_extend_before)) * c) + (pen_previous_extend_before))) /\ ((((exists fs_h_pen_extend_before_following. fs_h_pen_extend_before_following + S (pen_following_extend_before) = S ((S (S pen_index_extend_before)) * c)) /\ exists fs_q_pen_extend_before_following. b = fs_q_pen_extend_before_following * S ((S (S pen_index_extend_before)) * c) + (pen_following_extend_before))) /\ (((~(pen_following_extend_before = 1) /\ forall bpr_left_pc_pen_extend_before_next_prime bpr_right_pc_pen_extend_before_next_prime. pen_following_extend_before = bpr_left_pc_pen_extend_before_next_prime * bpr_right_pc_pen_extend_before_next_prime -> bpr_left_pc_pen_extend_before_next_prime = 1 \/ bpr_right_pc_pen_extend_before_next_prime = 1)) /\ ((exists pc_lt_pen_extend_before_next_greater. pc_lt_pen_extend_before_next_greater + S (pen_previous_extend_before) = (pen_following_extend_before)) /\ forall pen_comparison_extend_before_next. ((~(pen_comparison_extend_before_next = 1) /\ forall bpr_left_pc_pen_extend_before_next_comparison bpr_right_pc_pen_extend_before_next_comparison. pen_comparison_extend_before_next = bpr_left_pc_pen_extend_before_next_comparison * bpr_right_pc_pen_extend_before_next_comparison -> bpr_left_pc_pen_extend_before_next_comparison = 1 \/ bpr_right_pc_pen_extend_before_next_comparison = 1)) -> (exists pc_lt_pen_extend_before_next_above. pc_lt_pen_extend_before_next_above + S (pen_previous_extend_before) = (pen_comparison_extend_before_next)) -> (exists pc_le_pen_extend_before_next_minimal. pc_le_pen_extend_before_next_minimal + (pen_following_extend_before) = (pen_comparison_extend_before_next)))))) -> (((exists fs_h_pen_extend_terminal. fs_h_pen_extend_terminal + S (a) = S ((S (k)) * c)) /\ exists fs_q_pen_extend_terminal. b = fs_q_pen_extend_terminal * S ((S (k)) * c) + (a))) -> (((~(p = 1) /\ forall bpr_left_pc_pen_extend_next_prime bpr_right_pc_pen_extend_next_prime. p = bpr_left_pc_pen_extend_next_prime * bpr_right_pc_pen_extend_next_prime -> bpr_left_pc_pen_extend_next_prime = 1 \/ bpr_right_pc_pen_extend_next_prime = 1)) /\ ((exists pc_lt_pen_extend_next_greater. pc_lt_pen_extend_next_greater + S (a) = (p)) /\ forall pen_comparison_extend_next. ((~(pen_comparison_extend_next = 1) /\ forall bpr_left_pc_pen_extend_next_comparison bpr_right_pc_pen_extend_next_comparison. pen_comparison_extend_next = bpr_left_pc_pen_extend_next_comparison * bpr_right_pc_pen_extend_next_comparison -> bpr_left_pc_pen_extend_next_comparison = 1 \/ bpr_right_pc_pen_extend_next_comparison = 1)) -> (exists pc_lt_pen_extend_next_above. pc_lt_pen_extend_next_above + S (a) = (pen_comparison_extend_next)) -> (exists pc_le_pen_extend_next_minimal. pc_le_pen_extend_next_minimal + (p) = (pen_comparison_extend_next)))) -> exists z d. ((((exists fs_h_pen_extend_after_initial. fs_h_pen_extend_after_initial + S (2) = S ((S (0)) * d)) /\ exists fs_q_pen_extend_after_initial. z = fs_q_pen_extend_after_initial * S ((S (0)) * d) + (2))) /\ forall pen_index_extend_after. (exists pc_lt_pen_extend_after_bound. pc_lt_pen_extend_after_bound + S (pen_index_extend_after) = (S k)) -> exists pen_previous_extend_after pen_following_extend_after. (((exists fs_h_pen_extend_after_previous. fs_h_pen_extend_after_previous + S (pen_previous_extend_after) = S ((S (pen_index_extend_after)) * d)) /\ exists fs_q_pen_extend_after_previous. z = fs_q_pen_extend_after_previous * S ((S (pen_index_extend_after)) * d) + (pen_previous_extend_after))) /\ ((((exists fs_h_pen_extend_after_following. fs_h_pen_extend_after_following + S (pen_following_extend_after) = S ((S (S pen_index_extend_after)) * d)) /\ exists fs_q_pen_extend_after_following. z = fs_q_pen_extend_after_following * S ((S (S pen_index_extend_after)) * d) + (pen_following_extend_after))) /\ (((~(pen_following_extend_after = 1) /\ forall bpr_left_pc_pen_extend_after_next_prime bpr_right_pc_pen_extend_after_next_prime. pen_following_extend_after = bpr_left_pc_pen_extend_after_next_prime * bpr_right_pc_pen_extend_after_next_prime -> bpr_left_pc_pen_extend_after_next_prime = 1 \/ bpr_right_pc_pen_extend_after_next_prime = 1)) /\ ((exists pc_lt_pen_extend_after_next_greater. pc_lt_pen_extend_after_next_greater + S (pen_previous_extend_after) = (pen_following_extend_after)) /\ forall pen_comparison_extend_after_next. ((~(pen_comparison_extend_after_next = 1) /\ forall bpr_left_pc_pen_extend_after_next_comparison bpr_right_pc_pen_extend_after_next_comparison. pen_comparison_extend_after_next = bpr_left_pc_pen_extend_after_next_comparison * bpr_right_pc_pen_extend_after_next_comparison -> bpr_left_pc_pen_extend_after_next_comparison = 1 \/ bpr_right_pc_pen_extend_after_next_comparison = 1)) -> (exists pc_lt_pen_extend_after_next_above. pc_lt_pen_extend_after_next_above + S (pen_previous_extend_after) = (pen_comparison_extend_after_next)) -> (exists pc_le_pen_extend_after_next_minimal. pc_le_pen_extend_after_next_minimal + (pen_following_extend_after) = (pen_comparison_extend_after_next)))))) /\ (((exists fs_h_pen_extend_new_terminal. fs_h_pen_extend_new_terminal + S (p) = S ((S (S k)) * d)) /\ exists fs_q_pen_extend_new_terminal. z = fs_q_pen_extend_new_terminal * S ((S (S k)) * d) + (p)))

Complete tactic proof in conservative notation

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

82 script commands · 24 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–8

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

  1. L1
    intro k
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro a
  5. L5
    intro p
  6. L6
    intro hc
  7. L7
    intro ha
  8. L8
    intro hp
02Separate the logical casesL9–9

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

  1. L9
    cases hc
03Establish heL10–15

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

  1. L10
    have he : ∃ z. ∃ d. BetaAt(z,d,S k,p) ∧ (∀ x. ∀ y. Lt(x,S k) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))Definitions: BetaAt(z,d,S k,p)Lt(x,S k)BetaAt(b,c,x,y)BetaAt(z,d,x,y)Original native command in the exact edition
  2. L11
    specialize beta_prefix_extend (S k)
  3. L12
    specialize beta_prefix_extend b
  4. L13
    specialize beta_prefix_extend c
  5. L14
    specialize beta_prefix_extend p
  6. L15
    apply beta_prefix_extend
04Separate the logical casesL16–18

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

  1. L16
    cases he
  2. L17
    cases he_witness
  3. L18
    cases he_witness_witness
05Construct an explicit witnessL19–20

Supply the displayed value, then prove that it has the required property.

  1. L19
    exists x
  2. L20
    exists x1
06Separate the logical casesL21–22

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

  1. L21
    split
  2. L22
    split
07Use earlier factsL23–31

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

  1. L23
    specialize he_witness_witness_right 0
  2. L24
    specialize he_witness_witness_right 2
  3. L25
    apply he_witness_witness_right
  4. L26
    specialize succ_le_succ 0
  5. L27
    specialize succ_le_succ k
  6. L28
    apply succ_le_succ
  7. L29
    specialize zero_le k
  8. L30
    apply zero_le
  9. L31
    exact hc_left
08Fix variables and assumptionsL32–33

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

  1. L32
    intro i
  2. L33
    intro hi
09Establish hsL34–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L34
    have hs : i = k ∨ Lt(i,k)Definitions: Lt(i,k)Original native command in the exact edition
  2. L35
    specialize finite_lt_succ_eq_or_lt k
  3. L36
    specialize finite_lt_succ_eq_or_lt i
  4. L37
    apply finite_lt_succ_eq_or_lt
  5. L38
    exact hi
10Separate the logical casesL39–39

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

  1. L39
    cases hs
11Construct an explicit witnessL40–41

Supply the displayed value, then prove that it has the required property.

  1. L40
    exists a
  2. L41
    exists p
12Separate the logical casesL42–42

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

  1. L42
    split
13Calculate and transport equalitiesL43–44

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

  1. L43
    rewrite hs_left
  2. L44
    rewrite hs_left
14Use earlier factsL45–50

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

  1. L45
    specialize he_witness_witness_right k
  2. L46
    specialize he_witness_witness_right a
  3. L47
    apply he_witness_witness_right
  4. L48
    specialize le_refl (S k)
  5. L49
    apply le_refl
  6. L50
    exact ha
15Separate the logical casesL51–51

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

  1. L51
    split
16Calculate and transport equalitiesL52–53

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

  1. L52
    rewrite hs_left
  2. L53
    rewrite hs_left
17Use earlier factsL54–55

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

  1. L54
    exact he_witness_witness_left
  2. L55
    exact hp
18Establish holdL56–59

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

  1. L56
    have hold : ∃ u. ∃ v. BetaAt(b,c,i,u) ∧ (BetaAt(b,c,S i,v) ∧ NextPrime(u,v))Definitions: BetaAt(b,c,i,u)BetaAt(b,c,S i,v)NextPrime(u,v)Original native command in the exact edition
  2. L57
    specialize hc_right i
  3. L58
    apply hc_right
  4. L59
    exact hs_right
19Separate the logical casesL60–63

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

  1. L60
    cases hold
  2. L61
    cases hold_witness
  3. L62
    cases hold_witness_witness
  4. L63
    cases hold_witness_witness_right
20Construct an explicit witnessL64–65

Supply the displayed value, then prove that it has the required property.

  1. L64
    exists x2
  2. L65
    exists x3
21Separate the logical casesL66–66

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

  1. L66
    split
22Use earlier factsL67–71

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

  1. L67
    specialize he_witness_witness_right i
  2. L68
    specialize he_witness_witness_right x2
  3. L69
    apply he_witness_witness_right
  4. L70
    exact hi
  5. L71
    exact hold_witness_witness_left
23Separate the logical casesL72–72

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

  1. L72
    split
24Use earlier factsL73–82

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

  1. L73
    specialize he_witness_witness_right (S i)
  2. L74
    specialize he_witness_witness_right x3
  3. L75
    apply he_witness_witness_right
  4. L76
    specialize succ_le_succ (S i)
  5. L77
    specialize succ_le_succ k
  6. L78
    apply succ_le_succ
  7. L79
    exact hs_right
  8. L80
    exact hold_witness_witness_right_left
  9. L81
    exact hold_witness_witness_right_right
  10. L82
    exact he_witness_witness_left

Library-wide reading audit

Original defined command ledger · 82 lines
  1. 0001intro k
  2. 0002intro b
  3. 0003intro c
  4. 0004intro a
  5. 0005intro p
  6. 0006intro hc
  7. 0007intro ha
  8. 0008intro hp
  9. 0009cases hc
  10. 0010have he : ∃ z. ∃ d. BetaAt(z,d,S k,p) ∧ (∀ x. ∀ y. Lt(x,S k) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))
  11. 0011specialize beta_prefix_extend (S k)
  12. 0012specialize beta_prefix_extend b
  13. 0013specialize beta_prefix_extend c
  14. 0014specialize beta_prefix_extend p
  15. 0015apply beta_prefix_extend
  16. 0016cases he
  17. 0017cases he_witness
  18. 0018cases he_witness_witness
  19. 0019exists x
  20. 0020exists x1
  21. 0021split
  22. 0022split
  23. 0023specialize he_witness_witness_right 0
  24. 0024specialize he_witness_witness_right 2
  25. 0025apply he_witness_witness_right
  26. 0026specialize succ_le_succ 0
  27. 0027specialize succ_le_succ k
  28. 0028apply succ_le_succ
  29. 0029specialize zero_le k
  30. 0030apply zero_le
  31. 0031exact hc_left
  32. 0032intro i
  33. 0033intro hi
  34. 0034have hs : i = k ∨ Lt(i,k)
  35. 0035specialize finite_lt_succ_eq_or_lt k
  36. 0036specialize finite_lt_succ_eq_or_lt i
  37. 0037apply finite_lt_succ_eq_or_lt
  38. 0038exact hi
  39. 0039cases hs
  40. 0040exists a
  41. 0041exists p
  42. 0042split
  43. 0043rewrite hs_left
  44. 0044rewrite hs_left
  45. 0045specialize he_witness_witness_right k
  46. 0046specialize he_witness_witness_right a
  47. 0047apply he_witness_witness_right
  48. 0048specialize le_refl (S k)
  49. 0049apply le_refl
  50. 0050exact ha
  51. 0051split
  52. 0052rewrite hs_left
  53. 0053rewrite hs_left
  54. 0054exact he_witness_witness_left
  55. 0055exact hp
  56. 0056have hold : ∃ u. ∃ v. BetaAt(b,c,i,u) ∧ (BetaAt(b,c,S i,v) ∧ NextPrime(u,v))
  57. 0057specialize hc_right i
  58. 0058apply hc_right
  59. 0059exact hs_right
  60. 0060cases hold
  61. 0061cases hold_witness
  62. 0062cases hold_witness_witness
  63. 0063cases hold_witness_witness_right
  64. 0064exists x2
  65. 0065exists x3
  66. 0066split
  67. 0067specialize he_witness_witness_right i
  68. 0068specialize he_witness_witness_right x2
  69. 0069apply he_witness_witness_right
  70. 0070exact hi
  71. 0071exact hold_witness_witness_left
  72. 0072split
  73. 0073specialize he_witness_witness_right (S i)
  74. 0074specialize he_witness_witness_right x3
  75. 0075apply he_witness_witness_right
  76. 0076specialize succ_le_succ (S i)
  77. 0077specialize succ_le_succ k
  78. 0078apply succ_le_succ
  79. 0079exact hs_right
  80. 0080exact hold_witness_witness_right_left
  81. 0081exact hold_witness_witness_right_right
  82. 0082exact he_witness_witness_left