PE000B

initial_prime_chain_bounded_exists

Construct the first k+1 primes with their actual terminal value strictly below the witnessed power 2^(k+2).

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. ∃ p. ∃ P. InitialPrimeChain(b,c,k) ∧ (BetaAt(b,c,k,p) ∧ (PowTwo(S S k,P) ∧ Lt(p,P)))

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

Definition DAG

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

Actual proof prerequisites

initial_prime_chain_singleton_existspow_two_two_exact · checked external prerequisiteleast_prime_above_existsinitial_prime_chain_prefix_extendbinary_power_two_exists · checked external prerequisitebinary_power_two_successor_double · checked external prerequisiteinitial_prime_chain_terminal_is_primeleast_prime_above_bertrand_boundadd_lt_add · checked external prerequisitelt_trans · checked external prerequisite
Original expanded first-order statement 
forall k. exists b c p P. ((((exists fs_h_pen_bounded_chain_initial. fs_h_pen_bounded_chain_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_bounded_chain_initial. b = fs_q_pen_bounded_chain_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_bounded_chain. (exists pc_lt_pen_bounded_chain_bound. pc_lt_pen_bounded_chain_bound + S (pen_index_bounded_chain) = (k)) -> exists pen_previous_bounded_chain pen_following_bounded_chain. (((exists fs_h_pen_bounded_chain_previous. fs_h_pen_bounded_chain_previous + S (pen_previous_bounded_chain) = S ((S (pen_index_bounded_chain)) * c)) /\ exists fs_q_pen_bounded_chain_previous. b = fs_q_pen_bounded_chain_previous * S ((S (pen_index_bounded_chain)) * c) + (pen_previous_bounded_chain))) /\ ((((exists fs_h_pen_bounded_chain_following. fs_h_pen_bounded_chain_following + S (pen_following_bounded_chain) = S ((S (S pen_index_bounded_chain)) * c)) /\ exists fs_q_pen_bounded_chain_following. b = fs_q_pen_bounded_chain_following * S ((S (S pen_index_bounded_chain)) * c) + (pen_following_bounded_chain))) /\ (((~(pen_following_bounded_chain = 1) /\ forall bpr_left_pc_pen_bounded_chain_next_prime bpr_right_pc_pen_bounded_chain_next_prime. pen_following_bounded_chain = bpr_left_pc_pen_bounded_chain_next_prime * bpr_right_pc_pen_bounded_chain_next_prime -> bpr_left_pc_pen_bounded_chain_next_prime = 1 \/ bpr_right_pc_pen_bounded_chain_next_prime = 1)) /\ ((exists pc_lt_pen_bounded_chain_next_greater. pc_lt_pen_bounded_chain_next_greater + S (pen_previous_bounded_chain) = (pen_following_bounded_chain)) /\ forall pen_comparison_bounded_chain_next. ((~(pen_comparison_bounded_chain_next = 1) /\ forall bpr_left_pc_pen_bounded_chain_next_comparison bpr_right_pc_pen_bounded_chain_next_comparison. pen_comparison_bounded_chain_next = bpr_left_pc_pen_bounded_chain_next_comparison * bpr_right_pc_pen_bounded_chain_next_comparison -> bpr_left_pc_pen_bounded_chain_next_comparison = 1 \/ bpr_right_pc_pen_bounded_chain_next_comparison = 1)) -> (exists pc_lt_pen_bounded_chain_next_above. pc_lt_pen_bounded_chain_next_above + S (pen_previous_bounded_chain) = (pen_comparison_bounded_chain_next)) -> (exists pc_le_pen_bounded_chain_next_minimal. pc_le_pen_bounded_chain_next_minimal + (pen_following_bounded_chain) = (pen_comparison_bounded_chain_next)))))) /\ ((((exists fs_h_pen_bounded_terminal. fs_h_pen_bounded_terminal + S (p) = S ((S (k)) * c)) /\ exists fs_q_pen_bounded_terminal. b = fs_q_pen_bounded_terminal * S ((S (k)) * c) + (p))) /\ ((exists pa_b_bl_pen_bounded_power pa_c_bl_pen_bounded_power. ((forall pa_i_bl_pen_bounded_power_repeat. (exists pa_lt_bl_pen_bounded_power_repeat_bound. pa_lt_bl_pen_bounded_power_repeat_bound + S pa_i_bl_pen_bounded_power_repeat = S (S k)) -> (((exists pa_h_bl_pen_bounded_power_repeat_decoded. pa_h_bl_pen_bounded_power_repeat_decoded + S (2) = S ((S (pa_i_bl_pen_bounded_power_repeat)) * pa_c_bl_pen_bounded_power)) /\ exists pa_q_bl_pen_bounded_power_repeat_decoded. pa_b_bl_pen_bounded_power = pa_q_bl_pen_bounded_power_repeat_decoded * S ((S (pa_i_bl_pen_bounded_power_repeat)) * pa_c_bl_pen_bounded_power) + (2)))) /\ (exists pa_u_bl_pen_bounded_power_product pa_v_bl_pen_bounded_power_product. ((((exists pa_h_bl_pen_bounded_power_product_start. pa_h_bl_pen_bounded_power_product_start + S (1) = S ((S (0)) * pa_v_bl_pen_bounded_power_product)) /\ exists pa_q_bl_pen_bounded_power_product_start. pa_u_bl_pen_bounded_power_product = pa_q_bl_pen_bounded_power_product_start * S ((S (0)) * pa_v_bl_pen_bounded_power_product) + (1))) /\ ((((exists pa_h_bl_pen_bounded_power_product_terminal. pa_h_bl_pen_bounded_power_product_terminal + S (P) = S ((S (S (S k))) * pa_v_bl_pen_bounded_power_product)) /\ exists pa_q_bl_pen_bounded_power_product_terminal. pa_u_bl_pen_bounded_power_product = pa_q_bl_pen_bounded_power_product_terminal * S ((S (S (S k))) * pa_v_bl_pen_bounded_power_product) + (P))) /\ forall pa_i_bl_pen_bounded_power_product. (exists pa_lt_bl_pen_bounded_power_product_bound. pa_lt_bl_pen_bounded_power_product_bound + S pa_i_bl_pen_bounded_power_product = S (S k)) -> exists pa_p_bl_pen_bounded_power_product pa_r_bl_pen_bounded_power_product pa_s_bl_pen_bounded_power_product. ((((exists pa_h_bl_pen_bounded_power_product_factor. pa_h_bl_pen_bounded_power_product_factor + S (pa_p_bl_pen_bounded_power_product) = S ((S (pa_i_bl_pen_bounded_power_product)) * pa_c_bl_pen_bounded_power)) /\ exists pa_q_bl_pen_bounded_power_product_factor. pa_b_bl_pen_bounded_power = pa_q_bl_pen_bounded_power_product_factor * S ((S (pa_i_bl_pen_bounded_power_product)) * pa_c_bl_pen_bounded_power) + (pa_p_bl_pen_bounded_power_product))) /\ ((((exists pa_h_bl_pen_bounded_power_product_partial. pa_h_bl_pen_bounded_power_product_partial + S (pa_r_bl_pen_bounded_power_product) = S ((S (pa_i_bl_pen_bounded_power_product)) * pa_v_bl_pen_bounded_power_product)) /\ exists pa_q_bl_pen_bounded_power_product_partial. pa_u_bl_pen_bounded_power_product = pa_q_bl_pen_bounded_power_product_partial * S ((S (pa_i_bl_pen_bounded_power_product)) * pa_v_bl_pen_bounded_power_product) + (pa_r_bl_pen_bounded_power_product))) /\ ((((exists pa_h_bl_pen_bounded_power_product_successor. pa_h_bl_pen_bounded_power_product_successor + S (pa_s_bl_pen_bounded_power_product) = S ((S (S pa_i_bl_pen_bounded_power_product)) * pa_v_bl_pen_bounded_power_product)) /\ exists pa_q_bl_pen_bounded_power_product_successor. pa_u_bl_pen_bounded_power_product = pa_q_bl_pen_bounded_power_product_successor * S ((S (S pa_i_bl_pen_bounded_power_product)) * pa_v_bl_pen_bounded_power_product) + (pa_s_bl_pen_bounded_power_product))) /\ pa_s_bl_pen_bounded_power_product = pa_r_bl_pen_bounded_power_product * pa_p_bl_pen_bounded_power_product)))))))) /\ (exists pc_lt_pen_bounded_bound. pc_lt_pen_bounded_bound + S (p) = (P))))

Complete tactic proof in conservative notation

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

84 script commands · 28 reading checkpoints · 4 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 (4)
least prime above existsinitial prime chain prefix extendleast prime above bertrand boundinitial prime chain terminal is prime
01Induction on kL1–1

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

  1. L1
    induction k
02Separate the logical casesL2–3

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

  1. L2
    cases initial_prime_chain_singleton_exists
  2. L3
    cases initial_prime_chain_singleton_exists_witness
03Construct an explicit witnessL4–7

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

  1. L4
    exists x
  2. L5
    exists x1
  3. L6
    exists 2
  4. L7
    exists 4
04Separate the logical casesL8–8

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

  1. L8
    split
05Use earlier factsL9–9

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

  1. L9
    exact initial_prime_chain_singleton_exists_witness_witness
06Separate the logical casesL10–11

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

  1. L10
    split
  2. L11
    cases initial_prime_chain_singleton_exists_witness_witness
07Use earlier factsL12–12

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

  1. L12
    exact initial_prime_chain_singleton_exists_witness_witness_left
08Separate the logical casesL13–13

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

  1. L13
    split
09Use earlier factsL14–14

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

  1. L14
    exact pow_two_two_exact
10Construct an explicit witnessL15–15

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

  1. L15
    exists 1
11Calculate and transport equalitiesL16–16

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

  1. L16
    norm_num
12Separate the logical casesL17–23

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

  1. L17
    cases IH
  2. L18
    cases IH_witness
  3. L19
    cases IH_witness_witness
  4. L20
    cases IH_witness_witness_witness
  5. L21
    cases IH_witness_witness_witness_witness
  6. L22
    cases IH_witness_witness_witness_witness_right
  7. L23
    cases IH_witness_witness_witness_witness_right_right
13Establish hnL24–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply least prime above exists.

  1. L24
    have hn : ∃ q. NextPrime(x2,q)Definitions: NextPrime(x2,q)Original native command in the exact edition
  2. L25
    specialize least_prime_above_exists x2
  3. L26
    apply least_prime_above_exists
14Separate the logical casesL27–27

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

  1. L27
    cases hn
15Establish hPL28–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two exists.

  1. L28
    have hP : ∃ Q. PowTwo(S S S k,Q)Definitions: PowTwo(S S S k,Q)Original native command in the exact edition
  2. L29
    specialize binary_power_two_exists (S (S (S k)))
  3. L30
    apply binary_power_two_exists
16Separate the logical casesL31–31

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

  1. L31
    cases hP
17Establish heL32–41

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

  1. L32
    have he : ∃ z. ∃ d. InitialPrimeChain(z,d,S k) ∧ BetaAt(z,d,S k,x4)Definitions: InitialPrimeChain(z,d,S k)BetaAt(z,d,S k,x4)Original native command in the exact edition
  2. L33
    specialize initial_prime_chain_prefix_extend k
  3. L34
    specialize initial_prime_chain_prefix_extend x
  4. L35
    specialize initial_prime_chain_prefix_extend x1
  5. L36
    specialize initial_prime_chain_prefix_extend x2
  6. L37
    specialize initial_prime_chain_prefix_extend x4
  7. L38
    apply initial_prime_chain_prefix_extend
  8. L39
    exact IH_witness_witness_witness_witness_left
  9. L40
    exact IH_witness_witness_witness_witness_right_left
  10. L41
    exact hn_witness
18Separate the logical casesL42–44

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

  1. L42
    cases he
  2. L43
    cases he_witness
  3. L44
    cases he_witness_witness
19Construct an explicit witnessL45–48

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

  1. L45
    exists x6
  2. L46
    exists x7
  3. L47
    exists x4
  4. L48
    exists x5
20Separate the logical casesL49–49

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

  1. L49
    split
21Use earlier factsL50–50

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

  1. L50
    exact he_witness_witness_left
22Separate the logical casesL51–51

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

  1. L51
    split
23Use earlier factsL52–52

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

  1. L52
    exact he_witness_witness_right
24Separate the logical casesL53–53

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

  1. L53
    split
25Use earlier factsL54–54

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

  1. L54
    exact hP_witness
26Establish hdL55–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two successor double.

  1. L55
    have hd : x5 = x3 + x3
  2. L56
    specialize binary_power_two_successor_double (S (S k))
  3. L57
    specialize binary_power_two_successor_double x3
  4. L58
    specialize binary_power_two_successor_double x5
  5. L59
    apply binary_power_two_successor_double
  6. L60
    exact IH_witness_witness_witness_witness_right_right_left
  7. L61
    exact hP_witness
  8. L62
    rewrite hd
  9. L63
    specialize lt_trans x4
  10. L64
    specialize lt_trans (x2 + x2)
27Use earlier factsL65–74

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

  1. L65
    specialize lt_trans (x3 + x3)
  2. L66
    apply lt_trans
  3. L67
    specialize least_prime_above_bertrand_bound x2
  4. L68
    specialize least_prime_above_bertrand_bound x4
  5. L69
    apply least_prime_above_bertrand_bound
  6. L70
    specialize initial_prime_chain_terminal_is_prime x
  7. L71
    specialize initial_prime_chain_terminal_is_prime x1
  8. L72
    specialize initial_prime_chain_terminal_is_prime k
  9. L73
    specialize initial_prime_chain_terminal_is_prime x2
  10. L74
    apply initial_prime_chain_terminal_is_prime
28Use earlier factsL75–84

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

  1. L75
    exact IH_witness_witness_witness_witness_left
  2. L76
    exact IH_witness_witness_witness_witness_right_left
  3. L77
    exact hn_witness
  4. L78
    specialize add_lt_add x2
  5. L79
    specialize add_lt_add x3
  6. L80
    specialize add_lt_add x2
  7. L81
    specialize add_lt_add x3
  8. L82
    apply add_lt_add
  9. L83
    exact IH_witness_witness_witness_witness_right_right_right
  10. L84
    exact IH_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 84 lines
  1. 0001induction k
  2. 0002cases initial_prime_chain_singleton_exists
  3. 0003cases initial_prime_chain_singleton_exists_witness
  4. 0004exists x
  5. 0005exists x1
  6. 0006exists 2
  7. 0007exists 4
  8. 0008split
  9. 0009exact initial_prime_chain_singleton_exists_witness_witness
  10. 0010split
  11. 0011cases initial_prime_chain_singleton_exists_witness_witness
  12. 0012exact initial_prime_chain_singleton_exists_witness_witness_left
  13. 0013split
  14. 0014exact pow_two_two_exact
  15. 0015exists 1
  16. 0016norm_num
  17. 0017cases IH
  18. 0018cases IH_witness
  19. 0019cases IH_witness_witness
  20. 0020cases IH_witness_witness_witness
  21. 0021cases IH_witness_witness_witness_witness
  22. 0022cases IH_witness_witness_witness_witness_right
  23. 0023cases IH_witness_witness_witness_witness_right_right
  24. 0024have hn : ∃ q. NextPrime(x2,q)
  25. 0025specialize least_prime_above_exists x2
  26. 0026apply least_prime_above_exists
  27. 0027cases hn
  28. 0028have hP : ∃ Q. PowTwo(S S S k,Q)
  29. 0029specialize binary_power_two_exists (S (S (S k)))
  30. 0030apply binary_power_two_exists
  31. 0031cases hP
  32. 0032have he : ∃ z. ∃ d. InitialPrimeChain(z,d,S k) ∧ BetaAt(z,d,S k,x4)
  33. 0033specialize initial_prime_chain_prefix_extend k
  34. 0034specialize initial_prime_chain_prefix_extend x
  35. 0035specialize initial_prime_chain_prefix_extend x1
  36. 0036specialize initial_prime_chain_prefix_extend x2
  37. 0037specialize initial_prime_chain_prefix_extend x4
  38. 0038apply initial_prime_chain_prefix_extend
  39. 0039exact IH_witness_witness_witness_witness_left
  40. 0040exact IH_witness_witness_witness_witness_right_left
  41. 0041exact hn_witness
  42. 0042cases he
  43. 0043cases he_witness
  44. 0044cases he_witness_witness
  45. 0045exists x6
  46. 0046exists x7
  47. 0047exists x4
  48. 0048exists x5
  49. 0049split
  50. 0050exact he_witness_witness_left
  51. 0051split
  52. 0052exact he_witness_witness_right
  53. 0053split
  54. 0054exact hP_witness
  55. 0055have hd : x5 = x3 + x3
  56. 0056specialize binary_power_two_successor_double (S (S k))
  57. 0057specialize binary_power_two_successor_double x3
  58. 0058specialize binary_power_two_successor_double x5
  59. 0059apply binary_power_two_successor_double
  60. 0060exact IH_witness_witness_witness_witness_right_right_left
  61. 0061exact hP_witness
  62. 0062rewrite hd
  63. 0063specialize lt_trans x4
  64. 0064specialize lt_trans (x2 + x2)
  65. 0065specialize lt_trans (x3 + x3)
  66. 0066apply lt_trans
  67. 0067specialize least_prime_above_bertrand_bound x2
  68. 0068specialize least_prime_above_bertrand_bound x4
  69. 0069apply least_prime_above_bertrand_bound
  70. 0070specialize initial_prime_chain_terminal_is_prime x
  71. 0071specialize initial_prime_chain_terminal_is_prime x1
  72. 0072specialize initial_prime_chain_terminal_is_prime k
  73. 0073specialize initial_prime_chain_terminal_is_prime x2
  74. 0074apply initial_prime_chain_terminal_is_prime
  75. 0075exact IH_witness_witness_witness_witness_left
  76. 0076exact IH_witness_witness_witness_witness_right_left
  77. 0077exact hn_witness
  78. 0078specialize add_lt_add x2
  79. 0079specialize add_lt_add x3
  80. 0080specialize add_lt_add x2
  81. 0081specialize add_lt_add x3
  82. 0082apply add_lt_add
  83. 0083exact IH_witness_witness_witness_witness_right_right_right
  84. 0084exact IH_witness_witness_witness_witness_right_right_right