PC0031

prime_count_chebyshev_bounds

Exact G027: for every N at least two and its actual prime count and binary length, N <= 8*pi(N)*BitLen(N) and pi(N)*BitLen(N) <= 8N.

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. ∀ ell. ∀ k. Lt(1,N) → BitLen(N,ell) → PrimeCount(N,k) → Le(N,8 · k · ell) ∧ Le(k · ell,8 · N)

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

Definition DAG

BitLen(n,ell) · 1PrimeCount(x,z) · 1Le(a,b) · 2Lt(a,b) · 1

Actual proof prerequisites

prime_count_chebyshev_lowerprime_count_chebyshev_upper
Original expanded first-order statement 
forall N ell k. (exists pc_le_cheb_full_positive. pc_le_cheb_full_positive + (2) = (N)) -> ((((N) = 0 /\ (ell) = 1) \/ exists ff_exponent_bl_pc_cheb_full_length ff_lower_bl_pc_cheb_full_length ff_upper_bl_pc_cheb_full_length. (((ell) = S ff_exponent_bl_pc_cheb_full_length) /\ ((exists ff_positive_bl_pc_cheb_full_length. ff_positive_bl_pc_cheb_full_length + 1 = (N)) /\ ((exists pa_b_bl_pc_cheb_full_length_lower pa_c_bl_pc_cheb_full_length_lower. ((forall pa_i_bl_pc_cheb_full_length_lower_repeat. (exists pa_lt_bl_pc_cheb_full_length_lower_repeat_bound. pa_lt_bl_pc_cheb_full_length_lower_repeat_bound + S pa_i_bl_pc_cheb_full_length_lower_repeat = ff_exponent_bl_pc_cheb_full_length) -> (((exists pa_h_bl_pc_cheb_full_length_lower_repeat_decoded. pa_h_bl_pc_cheb_full_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_cheb_full_length_lower_repeat)) * pa_c_bl_pc_cheb_full_length_lower)) /\ exists pa_q_bl_pc_cheb_full_length_lower_repeat_decoded. pa_b_bl_pc_cheb_full_length_lower = pa_q_bl_pc_cheb_full_length_lower_repeat_decoded * S ((S (pa_i_bl_pc_cheb_full_length_lower_repeat)) * pa_c_bl_pc_cheb_full_length_lower) + (2)))) /\ (exists pa_u_bl_pc_cheb_full_length_lower_product pa_v_bl_pc_cheb_full_length_lower_product. ((((exists pa_h_bl_pc_cheb_full_length_lower_product_start. pa_h_bl_pc_cheb_full_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_cheb_full_length_lower_product)) /\ exists pa_q_bl_pc_cheb_full_length_lower_product_start. pa_u_bl_pc_cheb_full_length_lower_product = pa_q_bl_pc_cheb_full_length_lower_product_start * S ((S (0)) * pa_v_bl_pc_cheb_full_length_lower_product) + (1))) /\ ((((exists pa_h_bl_pc_cheb_full_length_lower_product_terminal. pa_h_bl_pc_cheb_full_length_lower_product_terminal + S (ff_lower_bl_pc_cheb_full_length) = S ((S (ff_exponent_bl_pc_cheb_full_length)) * pa_v_bl_pc_cheb_full_length_lower_product)) /\ exists pa_q_bl_pc_cheb_full_length_lower_product_terminal. pa_u_bl_pc_cheb_full_length_lower_product = pa_q_bl_pc_cheb_full_length_lower_product_terminal * S ((S (ff_exponent_bl_pc_cheb_full_length)) * pa_v_bl_pc_cheb_full_length_lower_product) + (ff_lower_bl_pc_cheb_full_length))) /\ forall pa_i_bl_pc_cheb_full_length_lower_product. (exists pa_lt_bl_pc_cheb_full_length_lower_product_bound. pa_lt_bl_pc_cheb_full_length_lower_product_bound + S pa_i_bl_pc_cheb_full_length_lower_product = ff_exponent_bl_pc_cheb_full_length) -> exists pa_p_bl_pc_cheb_full_length_lower_product pa_r_bl_pc_cheb_full_length_lower_product pa_s_bl_pc_cheb_full_length_lower_product. ((((exists pa_h_bl_pc_cheb_full_length_lower_product_factor. pa_h_bl_pc_cheb_full_length_lower_product_factor + S (pa_p_bl_pc_cheb_full_length_lower_product) = S ((S (pa_i_bl_pc_cheb_full_length_lower_product)) * pa_c_bl_pc_cheb_full_length_lower)) /\ exists pa_q_bl_pc_cheb_full_length_lower_product_factor. pa_b_bl_pc_cheb_full_length_lower = pa_q_bl_pc_cheb_full_length_lower_product_factor * S ((S (pa_i_bl_pc_cheb_full_length_lower_product)) * pa_c_bl_pc_cheb_full_length_lower) + (pa_p_bl_pc_cheb_full_length_lower_product))) /\ ((((exists pa_h_bl_pc_cheb_full_length_lower_product_partial. pa_h_bl_pc_cheb_full_length_lower_product_partial + S (pa_r_bl_pc_cheb_full_length_lower_product) = S ((S (pa_i_bl_pc_cheb_full_length_lower_product)) * pa_v_bl_pc_cheb_full_length_lower_product)) /\ exists pa_q_bl_pc_cheb_full_length_lower_product_partial. pa_u_bl_pc_cheb_full_length_lower_product = pa_q_bl_pc_cheb_full_length_lower_product_partial * S ((S (pa_i_bl_pc_cheb_full_length_lower_product)) * pa_v_bl_pc_cheb_full_length_lower_product) + (pa_r_bl_pc_cheb_full_length_lower_product))) /\ ((((exists pa_h_bl_pc_cheb_full_length_lower_product_successor. pa_h_bl_pc_cheb_full_length_lower_product_successor + S (pa_s_bl_pc_cheb_full_length_lower_product) = S ((S (S pa_i_bl_pc_cheb_full_length_lower_product)) * pa_v_bl_pc_cheb_full_length_lower_product)) /\ exists pa_q_bl_pc_cheb_full_length_lower_product_successor. pa_u_bl_pc_cheb_full_length_lower_product = pa_q_bl_pc_cheb_full_length_lower_product_successor * S ((S (S pa_i_bl_pc_cheb_full_length_lower_product)) * pa_v_bl_pc_cheb_full_length_lower_product) + (pa_s_bl_pc_cheb_full_length_lower_product))) /\ pa_s_bl_pc_cheb_full_length_lower_product = pa_r_bl_pc_cheb_full_length_lower_product * pa_p_bl_pc_cheb_full_length_lower_product)))))))) /\ ((exists pa_b_bl_pc_cheb_full_length_upper pa_c_bl_pc_cheb_full_length_upper. ((forall pa_i_bl_pc_cheb_full_length_upper_repeat. (exists pa_lt_bl_pc_cheb_full_length_upper_repeat_bound. pa_lt_bl_pc_cheb_full_length_upper_repeat_bound + S pa_i_bl_pc_cheb_full_length_upper_repeat = ell) -> (((exists pa_h_bl_pc_cheb_full_length_upper_repeat_decoded. pa_h_bl_pc_cheb_full_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_cheb_full_length_upper_repeat)) * pa_c_bl_pc_cheb_full_length_upper)) /\ exists pa_q_bl_pc_cheb_full_length_upper_repeat_decoded. pa_b_bl_pc_cheb_full_length_upper = pa_q_bl_pc_cheb_full_length_upper_repeat_decoded * S ((S (pa_i_bl_pc_cheb_full_length_upper_repeat)) * pa_c_bl_pc_cheb_full_length_upper) + (2)))) /\ (exists pa_u_bl_pc_cheb_full_length_upper_product pa_v_bl_pc_cheb_full_length_upper_product. ((((exists pa_h_bl_pc_cheb_full_length_upper_product_start. pa_h_bl_pc_cheb_full_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_cheb_full_length_upper_product)) /\ exists pa_q_bl_pc_cheb_full_length_upper_product_start. pa_u_bl_pc_cheb_full_length_upper_product = pa_q_bl_pc_cheb_full_length_upper_product_start * S ((S (0)) * pa_v_bl_pc_cheb_full_length_upper_product) + (1))) /\ ((((exists pa_h_bl_pc_cheb_full_length_upper_product_terminal. pa_h_bl_pc_cheb_full_length_upper_product_terminal + S (ff_upper_bl_pc_cheb_full_length) = S ((S (ell)) * pa_v_bl_pc_cheb_full_length_upper_product)) /\ exists pa_q_bl_pc_cheb_full_length_upper_product_terminal. pa_u_bl_pc_cheb_full_length_upper_product = pa_q_bl_pc_cheb_full_length_upper_product_terminal * S ((S (ell)) * pa_v_bl_pc_cheb_full_length_upper_product) + (ff_upper_bl_pc_cheb_full_length))) /\ forall pa_i_bl_pc_cheb_full_length_upper_product. (exists pa_lt_bl_pc_cheb_full_length_upper_product_bound. pa_lt_bl_pc_cheb_full_length_upper_product_bound + S pa_i_bl_pc_cheb_full_length_upper_product = ell) -> exists pa_p_bl_pc_cheb_full_length_upper_product pa_r_bl_pc_cheb_full_length_upper_product pa_s_bl_pc_cheb_full_length_upper_product. ((((exists pa_h_bl_pc_cheb_full_length_upper_product_factor. pa_h_bl_pc_cheb_full_length_upper_product_factor + S (pa_p_bl_pc_cheb_full_length_upper_product) = S ((S (pa_i_bl_pc_cheb_full_length_upper_product)) * pa_c_bl_pc_cheb_full_length_upper)) /\ exists pa_q_bl_pc_cheb_full_length_upper_product_factor. pa_b_bl_pc_cheb_full_length_upper = pa_q_bl_pc_cheb_full_length_upper_product_factor * S ((S (pa_i_bl_pc_cheb_full_length_upper_product)) * pa_c_bl_pc_cheb_full_length_upper) + (pa_p_bl_pc_cheb_full_length_upper_product))) /\ ((((exists pa_h_bl_pc_cheb_full_length_upper_product_partial. pa_h_bl_pc_cheb_full_length_upper_product_partial + S (pa_r_bl_pc_cheb_full_length_upper_product) = S ((S (pa_i_bl_pc_cheb_full_length_upper_product)) * pa_v_bl_pc_cheb_full_length_upper_product)) /\ exists pa_q_bl_pc_cheb_full_length_upper_product_partial. pa_u_bl_pc_cheb_full_length_upper_product = pa_q_bl_pc_cheb_full_length_upper_product_partial * S ((S (pa_i_bl_pc_cheb_full_length_upper_product)) * pa_v_bl_pc_cheb_full_length_upper_product) + (pa_r_bl_pc_cheb_full_length_upper_product))) /\ ((((exists pa_h_bl_pc_cheb_full_length_upper_product_successor. pa_h_bl_pc_cheb_full_length_upper_product_successor + S (pa_s_bl_pc_cheb_full_length_upper_product) = S ((S (S pa_i_bl_pc_cheb_full_length_upper_product)) * pa_v_bl_pc_cheb_full_length_upper_product)) /\ exists pa_q_bl_pc_cheb_full_length_upper_product_successor. pa_u_bl_pc_cheb_full_length_upper_product = pa_q_bl_pc_cheb_full_length_upper_product_successor * S ((S (S pa_i_bl_pc_cheb_full_length_upper_product)) * pa_v_bl_pc_cheb_full_length_upper_product) + (pa_s_bl_pc_cheb_full_length_upper_product))) /\ pa_s_bl_pc_cheb_full_length_upper_product = pa_r_bl_pc_cheb_full_length_upper_product * pa_p_bl_pc_cheb_full_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_pc_cheb_full_length. ff_lower_gap_bl_pc_cheb_full_length + (ff_lower_bl_pc_cheb_full_length) = (N)) /\ (exists ff_upper_gap_bl_pc_cheb_full_length. ff_upper_gap_bl_pc_cheb_full_length + S (N) = (ff_upper_bl_pc_cheb_full_length))))))))) -> (exists pc_code_cheb_full_count pc_scale_cheb_full_count. (forall pc_index_cheb_full_count_mask. (exists pc_lt_cheb_full_count_mask_bound. pc_lt_cheb_full_count_mask_bound + S (pc_index_cheb_full_count_mask) = (N)) -> exists pc_bit_cheb_full_count_mask. (((exists fs_h_pc_cheb_full_count_mask_entry. fs_h_pc_cheb_full_count_mask_entry + S (pc_bit_cheb_full_count_mask) = S ((S (pc_index_cheb_full_count_mask)) * pc_scale_cheb_full_count)) /\ exists fs_q_pc_cheb_full_count_mask_entry. pc_code_cheb_full_count = fs_q_pc_cheb_full_count_mask_entry * S ((S (pc_index_cheb_full_count_mask)) * pc_scale_cheb_full_count) + (pc_bit_cheb_full_count_mask))) /\ (((((~(S (pc_index_cheb_full_count_mask) = 1) /\ forall bpr_left_pc_cheb_full_count_mask_choice_prime bpr_right_pc_cheb_full_count_mask_choice_prime. S (pc_index_cheb_full_count_mask) = bpr_left_pc_cheb_full_count_mask_choice_prime * bpr_right_pc_cheb_full_count_mask_choice_prime -> bpr_left_pc_cheb_full_count_mask_choice_prime = 1 \/ bpr_right_pc_cheb_full_count_mask_choice_prime = 1)) /\ pc_bit_cheb_full_count_mask = 1) \/ (~((~(S (pc_index_cheb_full_count_mask) = 1) /\ forall bpr_left_pc_cheb_full_count_mask_choice_prime bpr_right_pc_cheb_full_count_mask_choice_prime. S (pc_index_cheb_full_count_mask) = bpr_left_pc_cheb_full_count_mask_choice_prime * bpr_right_pc_cheb_full_count_mask_choice_prime -> bpr_left_pc_cheb_full_count_mask_choice_prime = 1 \/ bpr_right_pc_cheb_full_count_mask_choice_prime = 1)) /\ pc_bit_cheb_full_count_mask = 0)))) /\ (exists fs_u_pc_cheb_full_count_sum fs_v_pc_cheb_full_count_sum. ((((exists fs_h_pc_cheb_full_count_sum_body_start. fs_h_pc_cheb_full_count_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_cheb_full_count_sum)) /\ exists fs_q_pc_cheb_full_count_sum_body_start. fs_u_pc_cheb_full_count_sum = fs_q_pc_cheb_full_count_sum_body_start * S ((S (0)) * fs_v_pc_cheb_full_count_sum) + (0))) /\ ((((exists fs_h_pc_cheb_full_count_sum_body_terminal. fs_h_pc_cheb_full_count_sum_body_terminal + S (k) = S ((S (N)) * fs_v_pc_cheb_full_count_sum)) /\ exists fs_q_pc_cheb_full_count_sum_body_terminal. fs_u_pc_cheb_full_count_sum = fs_q_pc_cheb_full_count_sum_body_terminal * S ((S (N)) * fs_v_pc_cheb_full_count_sum) + (k))) /\ forall fs_i_pc_cheb_full_count_sum_body_steps. (exists fs_lt_pc_cheb_full_count_sum_body_steps_bound. fs_lt_pc_cheb_full_count_sum_body_steps_bound + S fs_i_pc_cheb_full_count_sum_body_steps = N) -> exists fs_a_pc_cheb_full_count_sum_body_steps fs_r_pc_cheb_full_count_sum_body_steps fs_s_pc_cheb_full_count_sum_body_steps. ((((exists fs_h_pc_cheb_full_count_sum_body_steps_summand. fs_h_pc_cheb_full_count_sum_body_steps_summand + S (fs_a_pc_cheb_full_count_sum_body_steps) = S ((S (fs_i_pc_cheb_full_count_sum_body_steps)) * pc_scale_cheb_full_count)) /\ exists fs_q_pc_cheb_full_count_sum_body_steps_summand. pc_code_cheb_full_count = fs_q_pc_cheb_full_count_sum_body_steps_summand * S ((S (fs_i_pc_cheb_full_count_sum_body_steps)) * pc_scale_cheb_full_count) + (fs_a_pc_cheb_full_count_sum_body_steps))) /\ ((((exists fs_h_pc_cheb_full_count_sum_body_steps_partial. fs_h_pc_cheb_full_count_sum_body_steps_partial + S (fs_r_pc_cheb_full_count_sum_body_steps) = S ((S (fs_i_pc_cheb_full_count_sum_body_steps)) * fs_v_pc_cheb_full_count_sum)) /\ exists fs_q_pc_cheb_full_count_sum_body_steps_partial. fs_u_pc_cheb_full_count_sum = fs_q_pc_cheb_full_count_sum_body_steps_partial * S ((S (fs_i_pc_cheb_full_count_sum_body_steps)) * fs_v_pc_cheb_full_count_sum) + (fs_r_pc_cheb_full_count_sum_body_steps))) /\ ((((exists fs_h_pc_cheb_full_count_sum_body_steps_successor. fs_h_pc_cheb_full_count_sum_body_steps_successor + S (fs_s_pc_cheb_full_count_sum_body_steps) = S ((S (S fs_i_pc_cheb_full_count_sum_body_steps)) * fs_v_pc_cheb_full_count_sum)) /\ exists fs_q_pc_cheb_full_count_sum_body_steps_successor. fs_u_pc_cheb_full_count_sum = fs_q_pc_cheb_full_count_sum_body_steps_successor * S ((S (S fs_i_pc_cheb_full_count_sum_body_steps)) * fs_v_pc_cheb_full_count_sum) + (fs_s_pc_cheb_full_count_sum_body_steps))) /\ fs_s_pc_cheb_full_count_sum_body_steps = fs_r_pc_cheb_full_count_sum_body_steps + fs_a_pc_cheb_full_count_sum_body_steps))))))) -> (exists pc_le_cheb_full_lower. pc_le_cheb_full_lower + (N) = (8 * k * ell)) /\ (exists pc_le_cheb_full_upper. pc_le_cheb_full_upper + (k * ell) = (8 * N))

