PE0008

initial_prime_chain_prefix_extend

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 82 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_prefix_extend Stable theorem; checked-use authorized zero_le Stable theorem; checked-use authorized succ_le_succ Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

Direct dependents

PE000B initial_prime_chain_bounded_exists

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

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.

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–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: LtBetaAt
  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 \/ (exists pc_lt_pen_extend_case. pc_lt_pen_extend_case + S (i) = (k))
  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: NextPrimeBetaAt
  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 exact 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 : exists z d. (((exists fs_h_pen_extend_entry. fs_h_pen_extend_entry + S (p) = S ((S (S k)) * d)) /\ exists fs_q_pen_extend_entry. z = fs_q_pen_extend_entry * S ((S (S k)) * d) + (p))) /\ (forall pen_index_extend_transfer pen_value_extend_transfer. (exists pc_lt_pen_extend_transfer_bound. pc_lt_pen_extend_transfer_bound + S (pen_index_extend_transfer) = (S k)) -> (((exists fs_h_pen_extend_transfer_old. fs_h_pen_extend_transfer_old + S (pen_value_extend_transfer) = S ((S (pen_index_extend_transfer)) * c)) /\ exists fs_q_pen_extend_transfer_old. b = fs_q_pen_extend_transfer_old * S ((S (pen_index_extend_transfer)) * c) + (pen_value_extend_transfer))) -> (((exists fs_h_pen_extend_transfer_new. fs_h_pen_extend_transfer_new + S (pen_value_extend_transfer) = S ((S (pen_index_extend_transfer)) * d)) /\ exists fs_q_pen_extend_transfer_new. z = fs_q_pen_extend_transfer_new * S ((S (pen_index_extend_transfer)) * d) + (pen_value_extend_transfer))))
  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 \/ (exists pc_lt_pen_extend_case. pc_lt_pen_extend_case + S (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 : exists u v. (((exists fs_h_pen_extend_old_left. fs_h_pen_extend_old_left + S (u) = S ((S (i)) * c)) /\ exists fs_q_pen_extend_old_left. b = fs_q_pen_extend_old_left * S ((S (i)) * c) + (u))) /\ ((((exists fs_h_pen_extend_old_right. fs_h_pen_extend_old_right + S (v) = S ((S (S i)) * c)) /\ exists fs_q_pen_extend_old_right. b = fs_q_pen_extend_old_right * S ((S (S i)) * c) + (v))) /\ (((~(v = 1) /\ forall bpr_left_pc_pen_extend_old_next_prime bpr_right_pc_pen_extend_old_next_prime. v = bpr_left_pc_pen_extend_old_next_prime * bpr_right_pc_pen_extend_old_next_prime -> bpr_left_pc_pen_extend_old_next_prime = 1 \/ bpr_right_pc_pen_extend_old_next_prime = 1)) /\ ((exists pc_lt_pen_extend_old_next_greater. pc_lt_pen_extend_old_next_greater + S (u) = (v)) /\ forall pen_comparison_extend_old_next. ((~(pen_comparison_extend_old_next = 1) /\ forall bpr_left_pc_pen_extend_old_next_comparison bpr_right_pc_pen_extend_old_next_comparison. pen_comparison_extend_old_next = bpr_left_pc_pen_extend_old_next_comparison * bpr_right_pc_pen_extend_old_next_comparison -> bpr_left_pc_pen_extend_old_next_comparison = 1 \/ bpr_right_pc_pen_extend_old_next_comparison = 1)) -> (exists pc_lt_pen_extend_old_next_above. pc_lt_pen_extend_old_next_above + S (u) = (pen_comparison_extend_old_next)) -> (exists pc_le_pen_extend_old_next_minimal. pc_le_pen_extend_old_next_minimal + (v) = (pen_comparison_extend_old_next)))))
  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