PE000B

initial_prime_chain_bounded_exists

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 10 declared prerequisites and contains 84 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PE0007 initial_prime_chain_singleton_exists pow_two_two_exact Alpha theorem; checked-use authorized PE0003 least_prime_above_exists PE0008 initial_prime_chain_prefix_extend binary_power_two_exists Alpha theorem; checked-use authorized binary_power_two_successor_double Alpha theorem; checked-use authorized PE000A initial_prime_chain_terminal_is_prime PE0005 least_prime_above_bertrand_bound add_lt_add Alpha theorem; checked-use authorized lt_trans Stable theorem; checked-use authorized

Direct dependents

PE000C first_primes_double_exponential_bound

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

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.

Named ingredients (4)
least prime above existsinitial prime chain prefix extendinitial prime chain terminal is primeleast prime above bertrand bound

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.

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
  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
  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: InitialPrimeChainBetaAt
  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 exact 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 : exists q. ((~(q = 1) /\ forall bpr_left_pc_pen_bounded_next_prime bpr_right_pc_pen_bounded_next_prime. q = bpr_left_pc_pen_bounded_next_prime * bpr_right_pc_pen_bounded_next_prime -> bpr_left_pc_pen_bounded_next_prime = 1 \/ bpr_right_pc_pen_bounded_next_prime = 1)) /\ ((exists pc_lt_pen_bounded_next_greater. pc_lt_pen_bounded_next_greater + S (x2) = (q)) /\ forall pen_comparison_bounded_next. ((~(pen_comparison_bounded_next = 1) /\ forall bpr_left_pc_pen_bounded_next_comparison bpr_right_pc_pen_bounded_next_comparison. pen_comparison_bounded_next = bpr_left_pc_pen_bounded_next_comparison * bpr_right_pc_pen_bounded_next_comparison -> bpr_left_pc_pen_bounded_next_comparison = 1 \/ bpr_right_pc_pen_bounded_next_comparison = 1)) -> (exists pc_lt_pen_bounded_next_above. pc_lt_pen_bounded_next_above + S (x2) = (pen_comparison_bounded_next)) -> (exists pc_le_pen_bounded_next_minimal. pc_le_pen_bounded_next_minimal + (q) = (pen_comparison_bounded_next)))
  25. 0025specialize least_prime_above_exists x2
  26. 0026apply least_prime_above_exists
  27. 0027cases hn
  28. 0028have hP : exists Q. exists pa_b_bl_pen_bounded_next_power pa_c_bl_pen_bounded_next_power. ((forall pa_i_bl_pen_bounded_next_power_repeat. (exists pa_lt_bl_pen_bounded_next_power_repeat_bound. pa_lt_bl_pen_bounded_next_power_repeat_bound + S pa_i_bl_pen_bounded_next_power_repeat = S (S (S k))) -> (((exists pa_h_bl_pen_bounded_next_power_repeat_decoded. pa_h_bl_pen_bounded_next_power_repeat_decoded + S (2) = S ((S (pa_i_bl_pen_bounded_next_power_repeat)) * pa_c_bl_pen_bounded_next_power)) /\ exists pa_q_bl_pen_bounded_next_power_repeat_decoded. pa_b_bl_pen_bounded_next_power = pa_q_bl_pen_bounded_next_power_repeat_decoded * S ((S (pa_i_bl_pen_bounded_next_power_repeat)) * pa_c_bl_pen_bounded_next_power) + (2)))) /\ (exists pa_u_bl_pen_bounded_next_power_product pa_v_bl_pen_bounded_next_power_product. ((((exists pa_h_bl_pen_bounded_next_power_product_start. pa_h_bl_pen_bounded_next_power_product_start + S (1) = S ((S (0)) * pa_v_bl_pen_bounded_next_power_product)) /\ exists pa_q_bl_pen_bounded_next_power_product_start. pa_u_bl_pen_bounded_next_power_product = pa_q_bl_pen_bounded_next_power_product_start * S ((S (0)) * pa_v_bl_pen_bounded_next_power_product) + (1))) /\ ((((exists pa_h_bl_pen_bounded_next_power_product_terminal. pa_h_bl_pen_bounded_next_power_product_terminal + S (Q) = S ((S (S (S (S k)))) * pa_v_bl_pen_bounded_next_power_product)) /\ exists pa_q_bl_pen_bounded_next_power_product_terminal. pa_u_bl_pen_bounded_next_power_product = pa_q_bl_pen_bounded_next_power_product_terminal * S ((S (S (S (S k)))) * pa_v_bl_pen_bounded_next_power_product) + (Q))) /\ forall pa_i_bl_pen_bounded_next_power_product. (exists pa_lt_bl_pen_bounded_next_power_product_bound. pa_lt_bl_pen_bounded_next_power_product_bound + S pa_i_bl_pen_bounded_next_power_product = S (S (S k))) -> exists pa_p_bl_pen_bounded_next_power_product pa_r_bl_pen_bounded_next_power_product pa_s_bl_pen_bounded_next_power_product. ((((exists pa_h_bl_pen_bounded_next_power_product_factor. pa_h_bl_pen_bounded_next_power_product_factor + S (pa_p_bl_pen_bounded_next_power_product) = S ((S (pa_i_bl_pen_bounded_next_power_product)) * pa_c_bl_pen_bounded_next_power)) /\ exists pa_q_bl_pen_bounded_next_power_product_factor. pa_b_bl_pen_bounded_next_power = pa_q_bl_pen_bounded_next_power_product_factor * S ((S (pa_i_bl_pen_bounded_next_power_product)) * pa_c_bl_pen_bounded_next_power) + (pa_p_bl_pen_bounded_next_power_product))) /\ ((((exists pa_h_bl_pen_bounded_next_power_product_partial. pa_h_bl_pen_bounded_next_power_product_partial + S (pa_r_bl_pen_bounded_next_power_product) = S ((S (pa_i_bl_pen_bounded_next_power_product)) * pa_v_bl_pen_bounded_next_power_product)) /\ exists pa_q_bl_pen_bounded_next_power_product_partial. pa_u_bl_pen_bounded_next_power_product = pa_q_bl_pen_bounded_next_power_product_partial * S ((S (pa_i_bl_pen_bounded_next_power_product)) * pa_v_bl_pen_bounded_next_power_product) + (pa_r_bl_pen_bounded_next_power_product))) /\ ((((exists pa_h_bl_pen_bounded_next_power_product_successor. pa_h_bl_pen_bounded_next_power_product_successor + S (pa_s_bl_pen_bounded_next_power_product) = S ((S (S pa_i_bl_pen_bounded_next_power_product)) * pa_v_bl_pen_bounded_next_power_product)) /\ exists pa_q_bl_pen_bounded_next_power_product_successor. pa_u_bl_pen_bounded_next_power_product = pa_q_bl_pen_bounded_next_power_product_successor * S ((S (S pa_i_bl_pen_bounded_next_power_product)) * pa_v_bl_pen_bounded_next_power_product) + (pa_s_bl_pen_bounded_next_power_product))) /\ pa_s_bl_pen_bounded_next_power_product = pa_r_bl_pen_bounded_next_power_product * pa_p_bl_pen_bounded_next_power_product)))))))
  29. 0029specialize binary_power_two_exists (S (S (S k)))
  30. 0030apply binary_power_two_exists
  31. 0031cases hP
  32. 0032have he : exists z d. ((((exists fs_h_pen_bounded_new_chain_initial. fs_h_pen_bounded_new_chain_initial + S (2) = S ((S (0)) * d)) /\ exists fs_q_pen_bounded_new_chain_initial. z = fs_q_pen_bounded_new_chain_initial * S ((S (0)) * d) + (2))) /\ forall pen_index_bounded_new_chain. (exists pc_lt_pen_bounded_new_chain_bound. pc_lt_pen_bounded_new_chain_bound + S (pen_index_bounded_new_chain) = (S k)) -> exists pen_previous_bounded_new_chain pen_following_bounded_new_chain. (((exists fs_h_pen_bounded_new_chain_previous. fs_h_pen_bounded_new_chain_previous + S (pen_previous_bounded_new_chain) = S ((S (pen_index_bounded_new_chain)) * d)) /\ exists fs_q_pen_bounded_new_chain_previous. z = fs_q_pen_bounded_new_chain_previous * S ((S (pen_index_bounded_new_chain)) * d) + (pen_previous_bounded_new_chain))) /\ ((((exists fs_h_pen_bounded_new_chain_following. fs_h_pen_bounded_new_chain_following + S (pen_following_bounded_new_chain) = S ((S (S pen_index_bounded_new_chain)) * d)) /\ exists fs_q_pen_bounded_new_chain_following. z = fs_q_pen_bounded_new_chain_following * S ((S (S pen_index_bounded_new_chain)) * d) + (pen_following_bounded_new_chain))) /\ (((~(pen_following_bounded_new_chain = 1) /\ forall bpr_left_pc_pen_bounded_new_chain_next_prime bpr_right_pc_pen_bounded_new_chain_next_prime. pen_following_bounded_new_chain = bpr_left_pc_pen_bounded_new_chain_next_prime * bpr_right_pc_pen_bounded_new_chain_next_prime -> bpr_left_pc_pen_bounded_new_chain_next_prime = 1 \/ bpr_right_pc_pen_bounded_new_chain_next_prime = 1)) /\ ((exists pc_lt_pen_bounded_new_chain_next_greater. pc_lt_pen_bounded_new_chain_next_greater + S (pen_previous_bounded_new_chain) = (pen_following_bounded_new_chain)) /\ forall pen_comparison_bounded_new_chain_next. ((~(pen_comparison_bounded_new_chain_next = 1) /\ forall bpr_left_pc_pen_bounded_new_chain_next_comparison bpr_right_pc_pen_bounded_new_chain_next_comparison. pen_comparison_bounded_new_chain_next = bpr_left_pc_pen_bounded_new_chain_next_comparison * bpr_right_pc_pen_bounded_new_chain_next_comparison -> bpr_left_pc_pen_bounded_new_chain_next_comparison = 1 \/ bpr_right_pc_pen_bounded_new_chain_next_comparison = 1)) -> (exists pc_lt_pen_bounded_new_chain_next_above. pc_lt_pen_bounded_new_chain_next_above + S (pen_previous_bounded_new_chain) = (pen_comparison_bounded_new_chain_next)) -> (exists pc_le_pen_bounded_new_chain_next_minimal. pc_le_pen_bounded_new_chain_next_minimal + (pen_following_bounded_new_chain) = (pen_comparison_bounded_new_chain_next)))))) /\ (((exists fs_h_pen_bounded_new_last. fs_h_pen_bounded_new_last + S (x4) = S ((S (S k)) * d)) /\ exists fs_q_pen_bounded_new_last. z = fs_q_pen_bounded_new_last * S ((S (S k)) * d) + (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