PC0008

prime_count_exists

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

Construct the exact prime count for every bound, including zero and one.

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 n. exists k. exists pc_code_count_exists pc_scale_count_exists. (forall pc_index_count_exists_mask. (exists pc_lt_count_exists_mask_bound. pc_lt_count_exists_mask_bound + S (pc_index_count_exists_mask) = (n)) -> exists pc_bit_count_exists_mask. (((exists fs_h_pc_count_exists_mask_entry. fs_h_pc_count_exists_mask_entry + S (pc_bit_count_exists_mask) = S ((S (pc_index_count_exists_mask)) * pc_scale_count_exists)) /\ exists fs_q_pc_count_exists_mask_entry. pc_code_count_exists = fs_q_pc_count_exists_mask_entry * S ((S (pc_index_count_exists_mask)) * pc_scale_count_exists) + (pc_bit_count_exists_mask))) /\ (((((~(S (pc_index_count_exists_mask) = 1) /\ forall bpr_left_pc_count_exists_mask_choice_prime bpr_right_pc_count_exists_mask_choice_prime. S (pc_index_count_exists_mask) = bpr_left_pc_count_exists_mask_choice_prime * bpr_right_pc_count_exists_mask_choice_prime -> bpr_left_pc_count_exists_mask_choice_prime = 1 \/ bpr_right_pc_count_exists_mask_choice_prime = 1)) /\ pc_bit_count_exists_mask = 1) \/ (~((~(S (pc_index_count_exists_mask) = 1) /\ forall bpr_left_pc_count_exists_mask_choice_prime bpr_right_pc_count_exists_mask_choice_prime. S (pc_index_count_exists_mask) = bpr_left_pc_count_exists_mask_choice_prime * bpr_right_pc_count_exists_mask_choice_prime -> bpr_left_pc_count_exists_mask_choice_prime = 1 \/ bpr_right_pc_count_exists_mask_choice_prime = 1)) /\ pc_bit_count_exists_mask = 0)))) /\ (exists fs_u_pc_count_exists_sum fs_v_pc_count_exists_sum. ((((exists fs_h_pc_count_exists_sum_body_start. fs_h_pc_count_exists_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_count_exists_sum)) /\ exists fs_q_pc_count_exists_sum_body_start. fs_u_pc_count_exists_sum = fs_q_pc_count_exists_sum_body_start * S ((S (0)) * fs_v_pc_count_exists_sum) + (0))) /\ ((((exists fs_h_pc_count_exists_sum_body_terminal. fs_h_pc_count_exists_sum_body_terminal + S (k) = S ((S (n)) * fs_v_pc_count_exists_sum)) /\ exists fs_q_pc_count_exists_sum_body_terminal. fs_u_pc_count_exists_sum = fs_q_pc_count_exists_sum_body_terminal * S ((S (n)) * fs_v_pc_count_exists_sum) + (k))) /\ forall fs_i_pc_count_exists_sum_body_steps. (exists fs_lt_pc_count_exists_sum_body_steps_bound. fs_lt_pc_count_exists_sum_body_steps_bound + S fs_i_pc_count_exists_sum_body_steps = n) -> exists fs_a_pc_count_exists_sum_body_steps fs_r_pc_count_exists_sum_body_steps fs_s_pc_count_exists_sum_body_steps. ((((exists fs_h_pc_count_exists_sum_body_steps_summand. fs_h_pc_count_exists_sum_body_steps_summand + S (fs_a_pc_count_exists_sum_body_steps) = S ((S (fs_i_pc_count_exists_sum_body_steps)) * pc_scale_count_exists)) /\ exists fs_q_pc_count_exists_sum_body_steps_summand. pc_code_count_exists = fs_q_pc_count_exists_sum_body_steps_summand * S ((S (fs_i_pc_count_exists_sum_body_steps)) * pc_scale_count_exists) + (fs_a_pc_count_exists_sum_body_steps))) /\ ((((exists fs_h_pc_count_exists_sum_body_steps_partial. fs_h_pc_count_exists_sum_body_steps_partial + S (fs_r_pc_count_exists_sum_body_steps) = S ((S (fs_i_pc_count_exists_sum_body_steps)) * fs_v_pc_count_exists_sum)) /\ exists fs_q_pc_count_exists_sum_body_steps_partial. fs_u_pc_count_exists_sum = fs_q_pc_count_exists_sum_body_steps_partial * S ((S (fs_i_pc_count_exists_sum_body_steps)) * fs_v_pc_count_exists_sum) + (fs_r_pc_count_exists_sum_body_steps))) /\ ((((exists fs_h_pc_count_exists_sum_body_steps_successor. fs_h_pc_count_exists_sum_body_steps_successor + S (fs_s_pc_count_exists_sum_body_steps) = S ((S (S fs_i_pc_count_exists_sum_body_steps)) * fs_v_pc_count_exists_sum)) /\ exists fs_q_pc_count_exists_sum_body_steps_successor. fs_u_pc_count_exists_sum = fs_q_pc_count_exists_sum_body_steps_successor * S ((S (S fs_i_pc_count_exists_sum_body_steps)) * fs_v_pc_count_exists_sum) + (fs_s_pc_count_exists_sum_body_steps))) /\ fs_s_pc_count_exists_sum_body_steps = fs_r_pc_count_exists_sum_body_steps + fs_a_pc_count_exists_sum_body_steps))))))