Complete tactic proof in conservative notation

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

21 script commands · 4 reading checkpoints · 0 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 count chebyshev lowerprime count chebyshev upper
01Fix variables and assumptionsL1–6

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

  1. L1
    intro N
  2. L2
    intro ell
  3. L3
    intro k
  4. L4
    intro hN
  5. L5
    intro hl
  6. L6
    intro hk
02Separate the logical casesL7–7

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

  1. L7
    split
03Use earlier factsL8–17

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

  1. L8
    specialize prime_count_chebyshev_lower N
  2. L9
    specialize prime_count_chebyshev_lower ell
  3. L10
    specialize prime_count_chebyshev_lower k
  4. L11
    apply prime_count_chebyshev_lower
  5. L12
    exact hN
  6. L13
    exact hl
  7. L14
    exact hk
  8. L15
    specialize prime_count_chebyshev_upper N
  9. L16
    specialize prime_count_chebyshev_upper ell
  10. L17
    specialize prime_count_chebyshev_upper k
04Use earlier factsL18–21

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

  1. L18
    apply prime_count_chebyshev_upper
  2. L19
    exact hN
  3. L20
    exact hl
  4. L21
    exact hk

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro N
  2. 0002intro ell
  3. 0003intro k
  4. 0004intro hN
  5. 0005intro hl
  6. 0006intro hk
  7. 0007split
  8. 0008specialize prime_count_chebyshev_lower N
  9. 0009specialize prime_count_chebyshev_lower ell
  10. 0010specialize prime_count_chebyshev_lower k
  11. 0011apply prime_count_chebyshev_lower
  12. 0012exact hN
  13. 0013exact hl
  14. 0014exact hk
  15. 0015specialize prime_count_chebyshev_upper N
  16. 0016specialize prime_count_chebyshev_upper ell
  17. 0017specialize prime_count_chebyshev_upper k
  18. 0018apply prime_count_chebyshev_upper
  19. 0019exact hN
  20. 0020exact hl
  21. 0021exact hk