PC000B

prime_count_positive_above_one

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 42 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_two Stable theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized PC0004 prime_bit_prefix_entry PC000A beta_sum_entry_le

Direct dependents

PC0030 prime_count_chebyshev_lower

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

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.

Named ingredients (2)
prime bit prefix entrybeta sum entry le

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–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 : exists e. ((exists fs_h_pc_count_positive_entry. fs_h_pc_count_positive_entry + S (e) = S ((S (1)) * x1)) /\ exists fs_q_pc_count_positive_entry. x = fs_q_pc_count_positive_entry * S ((S (1)) * x1) + (e))
  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. 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
    have hle : exists g. g + x2 = k
  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 exact 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 : exists e. ((exists fs_h_pc_count_positive_entry. fs_h_pc_count_positive_entry + S (e) = S ((S (1)) * x1)) /\ exists fs_q_pc_count_positive_entry. x = fs_q_pc_count_positive_entry * S ((S (1)) * x1) + (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 : ((((~(S (1) = 1) /\ forall bpr_left_pc_count_positive_choice_prime bpr_right_pc_count_positive_choice_prime. S (1) = bpr_left_pc_count_positive_choice_prime * bpr_right_pc_count_positive_choice_prime -> bpr_left_pc_count_positive_choice_prime = 1 \/ bpr_right_pc_count_positive_choice_prime = 1)) /\ x2 = 1) \/ (~((~(S (1) = 1) /\ forall bpr_left_pc_count_positive_choice_prime bpr_right_pc_count_positive_choice_prime. S (1) = bpr_left_pc_count_positive_choice_prime * bpr_right_pc_count_positive_choice_prime -> bpr_left_pc_count_positive_choice_prime = 1 \/ bpr_right_pc_count_positive_choice_prime = 1)) /\ 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 : exists g. g + 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