Constructive proof overview

Generated structural guide

Construct the exact prime count for every bound, including zero and one.

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

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

Proof neighborhood

Direct dependencies

PC0006 prime_bit_prefix_exists beta_sum_exists Stable theorem; checked-use authorized

Direct dependents

PC0037 prime_count_exists_unique

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

18 script commands · 8 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)
prime bit prefix exists

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 n
02Establish hmL2–4

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

  1. L2
    have hm : ∃ b. ∃ c. PrimeBitPrefix(b,c,n)Definitions: PrimeBitPrefix
  2. L3
    specialize prime_bit_prefix_exists n
  3. L4
    apply prime_bit_prefix_exists
03Separate the logical casesL5–6

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

  1. L5
    cases hm
  2. L6
    cases hm_witness
04Establish hsL7–11

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

  1. L7
    have hs : ∃ k. Sum(x,x1,n,k)Definitions: Sum
  2. L8
    specialize beta_sum_exists x
  3. L9
    specialize beta_sum_exists x1
  4. L10
    specialize beta_sum_exists n
  5. L11
    apply beta_sum_exists
05Separate the logical casesL12–12

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

  1. L12
    cases hs
06Construct an explicit witnessL13–15

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

  1. L13
    exists x2
  2. L14
    exists x
  3. L15
    exists x1
07Separate the logical casesL16–16

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

  1. L16
    split
08Use earlier factsL17–18

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

  1. L17
    exact hm_witness_witness
  2. L18
    exact hs_witness

Library-wide reading audit

