PC002E — central_binom_prime_count_exponent_bound

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. ∀ h. Lt(3,h) → Le(h + h,N) → BitLen(N,ell) → PrimeCount(N,k) → Le(h,ell · k)

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

Definition DAG

PowTwo(e,p) · 3 BitLen(n,ell) · 1 PrimeCount(x,z) · 1 Le(a,b) · 6 Lt(a,b) · 2 Pow(a,e,z) · 2 CentralBinom(n,z) · 1

Actual proof prerequisites

central_binom_exists · checked external prerequisitepow_exists · checked external prerequisitebinary_length_upper_power_bound · checked external prerequisitecentral_binom_prime_count_power_bound central_binom_dominates_pow_twole_trans · checked external prerequisitelt_to_le · checked external prerequisitepow_base_monotone · checked external prerequisitepow_mul_exp · checked external prerequisitebinary_power_two_order_reflects_exponent

Original expanded first-order statement

forall N ell k h. (exists pc_le_central_exp_half_positive. pc_le_central_exp_half_positive + (4) = (h)) -> (exists pc_le_central_exp_range. pc_le_central_exp_range + (h + h) = (N)) -> ((((N) = 0 /\ (ell) = 1) \/ exists ff_exponent_bl_pc_central_exp_length ff_lower_bl_pc_central_exp_length ff_upper_bl_pc_central_exp_length. (((ell) = S ff_exponent_bl_pc_central_exp_length) /\ ((exists ff_positive_bl_pc_central_exp_length. ff_positive_bl_pc_central_exp_length + 1 = (N)) /\ ((exists pa_b_bl_pc_central_exp_length_lower pa_c_bl_pc_central_exp_length_lower. ((forall pa_i_bl_pc_central_exp_length_lower_repeat. (exists pa_lt_bl_pc_central_exp_length_lower_repeat_bound. pa_lt_bl_pc_central_exp_length_lower_repeat_bound + S pa_i_bl_pc_central_exp_length_lower_repeat = ff_exponent_bl_pc_central_exp_length) -> (((exists pa_h_bl_pc_central_exp_length_lower_repeat_decoded. pa_h_bl_pc_central_exp_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_central_exp_length_lower_repeat)) * pa_c_bl_pc_central_exp_length_lower)) /\ exists pa_q_bl_pc_central_exp_length_lower_repeat_decoded. pa_b_bl_pc_central_exp_length_lower = pa_q_bl_pc_central_exp_length_lower_repeat_decoded * S ((S (pa_i_bl_pc_central_exp_length_lower_repeat)) * pa_c_bl_pc_central_exp_length_lower) + (2)))) /\ (exists pa_u_bl_pc_central_exp_length_lower_product pa_v_bl_pc_central_exp_length_lower_product. ((((exists pa_h_bl_pc_central_exp_length_lower_product_start. pa_h_bl_pc_central_exp_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_central_exp_length_lower_product)) /\ exists pa_q_bl_pc_central_exp_length_lower_product_start. pa_u_bl_pc_central_exp_length_lower_product = pa_q_bl_pc_central_exp_length_lower_product_start * S ((S (0)) * pa_v_bl_pc_central_exp_length_lower_product) + (1))) /\ ((((exists pa_h_bl_pc_central_exp_length_lower_product_terminal. pa_h_bl_pc_central_exp_length_lower_product_terminal + S (ff_lower_bl_pc_central_exp_length) = S ((S (ff_exponent_bl_pc_central_exp_length)) * pa_v_bl_pc_central_exp_length_lower_product)) /\ exists pa_q_bl_pc_central_exp_length_lower_product_terminal. pa_u_bl_pc_central_exp_length_lower_product = pa_q_bl_pc_central_exp_length_lower_product_terminal * S ((S (ff_exponent_bl_pc_central_exp_length)) * pa_v_bl_pc_central_exp_length_lower_product) + (ff_lower_bl_pc_central_exp_length))) /\ forall pa_i_bl_pc_central_exp_length_lower_product. (exists pa_lt_bl_pc_central_exp_length_lower_product_bound. pa_lt_bl_pc_central_exp_length_lower_product_bound + S pa_i_bl_pc_central_exp_length_lower_product = ff_exponent_bl_pc_central_exp_length) -> exists pa_p_bl_pc_central_exp_length_lower_product pa_r_bl_pc_central_exp_length_lower_product pa_s_bl_pc_central_exp_length_lower_product. ((((exists pa_h_bl_pc_central_exp_length_lower_product_factor. pa_h_bl_pc_central_exp_length_lower_product_factor + S (pa_p_bl_pc_central_exp_length_lower_product) = S ((S (pa_i_bl_pc_central_exp_length_lower_product)) * pa_c_bl_pc_central_exp_length_lower)) /\ exists pa_q_bl_pc_central_exp_length_lower_product_factor. pa_b_bl_pc_central_exp_length_lower = pa_q_bl_pc_central_exp_length_lower_product_factor * S ((S (pa_i_bl_pc_central_exp_length_lower_product)) * pa_c_bl_pc_central_exp_length_lower) + (pa_p_bl_pc_central_exp_length_lower_product))) /\ ((((exists pa_h_bl_pc_central_exp_length_lower_product_partial. pa_h_bl_pc_central_exp_length_lower_product_partial + S (pa_r_bl_pc_central_exp_length_lower_product) = S ((S (pa_i_bl_pc_central_exp_length_lower_product)) * pa_v_bl_pc_central_exp_length_lower_product)) /\ exists pa_q_bl_pc_central_exp_length_lower_product_partial. pa_u_bl_pc_central_exp_length_lower_product = pa_q_bl_pc_central_exp_length_lower_product_partial * S ((S (pa_i_bl_pc_central_exp_length_lower_product)) * pa_v_bl_pc_central_exp_length_lower_product) + (pa_r_bl_pc_central_exp_length_lower_product))) /\ ((((exists pa_h_bl_pc_central_exp_length_lower_product_successor. pa_h_bl_pc_central_exp_length_lower_product_successor + S (pa_s_bl_pc_central_exp_length_lower_product) = S ((S (S pa_i_bl_pc_central_exp_length_lower_product)) * pa_v_bl_pc_central_exp_length_lower_product)) /\ exists pa_q_bl_pc_central_exp_length_lower_product_successor. pa_u_bl_pc_central_exp_length_lower_product = pa_q_bl_pc_central_exp_length_lower_product_successor * S ((S (S pa_i_bl_pc_central_exp_length_lower_product)) * pa_v_bl_pc_central_exp_length_lower_product) + (pa_s_bl_pc_central_exp_length_lower_product))) /\ pa_s_bl_pc_central_exp_length_lower_product = pa_r_bl_pc_central_exp_length_lower_product * pa_p_bl_pc_central_exp_length_lower_product)))))))) /\ ((exists pa_b_bl_pc_central_exp_length_upper pa_c_bl_pc_central_exp_length_upper. ((forall pa_i_bl_pc_central_exp_length_upper_repeat. (exists pa_lt_bl_pc_central_exp_length_upper_repeat_bound. pa_lt_bl_pc_central_exp_length_upper_repeat_bound + S pa_i_bl_pc_central_exp_length_upper_repeat = ell) -> (((exists pa_h_bl_pc_central_exp_length_upper_repeat_decoded. pa_h_bl_pc_central_exp_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_central_exp_length_upper_repeat)) * pa_c_bl_pc_central_exp_length_upper)) /\ exists pa_q_bl_pc_central_exp_length_upper_repeat_decoded. pa_b_bl_pc_central_exp_length_upper = pa_q_bl_pc_central_exp_length_upper_repeat_decoded * S ((S (pa_i_bl_pc_central_exp_length_upper_repeat)) * pa_c_bl_pc_central_exp_length_upper) + (2)))) /\ (exists pa_u_bl_pc_central_exp_length_upper_product pa_v_bl_pc_central_exp_length_upper_product. ((((exists pa_h_bl_pc_central_exp_length_upper_product_start. pa_h_bl_pc_central_exp_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_central_exp_length_upper_product)) /\ exists pa_q_bl_pc_central_exp_length_upper_product_start. pa_u_bl_pc_central_exp_length_upper_product = pa_q_bl_pc_central_exp_length_upper_product_start * S ((S (0)) * pa_v_bl_pc_central_exp_length_upper_product) + (1))) /\ ((((exists pa_h_bl_pc_central_exp_length_upper_product_terminal. pa_h_bl_pc_central_exp_length_upper_product_terminal + S (ff_upper_bl_pc_central_exp_length) = S ((S (ell)) * pa_v_bl_pc_central_exp_length_upper_product)) /\ exists pa_q_bl_pc_central_exp_length_upper_product_terminal. pa_u_bl_pc_central_exp_length_upper_product = pa_q_bl_pc_central_exp_length_upper_product_terminal * S ((S (ell)) * pa_v_bl_pc_central_exp_length_upper_product) + (ff_upper_bl_pc_central_exp_length))) /\ forall pa_i_bl_pc_central_exp_length_upper_product. (exists pa_lt_bl_pc_central_exp_length_upper_product_bound. pa_lt_bl_pc_central_exp_length_upper_product_bound + S pa_i_bl_pc_central_exp_length_upper_product = ell) -> exists pa_p_bl_pc_central_exp_length_upper_product pa_r_bl_pc_central_exp_length_upper_product pa_s_bl_pc_central_exp_length_upper_product. ((((exists pa_h_bl_pc_central_exp_length_upper_product_factor. pa_h_bl_pc_central_exp_length_upper_product_factor + S (pa_p_bl_pc_central_exp_length_upper_product) = S ((S (pa_i_bl_pc_central_exp_length_upper_product)) * pa_c_bl_pc_central_exp_length_upper)) /\ exists pa_q_bl_pc_central_exp_length_upper_product_factor. pa_b_bl_pc_central_exp_length_upper = pa_q_bl_pc_central_exp_length_upper_product_factor * S ((S (pa_i_bl_pc_central_exp_length_upper_product)) * pa_c_bl_pc_central_exp_length_upper) + (pa_p_bl_pc_central_exp_length_upper_product))) /\ ((((exists pa_h_bl_pc_central_exp_length_upper_product_partial. pa_h_bl_pc_central_exp_length_upper_product_partial + S (pa_r_bl_pc_central_exp_length_upper_product) = S ((S (pa_i_bl_pc_central_exp_length_upper_product)) * pa_v_bl_pc_central_exp_length_upper_product)) /\ exists pa_q_bl_pc_central_exp_length_upper_product_partial. pa_u_bl_pc_central_exp_length_upper_product = pa_q_bl_pc_central_exp_length_upper_product_partial * S ((S (pa_i_bl_pc_central_exp_length_upper_product)) * pa_v_bl_pc_central_exp_length_upper_product) + (pa_r_bl_pc_central_exp_length_upper_product))) /\ ((((exists pa_h_bl_pc_central_exp_length_upper_product_successor. pa_h_bl_pc_central_exp_length_upper_product_successor + S (pa_s_bl_pc_central_exp_length_upper_product) = S ((S (S pa_i_bl_pc_central_exp_length_upper_product)) * pa_v_bl_pc_central_exp_length_upper_product)) /\ exists pa_q_bl_pc_central_exp_length_upper_product_successor. pa_u_bl_pc_central_exp_length_upper_product = pa_q_bl_pc_central_exp_length_upper_product_successor * S ((S (S pa_i_bl_pc_central_exp_length_upper_product)) * pa_v_bl_pc_central_exp_length_upper_product) + (pa_s_bl_pc_central_exp_length_upper_product))) /\ pa_s_bl_pc_central_exp_length_upper_product = pa_r_bl_pc_central_exp_length_upper_product * pa_p_bl_pc_central_exp_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_pc_central_exp_length. ff_lower_gap_bl_pc_central_exp_length + (ff_lower_bl_pc_central_exp_length) = (N)) /\ (exists ff_upper_gap_bl_pc_central_exp_length. ff_upper_gap_bl_pc_central_exp_length + S (N) = (ff_upper_bl_pc_central_exp_length))))))))) -> (exists pc_code_central_exp_count pc_scale_central_exp_count. (forall pc_index_central_exp_count_mask. (exists pc_lt_central_exp_count_mask_bound. pc_lt_central_exp_count_mask_bound + S (pc_index_central_exp_count_mask) = (N)) -> exists pc_bit_central_exp_count_mask. (((exists fs_h_pc_central_exp_count_mask_entry. fs_h_pc_central_exp_count_mask_entry + S (pc_bit_central_exp_count_mask) = S ((S (pc_index_central_exp_count_mask)) * pc_scale_central_exp_count)) /\ exists fs_q_pc_central_exp_count_mask_entry. pc_code_central_exp_count = fs_q_pc_central_exp_count_mask_entry * S ((S (pc_index_central_exp_count_mask)) * pc_scale_central_exp_count) + (pc_bit_central_exp_count_mask))) /\ (((((~(S (pc_index_central_exp_count_mask) = 1) /\ forall bpr_left_pc_central_exp_count_mask_choice_prime bpr_right_pc_central_exp_count_mask_choice_prime. S (pc_index_central_exp_count_mask) = bpr_left_pc_central_exp_count_mask_choice_prime * bpr_right_pc_central_exp_count_mask_choice_prime -> bpr_left_pc_central_exp_count_mask_choice_prime = 1 \/ bpr_right_pc_central_exp_count_mask_choice_prime = 1)) /\ pc_bit_central_exp_count_mask = 1) \/ (~((~(S (pc_index_central_exp_count_mask) = 1) /\ forall bpr_left_pc_central_exp_count_mask_choice_prime bpr_right_pc_central_exp_count_mask_choice_prime. S (pc_index_central_exp_count_mask) = bpr_left_pc_central_exp_count_mask_choice_prime * bpr_right_pc_central_exp_count_mask_choice_prime -> bpr_left_pc_central_exp_count_mask_choice_prime = 1 \/ bpr_right_pc_central_exp_count_mask_choice_prime = 1)) /\ pc_bit_central_exp_count_mask = 0)))) /\ (exists fs_u_pc_central_exp_count_sum fs_v_pc_central_exp_count_sum. ((((exists fs_h_pc_central_exp_count_sum_body_start. fs_h_pc_central_exp_count_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_central_exp_count_sum)) /\ exists fs_q_pc_central_exp_count_sum_body_start. fs_u_pc_central_exp_count_sum = fs_q_pc_central_exp_count_sum_body_start * S ((S (0)) * fs_v_pc_central_exp_count_sum) + (0))) /\ ((((exists fs_h_pc_central_exp_count_sum_body_terminal. fs_h_pc_central_exp_count_sum_body_terminal + S (k) = S ((S (N)) * fs_v_pc_central_exp_count_sum)) /\ exists fs_q_pc_central_exp_count_sum_body_terminal. fs_u_pc_central_exp_count_sum = fs_q_pc_central_exp_count_sum_body_terminal * S ((S (N)) * fs_v_pc_central_exp_count_sum) + (k))) /\ forall fs_i_pc_central_exp_count_sum_body_steps. (exists fs_lt_pc_central_exp_count_sum_body_steps_bound. fs_lt_pc_central_exp_count_sum_body_steps_bound + S fs_i_pc_central_exp_count_sum_body_steps = N) -> exists fs_a_pc_central_exp_count_sum_body_steps fs_r_pc_central_exp_count_sum_body_steps fs_s_pc_central_exp_count_sum_body_steps. ((((exists fs_h_pc_central_exp_count_sum_body_steps_summand. fs_h_pc_central_exp_count_sum_body_steps_summand + S (fs_a_pc_central_exp_count_sum_body_steps) = S ((S (fs_i_pc_central_exp_count_sum_body_steps)) * pc_scale_central_exp_count)) /\ exists fs_q_pc_central_exp_count_sum_body_steps_summand. pc_code_central_exp_count = fs_q_pc_central_exp_count_sum_body_steps_summand * S ((S (fs_i_pc_central_exp_count_sum_body_steps)) * pc_scale_central_exp_count) + (fs_a_pc_central_exp_count_sum_body_steps))) /\ ((((exists fs_h_pc_central_exp_count_sum_body_steps_partial. fs_h_pc_central_exp_count_sum_body_steps_partial + S (fs_r_pc_central_exp_count_sum_body_steps) = S ((S (fs_i_pc_central_exp_count_sum_body_steps)) * fs_v_pc_central_exp_count_sum)) /\ exists fs_q_pc_central_exp_count_sum_body_steps_partial. fs_u_pc_central_exp_count_sum = fs_q_pc_central_exp_count_sum_body_steps_partial * S ((S (fs_i_pc_central_exp_count_sum_body_steps)) * fs_v_pc_central_exp_count_sum) + (fs_r_pc_central_exp_count_sum_body_steps))) /\ ((((exists fs_h_pc_central_exp_count_sum_body_steps_successor. fs_h_pc_central_exp_count_sum_body_steps_successor + S (fs_s_pc_central_exp_count_sum_body_steps) = S ((S (S fs_i_pc_central_exp_count_sum_body_steps)) * fs_v_pc_central_exp_count_sum)) /\ exists fs_q_pc_central_exp_count_sum_body_steps_successor. fs_u_pc_central_exp_count_sum = fs_q_pc_central_exp_count_sum_body_steps_successor * S ((S (S fs_i_pc_central_exp_count_sum_body_steps)) * fs_v_pc_central_exp_count_sum) + (fs_s_pc_central_exp_count_sum_body_steps))) /\ fs_s_pc_central_exp_count_sum_body_steps = fs_r_pc_central_exp_count_sum_body_steps + fs_a_pc_central_exp_count_sum_body_steps))))))) -> (exists pc_le_central_exp_result. pc_le_central_exp_result + (h) = (ell * k))

Complete tactic proof in conservative notation

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

117 script commands · 27 reading checkpoints · 11 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 (3)

central binom prime count power bound central binom dominates pow two binary power two order reflects exponent

01Fix variables and assumptionsL1–8

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

L1
intro N
L2
intro ell
L3
intro k
L4
intro h
L5
intro hh
L6
intro hN
L7
intro hl
L8
intro hk

02Establish hCL9–11

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

L9
have hC : ∃ C. CentralBinom(h,C)Definitions: CentralBinom(h,C)Original native command in the exact edition
L10
specialize central_binom_exists h
L11
apply central_binom_exists

03Separate the logical casesL12–12