PC000B

prime_count_positive_above_one

The actual prime two makes every prime count at bound at least two positive.

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. Lt(1,n) → PrimeCount(n,k) → Lt(0,k)

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

Definition DAG

PrimeCount(x,z) · 1Le(a,b) · 1Lt(a,b) · 2Prime(p) · 2BetaAt(b,c,i,x) · 1

Actual proof prerequisites

prime_two · checked external prerequisitebeta_at_exists · checked external prerequisiteprime_bit_prefix_entrybeta_sum_entry_le
Original expanded first-order statement 
forall n k. (exists pc_le_count_positive_bound. pc_le_count_positive_bound + (2) = (n)) -> (exists pc_code_count_positive_source pc_scale_count_positive_source. (forall pc_index_count_positive_source_mask. (exists pc_lt_count_positive_source_mask_bound. pc_lt_count_positive_source_mask_bound + S (pc_index_count_positive_source_mask) = (n)) -> exists pc_bit_count_positive_source_mask. (((exists fs_h_pc_count_positive_source_mask_entry. fs_h_pc_count_positive_source_mask_entry + S (pc_bit_count_positive_source_mask) = S ((S (pc_index_count_positive_source_mask)) * pc_scale_count_positive_source)) /\ exists fs_q_pc_count_positive_source_mask_entry. pc_code_count_positive_source = fs_q_pc_count_positive_source_mask_entry * S ((S (pc_index_count_positive_source_mask)) * pc_scale_count_positive_source) + (pc_bit_count_positive_source_mask))) /\ (((((~(S (pc_index_count_positive_source_mask) = 1) /\ forall bpr_left_pc_count_positive_source_mask_choice_prime bpr_right_pc_count_positive_source_mask_choice_prime. S (pc_index_count_positive_source_mask) = bpr_left_pc_count_positive_source_mask_choice_prime * bpr_right_pc_count_positive_source_mask_choice_prime -> bpr_left_pc_count_positive_source_mask_choice_prime = 1 \/ bpr_right_pc_count_positive_source_mask_choice_prime = 1)) /\ pc_bit_count_positive_source_mask = 1) \/ (~((~(S (pc_index_count_positive_source_mask) = 1) /\ forall bpr_left_pc_count_positive_source_mask_choice_prime bpr_right_pc_count_positive_source_mask_choice_prime. S (pc_index_count_positive_source_mask) = bpr_left_pc_count_positive_source_mask_choice_prime * bpr_right_pc_count_positive_source_mask_choice_prime -> bpr_left_pc_count_positive_source_mask_choice_prime = 1 \/ bpr_right_pc_count_positive_source_mask_choice_prime = 1)) /\ pc_bit_count_positive_source_mask = 0)))) /\ (exists fs_u_pc_count_positive_source_sum fs_v_pc_count_positive_source_sum. ((((exists fs_h_pc_count_positive_source_sum_body_start. fs_h_pc_count_positive_source_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_count_positive_source_sum)) /\ exists fs_q_pc_count_positive_source_sum_body_start. fs_u_pc_count_positive_source_sum = fs_q_pc_count_positive_source_sum_body_start * S ((S (0)) * fs_v_pc_count_positive_source_sum) + (0))) /\ ((((exists fs_h_pc_count_positive_source_sum_body_terminal. fs_h_pc_count_positive_source_sum_body_terminal + S (k) = S ((S (n)) * fs_v_pc_count_positive_source_sum)) /\ exists fs_q_pc_count_positive_source_sum_body_terminal. fs_u_pc_count_positive_source_sum = fs_q_pc_count_positive_source_sum_body_terminal * S ((S (n)) * fs_v_pc_count_positive_source_sum) + (k))) /\ forall fs_i_pc_count_positive_source_sum_body_steps. (exists fs_lt_pc_count_positive_source_sum_body_steps_bound. fs_lt_pc_count_positive_source_sum_body_steps_bound + S fs_i_pc_count_positive_source_sum_body_steps = n) -> exists fs_a_pc_count_positive_source_sum_body_steps fs_r_pc_count_positive_source_sum_body_steps fs_s_pc_count_positive_source_sum_body_steps. ((((exists fs_h_pc_count_positive_source_sum_body_steps_summand. fs_h_pc_count_positive_source_sum_body_steps_summand + S (fs_a_pc_count_positive_source_sum_body_steps) = S ((S (fs_i_pc_count_positive_source_sum_body_steps)) * pc_scale_count_positive_source)) /\ exists fs_q_pc_count_positive_source_sum_body_steps_summand. pc_code_count_positive_source = fs_q_pc_count_positive_source_sum_body_steps_summand * S ((S (fs_i_pc_count_positive_source_sum_body_steps)) * pc_scale_count_positive_source) + (fs_a_pc_count_positive_source_sum_body_steps))) /\ ((((exists fs_h_pc_count_positive_source_sum_body_steps_partial. fs_h_pc_count_positive_source_sum_body_steps_partial + S (fs_r_pc_count_positive_source_sum_body_steps) = S ((S (fs_i_pc_count_positive_source_sum_body_steps)) * fs_v_pc_count_positive_source_sum)) /\ exists fs_q_pc_count_positive_source_sum_body_steps_partial. fs_u_pc_count_positive_source_sum = fs_q_pc_count_positive_source_sum_body_steps_partial * S ((S (fs_i_pc_count_positive_source_sum_body_steps)) * fs_v_pc_count_positive_source_sum) + (fs_r_pc_count_positive_source_sum_body_steps))) /\ ((((exists fs_h_pc_count_positive_source_sum_body_steps_successor. fs_h_pc_count_positive_source_sum_body_steps_successor + S (fs_s_pc_count_positive_source_sum_body_steps) = S ((S (S fs_i_pc_count_positive_source_sum_body_steps)) * fs_v_pc_count_positive_source_sum)) /\ exists fs_q_pc_count_positive_source_sum_body_steps_successor. fs_u_pc_count_positive_source_sum = fs_q_pc_count_positive_source_sum_body_steps_successor * S ((S (S fs_i_pc_count_positive_source_sum_body_steps)) * fs_v_pc_count_positive_source_sum) + (fs_s_pc_count_positive_source_sum_body_steps))) /\ fs_s_pc_count_positive_source_sum_body_steps = fs_r_pc_count_positive_source_sum_body_steps + fs_a_pc_count_positive_source_sum_body_steps))))))) -> (exists pc_le_count_positive_result. pc_le_count_positive_result + (1) = (k))