Original exact command ledger · 18 lines
  1. 0001intro n
  2. 0002have hm : exists b c. forall pc_index_count_exists_mask. (exists pc_lt_count_exists_mask_bound. pc_lt_count_exists_mask_bound + S (pc_index_count_exists_mask) = (n)) -> exists pc_bit_count_exists_mask. (((exists fs_h_pc_count_exists_mask_entry. fs_h_pc_count_exists_mask_entry + S (pc_bit_count_exists_mask) = S ((S (pc_index_count_exists_mask)) * c)) /\ exists fs_q_pc_count_exists_mask_entry. b = fs_q_pc_count_exists_mask_entry * S ((S (pc_index_count_exists_mask)) * c) + (pc_bit_count_exists_mask))) /\ (((((~(S (pc_index_count_exists_mask) = 1) /\ forall bpr_left_pc_count_exists_mask_choice_prime bpr_right_pc_count_exists_mask_choice_prime. S (pc_index_count_exists_mask) = bpr_left_pc_count_exists_mask_choice_prime * bpr_right_pc_count_exists_mask_choice_prime -> bpr_left_pc_count_exists_mask_choice_prime = 1 \/ bpr_right_pc_count_exists_mask_choice_prime = 1)) /\ pc_bit_count_exists_mask = 1) \/ (~((~(S (pc_index_count_exists_mask) = 1) /\ forall bpr_left_pc_count_exists_mask_choice_prime bpr_right_pc_count_exists_mask_choice_prime. S (pc_index_count_exists_mask) = bpr_left_pc_count_exists_mask_choice_prime * bpr_right_pc_count_exists_mask_choice_prime -> bpr_left_pc_count_exists_mask_choice_prime = 1 \/ bpr_right_pc_count_exists_mask_choice_prime = 1)) /\ pc_bit_count_exists_mask = 0)))
  3. 0003specialize prime_bit_prefix_exists n
  4. 0004apply prime_bit_prefix_exists
  5. 0005cases hm
  6. 0006cases hm_witness
  7. 0007have hs : exists k. exists fs_u_pc_count_exists_sum fs_v_pc_count_exists_sum. ((((exists fs_h_pc_count_exists_sum_body_start. fs_h_pc_count_exists_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_count_exists_sum)) /\ exists fs_q_pc_count_exists_sum_body_start. fs_u_pc_count_exists_sum = fs_q_pc_count_exists_sum_body_start * S ((S (0)) * fs_v_pc_count_exists_sum) + (0))) /\ ((((exists fs_h_pc_count_exists_sum_body_terminal. fs_h_pc_count_exists_sum_body_terminal + S (k) = S ((S (n)) * fs_v_pc_count_exists_sum)) /\ exists fs_q_pc_count_exists_sum_body_terminal. fs_u_pc_count_exists_sum = fs_q_pc_count_exists_sum_body_terminal * S ((S (n)) * fs_v_pc_count_exists_sum) + (k))) /\ forall fs_i_pc_count_exists_sum_body_steps. (exists fs_lt_pc_count_exists_sum_body_steps_bound. fs_lt_pc_count_exists_sum_body_steps_bound + S fs_i_pc_count_exists_sum_body_steps = n) -> exists fs_a_pc_count_exists_sum_body_steps fs_r_pc_count_exists_sum_body_steps fs_s_pc_count_exists_sum_body_steps. ((((exists fs_h_pc_count_exists_sum_body_steps_summand. fs_h_pc_count_exists_sum_body_steps_summand + S (fs_a_pc_count_exists_sum_body_steps) = S ((S (fs_i_pc_count_exists_sum_body_steps)) * x1)) /\ exists fs_q_pc_count_exists_sum_body_steps_summand. x = fs_q_pc_count_exists_sum_body_steps_summand * S ((S (fs_i_pc_count_exists_sum_body_steps)) * x1) + (fs_a_pc_count_exists_sum_body_steps))) /\ ((((exists fs_h_pc_count_exists_sum_body_steps_partial. fs_h_pc_count_exists_sum_body_steps_partial + S (fs_r_pc_count_exists_sum_body_steps) = S ((S (fs_i_pc_count_exists_sum_body_steps)) * fs_v_pc_count_exists_sum)) /\ exists fs_q_pc_count_exists_sum_body_steps_partial. fs_u_pc_count_exists_sum = fs_q_pc_count_exists_sum_body_steps_partial * S ((S (fs_i_pc_count_exists_sum_body_steps)) * fs_v_pc_count_exists_sum) + (fs_r_pc_count_exists_sum_body_steps))) /\ ((((exists fs_h_pc_count_exists_sum_body_steps_successor. fs_h_pc_count_exists_sum_body_steps_successor + S (fs_s_pc_count_exists_sum_body_steps) = S ((S (S fs_i_pc_count_exists_sum_body_steps)) * fs_v_pc_count_exists_sum)) /\ exists fs_q_pc_count_exists_sum_body_steps_successor. fs_u_pc_count_exists_sum = fs_q_pc_count_exists_sum_body_steps_successor * S ((S (S fs_i_pc_count_exists_sum_body_steps)) * fs_v_pc_count_exists_sum) + (fs_s_pc_count_exists_sum_body_steps))) /\ fs_s_pc_count_exists_sum_body_steps = fs_r_pc_count_exists_sum_body_steps + fs_a_pc_count_exists_sum_body_steps)))))
  8. 0008specialize beta_sum_exists x
  9. 0009specialize beta_sum_exists x1
  10. 0010specialize beta_sum_exists n
  11. 0011apply beta_sum_exists
  12. 0012cases hs
  13. 0013exists x2
  14. 0014exists x
  15. 0015exists x1
  16. 0016split
  17. 0017exact hm_witness_witness
  18. 0018exact hs_witness