PE000D

initial_prime_chain_strict_order

Every earlier decoded prime is strictly smaller than the terminal prime; repetitions and descending lists are excluded.

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

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

Definition DAG

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

Actual proof prerequisites

lt_not_le · checked external prerequisitezero_le · checked external prerequisiteinitial_prime_chain_prefix_restrictle_succ_self · checked external prerequisitele_refl · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisitelt_trans · checked external prerequisite
Original expanded first-order statement 
forall b c k i p q. ((((exists fs_h_pen_order_chain_initial. fs_h_pen_order_chain_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_order_chain_initial. b = fs_q_pen_order_chain_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_order_chain. (exists pc_lt_pen_order_chain_bound. pc_lt_pen_order_chain_bound + S (pen_index_order_chain) = (k)) -> exists pen_previous_order_chain pen_following_order_chain. (((exists fs_h_pen_order_chain_previous. fs_h_pen_order_chain_previous + S (pen_previous_order_chain) = S ((S (pen_index_order_chain)) * c)) /\ exists fs_q_pen_order_chain_previous. b = fs_q_pen_order_chain_previous * S ((S (pen_index_order_chain)) * c) + (pen_previous_order_chain))) /\ ((((exists fs_h_pen_order_chain_following. fs_h_pen_order_chain_following + S (pen_following_order_chain) = S ((S (S pen_index_order_chain)) * c)) /\ exists fs_q_pen_order_chain_following. b = fs_q_pen_order_chain_following * S ((S (S pen_index_order_chain)) * c) + (pen_following_order_chain))) /\ (((~(pen_following_order_chain = 1) /\ forall bpr_left_pc_pen_order_chain_next_prime bpr_right_pc_pen_order_chain_next_prime. pen_following_order_chain = bpr_left_pc_pen_order_chain_next_prime * bpr_right_pc_pen_order_chain_next_prime -> bpr_left_pc_pen_order_chain_next_prime = 1 \/ bpr_right_pc_pen_order_chain_next_prime = 1)) /\ ((exists pc_lt_pen_order_chain_next_greater. pc_lt_pen_order_chain_next_greater + S (pen_previous_order_chain) = (pen_following_order_chain)) /\ forall pen_comparison_order_chain_next. ((~(pen_comparison_order_chain_next = 1) /\ forall bpr_left_pc_pen_order_chain_next_comparison bpr_right_pc_pen_order_chain_next_comparison. pen_comparison_order_chain_next = bpr_left_pc_pen_order_chain_next_comparison * bpr_right_pc_pen_order_chain_next_comparison -> bpr_left_pc_pen_order_chain_next_comparison = 1 \/ bpr_right_pc_pen_order_chain_next_comparison = 1)) -> (exists pc_lt_pen_order_chain_next_above. pc_lt_pen_order_chain_next_above + S (pen_previous_order_chain) = (pen_comparison_order_chain_next)) -> (exists pc_le_pen_order_chain_next_minimal. pc_le_pen_order_chain_next_minimal + (pen_following_order_chain) = (pen_comparison_order_chain_next)))))) -> (exists pc_lt_pen_order_indices. pc_lt_pen_order_indices + S (i) = (k)) -> (((exists fs_h_pen_order_first. fs_h_pen_order_first + S (p) = S ((S (i)) * c)) /\ exists fs_q_pen_order_first. b = fs_q_pen_order_first * S ((S (i)) * c) + (p))) -> (((exists fs_h_pen_order_last. fs_h_pen_order_last + S (q) = S ((S (k)) * c)) /\ exists fs_q_pen_order_last. b = fs_q_pen_order_last * S ((S (k)) * c) + (q))) -> (exists pc_lt_pen_order_values. pc_lt_pen_order_values + S (p) = (q))

Complete tactic proof in conservative notation

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

87 script commands · 17 reading checkpoints · 5 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.

Named ingredients (1)
initial prime chain prefix restrict
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–10

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 i
  3. L5
    intro p
  4. L6
    intro q
  5. L7
    intro hc
  6. L8
    intro hi
  7. L9
    intro hp
  8. L10
    intro hq
03Separate the logical casesL11–11

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

  1. L11
    exfalso
04Use earlier factsL12–17

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

  1. L12
    specialize lt_not_le i
  2. L13
    specialize lt_not_le 0
  3. L14
    apply lt_not_le
  4. L15
    exact hi
  5. L16
    specialize zero_le i
  6. L17
    apply zero_le
05Fix variables and assumptionsL18–24

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

  1. L18
    intro i
  2. L19
    intro p
  3. L20
    intro q
  4. L21
    intro hc
  5. L22
    intro hi
  6. L23
    intro hp
  7. L24
    intro hq
06Establish hrL25–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply initial prime chain prefix restrict.

  1. L25
    have hr : InitialPrimeChain(b,c,k)Definitions: InitialPrimeChain(b,c,k)Original native command in the exact edition
  2. L26
    specialize initial_prime_chain_prefix_restrict b
  3. L27
    specialize initial_prime_chain_prefix_restrict c
  4. L28
    specialize initial_prime_chain_prefix_restrict (S k)
  5. L29
    specialize initial_prime_chain_prefix_restrict k
  6. L30
    apply initial_prime_chain_prefix_restrict
  7. L31
    specialize le_succ_self k
  8. L32
    apply le_succ_self
  9. L33
    exact hc
07Separate the logical casesL34–34

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

  1. L34
    cases hc
08Establish heL35–39

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

  1. L35
    have he : ∃ a. ∃ t. BetaAt(b,c,k,a) ∧ (BetaAt(b,c,S k,t) ∧ NextPrime(a,t))Definitions: BetaAt(b,c,k,a)BetaAt(b,c,S k,t)NextPrime(a,t)Original native command in the exact edition
  2. L36
    specialize hc_right k
  3. L37
    apply hc_right
  4. L38
    specialize le_refl (S k)
  5. L39
    apply le_refl
09Separate the logical casesL40–45

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

  1. L40
    cases he
  2. L41
    cases he_witness
  3. L42
    cases he_witness_witness
  4. L43
    cases he_witness_witness_right
  5. L44
    cases he_witness_witness_right_right
  6. L45
    cases he_witness_witness_right_right_right
10Establish hqeqL46–55

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

  1. L46
    have hqeq : q = x1
  2. L47
    specialize beta_at_unique b
  3. L48
    specialize beta_at_unique c
  4. L49
    specialize beta_at_unique (S k)
  5. L50
    specialize beta_at_unique q
  6. L51
    specialize beta_at_unique x1
  7. L52
    apply beta_at_unique
  8. L53
    exact hq
  9. L54
    exact he_witness_witness_right_left
  10. L55
    rewrite hqeq
11Establish hsL56–60

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. L56
    have hs : i = k ∨ Lt(i,k)Definitions: Lt(i,k)Original native command in the exact edition
  2. L57
    specialize finite_lt_succ_eq_or_lt k
  3. L58
    specialize finite_lt_succ_eq_or_lt i
  4. L59
    apply finite_lt_succ_eq_or_lt
  5. L60
    exact hi
12Separate the logical casesL61–61

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

  1. L61
    cases hs
13Establish hpeqL62–71

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

  1. L62
    have hpeq : p = x
  2. L63
    specialize beta_at_unique b
  3. L64
    specialize beta_at_unique c
  4. L65
    specialize beta_at_unique k
  5. L66
    specialize beta_at_unique p
  6. L67
    specialize beta_at_unique x
  7. L68
    apply beta_at_unique
  8. L69
    rewrite hs_left at hp
  9. L70
    rewrite hs_left at hp
  10. L71
    exact hp
14Use earlier factsL72–72

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

  1. L72
    exact he_witness_witness_left
15Calculate and transport equalitiesL73–73

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

  1. L73
    rewrite hpeq
16Use earlier factsL74–83

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

  1. L74
    exact he_witness_witness_right_right_right_left
  2. L75
    specialize lt_trans p
  3. L76
    specialize lt_trans x
  4. L77
    specialize lt_trans x1
  5. L78
    apply lt_trans
  6. L79
    specialize IH i
  7. L80
    specialize IH p
  8. L81
    specialize IH x
  9. L82
    apply IH
  10. L83
    exact hr
17Use earlier factsL84–87

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

  1. L84
    exact hs_right
  2. L85
    exact hp
  3. L86
    exact he_witness_witness_left
  4. L87
    exact he_witness_witness_right_right_right_left

Library-wide reading audit

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