Complete tactic proof in conservative notation

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

42 script commands · 12 reading checkpoints · 3 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 (2)
prime bit prefix entrybeta sum entry le
01Fix variables and assumptionsL1–4

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

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro hn
  4. L4
    intro h
02Separate the logical casesL5–7

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

  1. L5
    cases h
  2. L6
    cases h_witness
  3. L7
    cases h_witness_witness
03Establish heL8–12

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

  1. L8
    have he : ∃ e. BetaAt(x,x1,1,e)Definitions: BetaAt(x,x1,1,e)Original native command in the exact edition
  2. L9
    specialize beta_at_exists x
  3. L10
    specialize beta_at_exists x1
  4. L11
    specialize beta_at_exists 1
  5. L12
    apply beta_at_exists
04Separate the logical casesL13–13

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

  1. L13
    cases he
05Establish hcL14–23

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

  1. L14
    have hc : Prime(2) ∧ x2 = 1 ∨ ¬Prime(2) ∧ x2 = 0Definitions: Prime(2)Original native command in the exact edition
  2. L15
    specialize prime_bit_prefix_entry x
  3. L16
    specialize prime_bit_prefix_entry x1
  4. L17
    specialize prime_bit_prefix_entry n
  5. L18
    specialize prime_bit_prefix_entry 1
  6. L19
    specialize prime_bit_prefix_entry x2
  7. L20
    apply prime_bit_prefix_entry
  8. L21
    exact h_witness_witness_left
  9. L22
    exact hn
  10. L23
    exact he_witness
06Separate the logical casesL24–25

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

  1. L24
    cases hc
  2. L25
    cases hc_left
07Establish hleL26–35

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

  1. L26
  2. L27
    specialize beta_sum_entry_le x
  3. L28
    specialize beta_sum_entry_le x1
  4. L29
    specialize beta_sum_entry_le n
  5. L30
    specialize beta_sum_entry_le k
  6. L31
    specialize beta_sum_entry_le 1
  7. L32
    specialize beta_sum_entry_le x2
  8. L33
    apply beta_sum_entry_le
  9. L34
    exact h_witness_witness_right
  10. L35
    exact hn
08Use earlier factsL36–36

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

  1. L36
    exact he_witness
09Calculate and transport equalitiesL37–37

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

  1. L37
    rewrite hc_left_right at hle
10Use earlier factsL38–38

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

  1. L38
    exact hle
11Separate the logical casesL39–40

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

  1. L39
    cases hc_right
  2. L40
    exfalso
12Use earlier factsL41–42

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

  1. L41
    apply hc_right_left
  2. L42
    exact prime_two

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro hn
  4. 0004intro h
  5. 0005cases h
  6. 0006cases h_witness
  7. 0007cases h_witness_witness
  8. 0008have he : ∃ e. BetaAt(x,x1,1,e)
  9. 0009specialize beta_at_exists x
  10. 0010specialize beta_at_exists x1
  11. 0011specialize beta_at_exists 1
  12. 0012apply beta_at_exists
  13. 0013cases he
  14. 0014have hc : Prime(2) ∧ x2 = 1 ∨ ¬Prime(2) ∧ x2 = 0
  15. 0015specialize prime_bit_prefix_entry x
  16. 0016specialize prime_bit_prefix_entry x1
  17. 0017specialize prime_bit_prefix_entry n
  18. 0018specialize prime_bit_prefix_entry 1
  19. 0019specialize prime_bit_prefix_entry x2
  20. 0020apply prime_bit_prefix_entry
  21. 0021exact h_witness_witness_left
  22. 0022exact hn
  23. 0023exact he_witness
  24. 0024cases hc
  25. 0025cases hc_left
  26. 0026have hle : Le(x2,k)
  27. 0027specialize beta_sum_entry_le x
  28. 0028specialize beta_sum_entry_le x1
  29. 0029specialize beta_sum_entry_le n
  30. 0030specialize beta_sum_entry_le k
  31. 0031specialize beta_sum_entry_le 1
  32. 0032specialize beta_sum_entry_le x2
  33. 0033apply beta_sum_entry_le
  34. 0034exact h_witness_witness_right
  35. 0035exact hn
  36. 0036exact he_witness
  37. 0037rewrite hc_left_right at hle
  38. 0038exact hle
  39. 0039cases hc_right
  40. 0040exfalso
  41. 0041apply hc_right_left
  42. 0042exact prime_two