PE0013

first_primes_list_exists

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

Every finite number of initial primes has a real beta-coded list, including the empty list at zero.

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. (k = 0 \/ exists pen_last_index_total_list. k = S pen_last_index_total_list /\ ((((exists fs_h_pen_total_list_chain_initial. fs_h_pen_total_list_chain_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_total_list_chain_initial. b = fs_q_pen_total_list_chain_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_total_list_chain. (exists pc_lt_pen_total_list_chain_bound. pc_lt_pen_total_list_chain_bound + S (pen_index_total_list_chain) = (pen_last_index_total_list)) -> exists pen_previous_total_list_chain pen_following_total_list_chain. (((exists fs_h_pen_total_list_chain_previous. fs_h_pen_total_list_chain_previous + S (pen_previous_total_list_chain) = S ((S (pen_index_total_list_chain)) * c)) /\ exists fs_q_pen_total_list_chain_previous. b = fs_q_pen_total_list_chain_previous * S ((S (pen_index_total_list_chain)) * c) + (pen_previous_total_list_chain))) /\ ((((exists fs_h_pen_total_list_chain_following. fs_h_pen_total_list_chain_following + S (pen_following_total_list_chain) = S ((S (S pen_index_total_list_chain)) * c)) /\ exists fs_q_pen_total_list_chain_following. b = fs_q_pen_total_list_chain_following * S ((S (S pen_index_total_list_chain)) * c) + (pen_following_total_list_chain))) /\ (((~(pen_following_total_list_chain = 1) /\ forall bpr_left_pc_pen_total_list_chain_next_prime bpr_right_pc_pen_total_list_chain_next_prime. pen_following_total_list_chain = bpr_left_pc_pen_total_list_chain_next_prime * bpr_right_pc_pen_total_list_chain_next_prime -> bpr_left_pc_pen_total_list_chain_next_prime = 1 \/ bpr_right_pc_pen_total_list_chain_next_prime = 1)) /\ ((exists pc_lt_pen_total_list_chain_next_greater. pc_lt_pen_total_list_chain_next_greater + S (pen_previous_total_list_chain) = (pen_following_total_list_chain)) /\ forall pen_comparison_total_list_chain_next. ((~(pen_comparison_total_list_chain_next = 1) /\ forall bpr_left_pc_pen_total_list_chain_next_comparison bpr_right_pc_pen_total_list_chain_next_comparison. pen_comparison_total_list_chain_next = bpr_left_pc_pen_total_list_chain_next_comparison * bpr_right_pc_pen_total_list_chain_next_comparison -> bpr_left_pc_pen_total_list_chain_next_comparison = 1 \/ bpr_right_pc_pen_total_list_chain_next_comparison = 1)) -> (exists pc_lt_pen_total_list_chain_next_above. pc_lt_pen_total_list_chain_next_above + S (pen_previous_total_list_chain) = (pen_comparison_total_list_chain_next)) -> (exists pc_le_pen_total_list_chain_next_minimal. pc_le_pen_total_list_chain_next_minimal + (pen_following_total_list_chain) = (pen_comparison_total_list_chain_next)))))))

Constructive proof overview

Generated structural guide

Every finite number of initial primes has a real beta-coded list, including the empty list at zero.

The unchanged tactic script uses 2 declared prerequisites and contains 25 exact native proof lines.

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

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized PE000C first_primes_double_exponential_bound

Direct dependents

none

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

25 script commands · 10 reading checkpoints · 2 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 (1)
first primes double exponential 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.

01Fix variables and assumptionsL1–1

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

  1. L1
    intro k
02Establish hzL2–5

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

  1. L2
    have hz : k = 0 \/ ~(k = 0)
  2. L3
    specialize eq_decidable k
  3. L4
    specialize eq_decidable 0
  4. L5
    apply eq_decidable
03Separate the logical casesL6–6

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

  1. L6
    cases hz
04Construct an explicit witnessL7–8

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

  1. L7
    exists 0
  2. L8
    exists 0
05Separate the logical casesL9–9

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

  1. L9
    left
06Use earlier factsL10–11

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

  1. L10
    exact hz_left
  2. L11
    specialize first_primes_double_exponential_bound k
07Establish hpositiveL12–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply first primes double exponential bound.

  1. L12
    have hpositive : ∃ b. ∃ c. ∃ j. ∃ p. ∃ e. ∃ B. k = S j ∧ (InitialPrimeList(b,c,k) ∧ (BetaAt(b,c,j,p) ∧ (PowTwo(k,e) ∧ (PowTwo(e,B) ∧ Lt(p,B)))))Definitions: PowTwoInitialPrimeListLtBetaAt
  2. L13
    apply first_primes_double_exponential_bound
  3. L14
    exact hz_right
08Separate the logical casesL15–22

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

  1. L15
    cases hpositive
  2. L16
    cases hpositive_witness
  3. L17
    cases hpositive_witness_witness
  4. L18
    cases hpositive_witness_witness_witness
  5. L19
    cases hpositive_witness_witness_witness_witness
  6. L20
    cases hpositive_witness_witness_witness_witness_witness
  7. L21
    cases hpositive_witness_witness_witness_witness_witness_witness
  8. L22
    cases hpositive_witness_witness_witness_witness_witness_witness_right
09Construct an explicit witnessL23–24

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

  1. L23
    exists x
  2. L24
    exists x1
10Use earlier factsL25–25

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

  1. L25
    exact hpositive_witness_witness_witness_witness_witness_witness_right_left

Library-wide reading audit

Original exact command ledger · 25 lines
  1. 0001intro k
  2. 0002have hz : k = 0 \/ ~(k = 0)
  3. 0003specialize eq_decidable k
  4. 0004specialize eq_decidable 0
  5. 0005apply eq_decidable
  6. 0006cases hz
  7. 0007exists 0
  8. 0008exists 0
  9. 0009left
  10. 0010exact hz_left
  11. 0011specialize first_primes_double_exponential_bound k
  12. 0012have hpositive : exists b c j p e B. k = S j /\ (((k = 0 \/ exists pen_last_index_total_positive_list. k = S pen_last_index_total_positive_list /\ ((((exists fs_h_pen_total_positive_list_chain_initial. fs_h_pen_total_positive_list_chain_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_total_positive_list_chain_initial. b = fs_q_pen_total_positive_list_chain_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_total_positive_list_chain. (exists pc_lt_pen_total_positive_list_chain_bound. pc_lt_pen_total_positive_list_chain_bound + S (pen_index_total_positive_list_chain) = (pen_last_index_total_positive_list)) -> exists pen_previous_total_positive_list_chain pen_following_total_positive_list_chain. (((exists fs_h_pen_total_positive_list_chain_previous. fs_h_pen_total_positive_list_chain_previous + S (pen_previous_total_positive_list_chain) = S ((S (pen_index_total_positive_list_chain)) * c)) /\ exists fs_q_pen_total_positive_list_chain_previous. b = fs_q_pen_total_positive_list_chain_previous * S ((S (pen_index_total_positive_list_chain)) * c) + (pen_previous_total_positive_list_chain))) /\ ((((exists fs_h_pen_total_positive_list_chain_following. fs_h_pen_total_positive_list_chain_following + S (pen_following_total_positive_list_chain) = S ((S (S pen_index_total_positive_list_chain)) * c)) /\ exists fs_q_pen_total_positive_list_chain_following. b = fs_q_pen_total_positive_list_chain_following * S ((S (S pen_index_total_positive_list_chain)) * c) + (pen_following_total_positive_list_chain))) /\ (((~(pen_following_total_positive_list_chain = 1) /\ forall bpr_left_pc_pen_total_positive_list_chain_next_prime bpr_right_pc_pen_total_positive_list_chain_next_prime. pen_following_total_positive_list_chain = bpr_left_pc_pen_total_positive_list_chain_next_prime * bpr_right_pc_pen_total_positive_list_chain_next_prime -> bpr_left_pc_pen_total_positive_list_chain_next_prime = 1 \/ bpr_right_pc_pen_total_positive_list_chain_next_prime = 1)) /\ ((exists pc_lt_pen_total_positive_list_chain_next_greater. pc_lt_pen_total_positive_list_chain_next_greater + S (pen_previous_total_positive_list_chain) = (pen_following_total_positive_list_chain)) /\ forall pen_comparison_total_positive_list_chain_next. ((~(pen_comparison_total_positive_list_chain_next = 1) /\ forall bpr_left_pc_pen_total_positive_list_chain_next_comparison bpr_right_pc_pen_total_positive_list_chain_next_comparison. pen_comparison_total_positive_list_chain_next = bpr_left_pc_pen_total_positive_list_chain_next_comparison * bpr_right_pc_pen_total_positive_list_chain_next_comparison -> bpr_left_pc_pen_total_positive_list_chain_next_comparison = 1 \/ bpr_right_pc_pen_total_positive_list_chain_next_comparison = 1)) -> (exists pc_lt_pen_total_positive_list_chain_next_above. pc_lt_pen_total_positive_list_chain_next_above + S (pen_previous_total_positive_list_chain) = (pen_comparison_total_positive_list_chain_next)) -> (exists pc_le_pen_total_positive_list_chain_next_minimal. pc_le_pen_total_positive_list_chain_next_minimal + (pen_following_total_positive_list_chain) = (pen_comparison_total_positive_list_chain_next)))))))) /\ ((((exists fs_h_pen_total_positive_last. fs_h_pen_total_positive_last + S (p) = S ((S (j)) * c)) /\ exists fs_q_pen_total_positive_last. b = fs_q_pen_total_positive_last * S ((S (j)) * c) + (p))) /\ ((exists pa_b_bl_pen_total_positive_exponent pa_c_bl_pen_total_positive_exponent. ((forall pa_i_bl_pen_total_positive_exponent_repeat. (exists pa_lt_bl_pen_total_positive_exponent_repeat_bound. pa_lt_bl_pen_total_positive_exponent_repeat_bound + S pa_i_bl_pen_total_positive_exponent_repeat = k) -> (((exists pa_h_bl_pen_total_positive_exponent_repeat_decoded. pa_h_bl_pen_total_positive_exponent_repeat_decoded + S (2) = S ((S (pa_i_bl_pen_total_positive_exponent_repeat)) * pa_c_bl_pen_total_positive_exponent)) /\ exists pa_q_bl_pen_total_positive_exponent_repeat_decoded. pa_b_bl_pen_total_positive_exponent = pa_q_bl_pen_total_positive_exponent_repeat_decoded * S ((S (pa_i_bl_pen_total_positive_exponent_repeat)) * pa_c_bl_pen_total_positive_exponent) + (2)))) /\ (exists pa_u_bl_pen_total_positive_exponent_product pa_v_bl_pen_total_positive_exponent_product. ((((exists pa_h_bl_pen_total_positive_exponent_product_start. pa_h_bl_pen_total_positive_exponent_product_start + S (1) = S ((S (0)) * pa_v_bl_pen_total_positive_exponent_product)) /\ exists pa_q_bl_pen_total_positive_exponent_product_start. pa_u_bl_pen_total_positive_exponent_product = pa_q_bl_pen_total_positive_exponent_product_start * S ((S (0)) * pa_v_bl_pen_total_positive_exponent_product) + (1))) /\ ((((exists pa_h_bl_pen_total_positive_exponent_product_terminal. pa_h_bl_pen_total_positive_exponent_product_terminal + S (e) = S ((S (k)) * pa_v_bl_pen_total_positive_exponent_product)) /\ exists pa_q_bl_pen_total_positive_exponent_product_terminal. pa_u_bl_pen_total_positive_exponent_product = pa_q_bl_pen_total_positive_exponent_product_terminal * S ((S (k)) * pa_v_bl_pen_total_positive_exponent_product) + (e))) /\ forall pa_i_bl_pen_total_positive_exponent_product. (exists pa_lt_bl_pen_total_positive_exponent_product_bound. pa_lt_bl_pen_total_positive_exponent_product_bound + S pa_i_bl_pen_total_positive_exponent_product = k) -> exists pa_p_bl_pen_total_positive_exponent_product pa_r_bl_pen_total_positive_exponent_product pa_s_bl_pen_total_positive_exponent_product. ((((exists pa_h_bl_pen_total_positive_exponent_product_factor. pa_h_bl_pen_total_positive_exponent_product_factor + S (pa_p_bl_pen_total_positive_exponent_product) = S ((S (pa_i_bl_pen_total_positive_exponent_product)) * pa_c_bl_pen_total_positive_exponent)) /\ exists pa_q_bl_pen_total_positive_exponent_product_factor. pa_b_bl_pen_total_positive_exponent = pa_q_bl_pen_total_positive_exponent_product_factor * S ((S (pa_i_bl_pen_total_positive_exponent_product)) * pa_c_bl_pen_total_positive_exponent) + (pa_p_bl_pen_total_positive_exponent_product))) /\ ((((exists pa_h_bl_pen_total_positive_exponent_product_partial. pa_h_bl_pen_total_positive_exponent_product_partial + S (pa_r_bl_pen_total_positive_exponent_product) = S ((S (pa_i_bl_pen_total_positive_exponent_product)) * pa_v_bl_pen_total_positive_exponent_product)) /\ exists pa_q_bl_pen_total_positive_exponent_product_partial. pa_u_bl_pen_total_positive_exponent_product = pa_q_bl_pen_total_positive_exponent_product_partial * S ((S (pa_i_bl_pen_total_positive_exponent_product)) * pa_v_bl_pen_total_positive_exponent_product) + (pa_r_bl_pen_total_positive_exponent_product))) /\ ((((exists pa_h_bl_pen_total_positive_exponent_product_successor. pa_h_bl_pen_total_positive_exponent_product_successor + S (pa_s_bl_pen_total_positive_exponent_product) = S ((S (S pa_i_bl_pen_total_positive_exponent_product)) * pa_v_bl_pen_total_positive_exponent_product)) /\ exists pa_q_bl_pen_total_positive_exponent_product_successor. pa_u_bl_pen_total_positive_exponent_product = pa_q_bl_pen_total_positive_exponent_product_successor * S ((S (S pa_i_bl_pen_total_positive_exponent_product)) * pa_v_bl_pen_total_positive_exponent_product) + (pa_s_bl_pen_total_positive_exponent_product))) /\ pa_s_bl_pen_total_positive_exponent_product = pa_r_bl_pen_total_positive_exponent_product * pa_p_bl_pen_total_positive_exponent_product)))))))) /\ ((exists pa_b_bl_pen_total_positive_bound pa_c_bl_pen_total_positive_bound. ((forall pa_i_bl_pen_total_positive_bound_repeat. (exists pa_lt_bl_pen_total_positive_bound_repeat_bound. pa_lt_bl_pen_total_positive_bound_repeat_bound + S pa_i_bl_pen_total_positive_bound_repeat = e) -> (((exists pa_h_bl_pen_total_positive_bound_repeat_decoded. pa_h_bl_pen_total_positive_bound_repeat_decoded + S (2) = S ((S (pa_i_bl_pen_total_positive_bound_repeat)) * pa_c_bl_pen_total_positive_bound)) /\ exists pa_q_bl_pen_total_positive_bound_repeat_decoded. pa_b_bl_pen_total_positive_bound = pa_q_bl_pen_total_positive_bound_repeat_decoded * S ((S (pa_i_bl_pen_total_positive_bound_repeat)) * pa_c_bl_pen_total_positive_bound) + (2)))) /\ (exists pa_u_bl_pen_total_positive_bound_product pa_v_bl_pen_total_positive_bound_product. ((((exists pa_h_bl_pen_total_positive_bound_product_start. pa_h_bl_pen_total_positive_bound_product_start + S (1) = S ((S (0)) * pa_v_bl_pen_total_positive_bound_product)) /\ exists pa_q_bl_pen_total_positive_bound_product_start. pa_u_bl_pen_total_positive_bound_product = pa_q_bl_pen_total_positive_bound_product_start * S ((S (0)) * pa_v_bl_pen_total_positive_bound_product) + (1))) /\ ((((exists pa_h_bl_pen_total_positive_bound_product_terminal. pa_h_bl_pen_total_positive_bound_product_terminal + S (B) = S ((S (e)) * pa_v_bl_pen_total_positive_bound_product)) /\ exists pa_q_bl_pen_total_positive_bound_product_terminal. pa_u_bl_pen_total_positive_bound_product = pa_q_bl_pen_total_positive_bound_product_terminal * S ((S (e)) * pa_v_bl_pen_total_positive_bound_product) + (B))) /\ forall pa_i_bl_pen_total_positive_bound_product. (exists pa_lt_bl_pen_total_positive_bound_product_bound. pa_lt_bl_pen_total_positive_bound_product_bound + S pa_i_bl_pen_total_positive_bound_product = e) -> exists pa_p_bl_pen_total_positive_bound_product pa_r_bl_pen_total_positive_bound_product pa_s_bl_pen_total_positive_bound_product. ((((exists pa_h_bl_pen_total_positive_bound_product_factor. pa_h_bl_pen_total_positive_bound_product_factor + S (pa_p_bl_pen_total_positive_bound_product) = S ((S (pa_i_bl_pen_total_positive_bound_product)) * pa_c_bl_pen_total_positive_bound)) /\ exists pa_q_bl_pen_total_positive_bound_product_factor. pa_b_bl_pen_total_positive_bound = pa_q_bl_pen_total_positive_bound_product_factor * S ((S (pa_i_bl_pen_total_positive_bound_product)) * pa_c_bl_pen_total_positive_bound) + (pa_p_bl_pen_total_positive_bound_product))) /\ ((((exists pa_h_bl_pen_total_positive_bound_product_partial. pa_h_bl_pen_total_positive_bound_product_partial + S (pa_r_bl_pen_total_positive_bound_product) = S ((S (pa_i_bl_pen_total_positive_bound_product)) * pa_v_bl_pen_total_positive_bound_product)) /\ exists pa_q_bl_pen_total_positive_bound_product_partial. pa_u_bl_pen_total_positive_bound_product = pa_q_bl_pen_total_positive_bound_product_partial * S ((S (pa_i_bl_pen_total_positive_bound_product)) * pa_v_bl_pen_total_positive_bound_product) + (pa_r_bl_pen_total_positive_bound_product))) /\ ((((exists pa_h_bl_pen_total_positive_bound_product_successor. pa_h_bl_pen_total_positive_bound_product_successor + S (pa_s_bl_pen_total_positive_bound_product) = S ((S (S pa_i_bl_pen_total_positive_bound_product)) * pa_v_bl_pen_total_positive_bound_product)) /\ exists pa_q_bl_pen_total_positive_bound_product_successor. pa_u_bl_pen_total_positive_bound_product = pa_q_bl_pen_total_positive_bound_product_successor * S ((S (S pa_i_bl_pen_total_positive_bound_product)) * pa_v_bl_pen_total_positive_bound_product) + (pa_s_bl_pen_total_positive_bound_product))) /\ pa_s_bl_pen_total_positive_bound_product = pa_r_bl_pen_total_positive_bound_product * pa_p_bl_pen_total_positive_bound_product)))))))) /\ (exists pc_lt_pen_total_positive_strict. pc_lt_pen_total_positive_strict + S (p) = (B))))))
  13. 0013apply first_primes_double_exponential_bound
  14. 0014exact hz_right
  15. 0015cases hpositive
  16. 0016cases hpositive_witness
  17. 0017cases hpositive_witness_witness
  18. 0018cases hpositive_witness_witness_witness
  19. 0019cases hpositive_witness_witness_witness_witness
  20. 0020cases hpositive_witness_witness_witness_witness_witness
  21. 0021cases hpositive_witness_witness_witness_witness_witness_witness
  22. 0022cases hpositive_witness_witness_witness_witness_witness_witness_right
  23. 0023exists x
  24. 0024exists x1
  25. 0025exact hpositive_witness_witness_witness_witness_witness_witness_right_left