PC0008

prime_count_exists

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

Alpha v34 checked-use · first admitted v27 · 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.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ n. ∃ k. PrimeCount(n,k)

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

Definition DAG

PrimeBitPrefix(b,c,l) · 1PrimeCount(x,z) · 1Sum(b,c,l,z) · 1

Actual proof prerequisites

prime_bit_prefix_existsbeta_sum_exists · checked external prerequisite
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

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

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.

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)
prime bit prefix exists
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(b,c,n)Original native command in the exact edition
  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(x,x1,n,k)Original native command in the exact edition
  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 defined command ledger · 18 lines
  1. 0001intro n
  2. 0002have hm : ∃ b. ∃ c. PrimeBitPrefix(b,c,n)
  3. 0003specialize prime_bit_prefix_exists n
  4. 0004apply prime_bit_prefix_exists
  5. 0005cases hm
  6. 0006cases hm_witness
  7. 0007have hs : ∃ k. Sum(x,x1,n,k)
  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