PC001D

central_binom_prime_mask_weighted_upper

The actual central-binomial contribution product is bounded factorwise by 2n exactly at prime-mask positions.

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. ∀ C. ∀ b. ∀ c. ∀ d. ∀ f. ∀ l. Lt(0,n) → CentralBinom(n,C) → (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ (Prime(S x) ∧ (∃ z. Le(z,C) ∧ (∃ m. Pow(S x,z,m) ∧ (∃ k. C = m · k)) ∧ (∀ m. Le(m,C) → (∃ k. Pow(S x,m,k) ∧ (∃ i. C = k · i)) → Le(m,z)) ∧ Pow(S x,z,y)) ∨ ¬Prime(S x) ∧ y = 1)) → PrimeBitPrefix(d,f,l) → ∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,f,x,z) → z = 0 ∧ y = 1 ∨ z = 1 ∧ Le(y,n + n)

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

Definition DAG

PrimeBitPrefix(b,c,l) · 1Le(a,b) · 7Lt(a,b) · 3Prime(p) · 6BetaAt(b,c,i,x) · 3Pow(a,e,z) · 6CentralBinom(n,z) · 1

Actual proof prerequisites

prime_bit_prefix_entryprime_contribution_prefix_decoded_choicecentral_binom_prime_power_contribution_le_double · checked external prerequisite
Original expanded first-order statement 
forall n C b c d f l. (exists pc_le_central_weight_positive. pc_le_central_weight_positive + (1) = (n)) -> (((exists bcf_lt_gap_pc_central_weight_value_out_of_range. bcf_lt_gap_pc_central_weight_value_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_pc_central_weight_value_in_range. bcf_le_gap_pc_central_weight_value_in_range + (n) = n + n) /\ (exists bcf_row_code_code_pc_central_weight_value bcf_row_code_scale_pc_central_weight_value bcf_row_scale_code_pc_central_weight_value bcf_row_scale_scale_pc_central_weight_value bcf_row_code_pc_central_weight_value bcf_row_scale_pc_central_weight_value. ((forall bcf_row_index_pc_central_weight_value_table. (exists bcf_lt_gap_pc_central_weight_value_table_row_bound. bcf_lt_gap_pc_central_weight_value_table_row_bound + S (bcf_row_index_pc_central_weight_value_table) = S (n + n)) -> exists bcf_row_code_pc_central_weight_value_table bcf_row_scale_pc_central_weight_value_table. ((((exists bcf_height_pc_central_weight_value_table_decoded_row_code. bcf_height_pc_central_weight_value_table_decoded_row_code + S (bcf_row_code_pc_central_weight_value_table) = S ((S (bcf_row_index_pc_central_weight_value_table)) * bcf_row_code_scale_pc_central_weight_value)) /\ exists bcf_quotient_pc_central_weight_value_table_decoded_row_code. bcf_row_code_code_pc_central_weight_value = bcf_quotient_pc_central_weight_value_table_decoded_row_code * S ((S (bcf_row_index_pc_central_weight_value_table)) * bcf_row_code_scale_pc_central_weight_value) + (bcf_row_code_pc_central_weight_value_table))) /\ ((((exists bcf_height_pc_central_weight_value_table_decoded_row_scale. bcf_height_pc_central_weight_value_table_decoded_row_scale + S (bcf_row_scale_pc_central_weight_value_table) = S ((S (bcf_row_index_pc_central_weight_value_table)) * bcf_row_scale_scale_pc_central_weight_value)) /\ exists bcf_quotient_pc_central_weight_value_table_decoded_row_scale. bcf_row_scale_code_pc_central_weight_value = bcf_quotient_pc_central_weight_value_table_decoded_row_scale * S ((S (bcf_row_index_pc_central_weight_value_table)) * bcf_row_scale_scale_pc_central_weight_value) + (bcf_row_scale_pc_central_weight_value_table))) /\ ((bcf_row_index_pc_central_weight_value_table = 0 /\ (forall bcf_index_pc_central_weight_value_table_zero_row. (exists bcf_lt_gap_pc_central_weight_value_table_zero_row_bound. bcf_lt_gap_pc_central_weight_value_table_zero_row_bound + S (bcf_index_pc_central_weight_value_table_zero_row) = S (n + n)) -> exists bcf_value_pc_central_weight_value_table_zero_row. ((((exists bcf_height_pc_central_weight_value_table_zero_row_entry. bcf_height_pc_central_weight_value_table_zero_row_entry + S (bcf_value_pc_central_weight_value_table_zero_row) = S ((S (bcf_index_pc_central_weight_value_table_zero_row)) * bcf_row_scale_pc_central_weight_value_table)) /\ exists bcf_quotient_pc_central_weight_value_table_zero_row_entry. bcf_row_code_pc_central_weight_value_table = bcf_quotient_pc_central_weight_value_table_zero_row_entry * S ((S (bcf_index_pc_central_weight_value_table_zero_row)) * bcf_row_scale_pc_central_weight_value_table) + (bcf_value_pc_central_weight_value_table_zero_row))) /\ ((bcf_index_pc_central_weight_value_table_zero_row = 0 /\ bcf_value_pc_central_weight_value_table_zero_row = 1) \/ exists bcf_predecessor_pc_central_weight_value_table_zero_row. bcf_index_pc_central_weight_value_table_zero_row = S bcf_predecessor_pc_central_weight_value_table_zero_row /\ bcf_value_pc_central_weight_value_table_zero_row = 0)))) \/ exists bcf_predecessor_pc_central_weight_value_table bcf_previous_code_pc_central_weight_value_table bcf_previous_scale_pc_central_weight_value_table. bcf_row_index_pc_central_weight_value_table = S bcf_predecessor_pc_central_weight_value_table /\ ((((exists bcf_height_pc_central_weight_value_table_decoded_previous_code. bcf_height_pc_central_weight_value_table_decoded_previous_code + S (bcf_previous_code_pc_central_weight_value_table) = S ((S (bcf_predecessor_pc_central_weight_value_table)) * bcf_row_code_scale_pc_central_weight_value)) /\ exists bcf_quotient_pc_central_weight_value_table_decoded_previous_code. bcf_row_code_code_pc_central_weight_value = bcf_quotient_pc_central_weight_value_table_decoded_previous_code * S ((S (bcf_predecessor_pc_central_weight_value_table)) * bcf_row_code_scale_pc_central_weight_value) + (bcf_previous_code_pc_central_weight_value_table))) /\ ((((exists bcf_height_pc_central_weight_value_table_decoded_previous_scale. bcf_height_pc_central_weight_value_table_decoded_previous_scale + S (bcf_previous_scale_pc_central_weight_value_table) = S ((S (bcf_predecessor_pc_central_weight_value_table)) * bcf_row_scale_scale_pc_central_weight_value)) /\ exists bcf_quotient_pc_central_weight_value_table_decoded_previous_scale. bcf_row_scale_code_pc_central_weight_value = bcf_quotient_pc_central_weight_value_table_decoded_previous_scale * S ((S (bcf_predecessor_pc_central_weight_value_table)) * bcf_row_scale_scale_pc_central_weight_value) + (bcf_previous_scale_pc_central_weight_value_table))) /\ (forall bcf_index_pc_central_weight_value_table_row_step. (exists bcf_lt_gap_pc_central_weight_value_table_row_step_bound. bcf_lt_gap_pc_central_weight_value_table_row_step_bound + S (bcf_index_pc_central_weight_value_table_row_step) = S (n + n)) -> exists bcf_value_pc_central_weight_value_table_row_step. ((((exists bcf_height_pc_central_weight_value_table_row_step_entry. bcf_height_pc_central_weight_value_table_row_step_entry + S (bcf_value_pc_central_weight_value_table_row_step) = S ((S (bcf_index_pc_central_weight_value_table_row_step)) * bcf_row_scale_pc_central_weight_value_table)) /\ exists bcf_quotient_pc_central_weight_value_table_row_step_entry. bcf_row_code_pc_central_weight_value_table = bcf_quotient_pc_central_weight_value_table_row_step_entry * S ((S (bcf_index_pc_central_weight_value_table_row_step)) * bcf_row_scale_pc_central_weight_value_table) + (bcf_value_pc_central_weight_value_table_row_step))) /\ ((bcf_index_pc_central_weight_value_table_row_step = 0 /\ bcf_value_pc_central_weight_value_table_row_step = 1) \/ exists bcf_predecessor_pc_central_weight_value_table_row_step bcf_left_pc_central_weight_value_table_row_step bcf_right_pc_central_weight_value_table_row_step. bcf_index_pc_central_weight_value_table_row_step = S bcf_predecessor_pc_central_weight_value_table_row_step /\ ((((exists bcf_height_pc_central_weight_value_table_row_step_previous_left. bcf_height_pc_central_weight_value_table_row_step_previous_left + S (bcf_left_pc_central_weight_value_table_row_step) = S ((S (bcf_predecessor_pc_central_weight_value_table_row_step)) * bcf_previous_scale_pc_central_weight_value_table)) /\ exists bcf_quotient_pc_central_weight_value_table_row_step_previous_left. bcf_previous_code_pc_central_weight_value_table = bcf_quotient_pc_central_weight_value_table_row_step_previous_left * S ((S (bcf_predecessor_pc_central_weight_value_table_row_step)) * bcf_previous_scale_pc_central_weight_value_table) + (bcf_left_pc_central_weight_value_table_row_step))) /\ ((((exists bcf_height_pc_central_weight_value_table_row_step_previous_right. bcf_height_pc_central_weight_value_table_row_step_previous_right + S (bcf_right_pc_central_weight_value_table_row_step) = S ((S (S (bcf_predecessor_pc_central_weight_value_table_row_step))) * bcf_previous_scale_pc_central_weight_value_table)) /\ exists bcf_quotient_pc_central_weight_value_table_row_step_previous_right. bcf_previous_code_pc_central_weight_value_table = bcf_quotient_pc_central_weight_value_table_row_step_previous_right * S ((S (S (bcf_predecessor_pc_central_weight_value_table_row_step))) * bcf_previous_scale_pc_central_weight_value_table) + (bcf_right_pc_central_weight_value_table_row_step))) /\ bcf_value_pc_central_weight_value_table_row_step = bcf_left_pc_central_weight_value_table_row_step + bcf_right_pc_central_weight_value_table_row_step))))))))))) /\ ((((exists bcf_height_pc_central_weight_value_decoded_row_code. bcf_height_pc_central_weight_value_decoded_row_code + S (bcf_row_code_pc_central_weight_value) = S ((S (n + n)) * bcf_row_code_scale_pc_central_weight_value)) /\ exists bcf_quotient_pc_central_weight_value_decoded_row_code. bcf_row_code_code_pc_central_weight_value = bcf_quotient_pc_central_weight_value_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_pc_central_weight_value) + (bcf_row_code_pc_central_weight_value))) /\ ((((exists bcf_height_pc_central_weight_value_decoded_row_scale. bcf_height_pc_central_weight_value_decoded_row_scale + S (bcf_row_scale_pc_central_weight_value) = S ((S (n + n)) * bcf_row_scale_scale_pc_central_weight_value)) /\ exists bcf_quotient_pc_central_weight_value_decoded_row_scale. bcf_row_scale_code_pc_central_weight_value = bcf_quotient_pc_central_weight_value_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_pc_central_weight_value) + (bcf_row_scale_pc_central_weight_value))) /\ (((exists bcf_height_pc_central_weight_value_decoded_value. bcf_height_pc_central_weight_value_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_pc_central_weight_value)) /\ exists bcf_quotient_pc_central_weight_value_decoded_value. bcf_row_code_pc_central_weight_value = bcf_quotient_pc_central_weight_value_decoded_value * S ((S (n)) * bcf_row_scale_pc_central_weight_value) + (C))))))))) -> (forall bpr_prefix_index_pc_central_weight_factors. (exists bpr_gap_pc_central_weight_factors_bound. bpr_gap_pc_central_weight_factors_bound + S (bpr_prefix_index_pc_central_weight_factors) = l) -> exists bpr_prefix_value_pc_central_weight_factors. ((((exists bpr_height_pc_central_weight_factors_decoded. bpr_height_pc_central_weight_factors_decoded + S (bpr_prefix_value_pc_central_weight_factors) = S ((S (bpr_prefix_index_pc_central_weight_factors)) * c)) /\ exists bpr_quotient_pc_central_weight_factors_decoded. b = bpr_quotient_pc_central_weight_factors_decoded * S ((S (bpr_prefix_index_pc_central_weight_factors)) * c) + (bpr_prefix_value_pc_central_weight_factors))) /\ (((((~(S (bpr_prefix_index_pc_central_weight_factors) = 1) /\ forall bpr_left_pc_central_weight_factors_choice_prime bpr_right_pc_central_weight_factors_choice_prime. S (bpr_prefix_index_pc_central_weight_factors) = bpr_left_pc_central_weight_factors_choice_prime * bpr_right_pc_central_weight_factors_choice_prime -> bpr_left_pc_central_weight_factors_choice_prime = 1 \/ bpr_right_pc_central_weight_factors_choice_prime = 1)) /\ exists bpr_choice_exponent_pc_central_weight_factors_choice. ((((exists bpr_le_gap_pc_central_weight_factors_choice_valuation_selected_bound. bpr_le_gap_pc_central_weight_factors_choice_valuation_selected_bound + (bpr_choice_exponent_pc_central_weight_factors_choice) = (C)) /\ (exists bpr_power_value_pc_central_weight_factors_choice_valuation_selected. ((exists bpr_power_code_pc_central_weight_factors_choice_valuation_selected_power bpr_power_scale_pc_central_weight_factors_choice_valuation_selected_power. ((forall bpr_power_index_pc_central_weight_factors_choice_valuation_selected_power. (exists bpr_gap_pc_central_weight_factors_choice_valuation_selected_power_repeat_bound. bpr_gap_pc_central_weight_factors_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_pc_central_weight_factors_choice_valuation_selected_power) = bpr_choice_exponent_pc_central_weight_factors_choice) -> (((exists bpr_height_pc_central_weight_factors_choice_valuation_selected_power_repeat_entry. bpr_height_pc_central_weight_factors_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_pc_central_weight_factors)) = S ((S (bpr_power_index_pc_central_weight_factors_choice_valuation_selected_power)) * bpr_power_scale_pc_central_weight_factors_choice_valuation_selected_power)) /\ exists bpr_quotient_pc_central_weight_factors_choice_valuation_selected_power_repeat_entry. bpr_power_code_pc_central_weight_factors_choice_valuation_selected_power = bpr_quotient_pc_central_weight_factors_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_pc_central_weight_factors_choice_valuation_selected_power)) * bpr_power_scale_pc_central_weight_factors_choice_valuation_selected_power) + (S (bpr_prefix_index_pc_central_weight_factors))))) /\ (exists ff_u_pc_central_weight_factors_choice_valuation_selected_power_product ff_v_pc_central_weight_factors_choice_valuation_selected_power_product. ((((exists ff_h_pc_central_weight_factors_choice_valuation_selected_power_product_start. ff_h_pc_central_weight_factors_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_pc_central_weight_factors_choice_valuation_selected_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_valuation_selected_power_product_start. ff_u_pc_central_weight_factors_choice_valuation_selected_power_product = ff_q_pc_central_weight_factors_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_pc_central_weight_factors_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_pc_central_weight_factors_choice_valuation_selected_power_product_terminal. ff_h_pc_central_weight_factors_choice_valuation_selected_power_product_terminal + S (bpr_power_value_pc_central_weight_factors_choice_valuation_selected) = S ((S (bpr_choice_exponent_pc_central_weight_factors_choice)) * ff_v_pc_central_weight_factors_choice_valuation_selected_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_valuation_selected_power_product_terminal. ff_u_pc_central_weight_factors_choice_valuation_selected_power_product = ff_q_pc_central_weight_factors_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_pc_central_weight_factors_choice)) * ff_v_pc_central_weight_factors_choice_valuation_selected_power_product) + (bpr_power_value_pc_central_weight_factors_choice_valuation_selected))) /\ forall ff_i_pc_central_weight_factors_choice_valuation_selected_power_product. (exists ff_lt_pc_central_weight_factors_choice_valuation_selected_power_product_bound. ff_lt_pc_central_weight_factors_choice_valuation_selected_power_product_bound + S ff_i_pc_central_weight_factors_choice_valuation_selected_power_product = bpr_choice_exponent_pc_central_weight_factors_choice) -> exists ff_p_pc_central_weight_factors_choice_valuation_selected_power_product ff_r_pc_central_weight_factors_choice_valuation_selected_power_product ff_s_pc_central_weight_factors_choice_valuation_selected_power_product. ((((exists ff_h_pc_central_weight_factors_choice_valuation_selected_power_product_factor. ff_h_pc_central_weight_factors_choice_valuation_selected_power_product_factor + S (ff_p_pc_central_weight_factors_choice_valuation_selected_power_product) = S ((S (ff_i_pc_central_weight_factors_choice_valuation_selected_power_product)) * bpr_power_scale_pc_central_weight_factors_choice_valuation_selected_power)) /\ exists ff_q_pc_central_weight_factors_choice_valuation_selected_power_product_factor. bpr_power_code_pc_central_weight_factors_choice_valuation_selected_power = ff_q_pc_central_weight_factors_choice_valuation_selected_power_product_factor * S ((S (ff_i_pc_central_weight_factors_choice_valuation_selected_power_product)) * bpr_power_scale_pc_central_weight_factors_choice_valuation_selected_power) + (ff_p_pc_central_weight_factors_choice_valuation_selected_power_product))) /\ ((((exists ff_h_pc_central_weight_factors_choice_valuation_selected_power_product_partial. ff_h_pc_central_weight_factors_choice_valuation_selected_power_product_partial + S (ff_r_pc_central_weight_factors_choice_valuation_selected_power_product) = S ((S (ff_i_pc_central_weight_factors_choice_valuation_selected_power_product)) * ff_v_pc_central_weight_factors_choice_valuation_selected_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_valuation_selected_power_product_partial. ff_u_pc_central_weight_factors_choice_valuation_selected_power_product = ff_q_pc_central_weight_factors_choice_valuation_selected_power_product_partial * S ((S (ff_i_pc_central_weight_factors_choice_valuation_selected_power_product)) * ff_v_pc_central_weight_factors_choice_valuation_selected_power_product) + (ff_r_pc_central_weight_factors_choice_valuation_selected_power_product))) /\ ((((exists ff_h_pc_central_weight_factors_choice_valuation_selected_power_product_successor. ff_h_pc_central_weight_factors_choice_valuation_selected_power_product_successor + S (ff_s_pc_central_weight_factors_choice_valuation_selected_power_product) = S ((S (S ff_i_pc_central_weight_factors_choice_valuation_selected_power_product)) * ff_v_pc_central_weight_factors_choice_valuation_selected_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_valuation_selected_power_product_successor. ff_u_pc_central_weight_factors_choice_valuation_selected_power_product = ff_q_pc_central_weight_factors_choice_valuation_selected_power_product_successor * S ((S (S ff_i_pc_central_weight_factors_choice_valuation_selected_power_product)) * ff_v_pc_central_weight_factors_choice_valuation_selected_power_product) + (ff_s_pc_central_weight_factors_choice_valuation_selected_power_product))) /\ ff_s_pc_central_weight_factors_choice_valuation_selected_power_product = ff_r_pc_central_weight_factors_choice_valuation_selected_power_product * ff_p_pc_central_weight_factors_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_pc_central_weight_factors_choice_valuation_selected_divides. C = (bpr_power_value_pc_central_weight_factors_choice_valuation_selected) * bpr_divides_quotient_pc_central_weight_factors_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_pc_central_weight_factors_choice_valuation. (exists bpr_le_gap_pc_central_weight_factors_choice_valuation_candidate_bound. bpr_le_gap_pc_central_weight_factors_choice_valuation_candidate_bound + (bpr_valuation_candidate_pc_central_weight_factors_choice_valuation) = (C)) -> (exists bpr_power_value_pc_central_weight_factors_choice_valuation_candidate. ((exists bpr_power_code_pc_central_weight_factors_choice_valuation_candidate_power bpr_power_scale_pc_central_weight_factors_choice_valuation_candidate_power. ((forall bpr_power_index_pc_central_weight_factors_choice_valuation_candidate_power. (exists bpr_gap_pc_central_weight_factors_choice_valuation_candidate_power_repeat_bound. bpr_gap_pc_central_weight_factors_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_pc_central_weight_factors_choice_valuation_candidate_power) = bpr_valuation_candidate_pc_central_weight_factors_choice_valuation) -> (((exists bpr_height_pc_central_weight_factors_choice_valuation_candidate_power_repeat_entry. bpr_height_pc_central_weight_factors_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_pc_central_weight_factors)) = S ((S (bpr_power_index_pc_central_weight_factors_choice_valuation_candidate_power)) * bpr_power_scale_pc_central_weight_factors_choice_valuation_candidate_power)) /\ exists bpr_quotient_pc_central_weight_factors_choice_valuation_candidate_power_repeat_entry. bpr_power_code_pc_central_weight_factors_choice_valuation_candidate_power = bpr_quotient_pc_central_weight_factors_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_pc_central_weight_factors_choice_valuation_candidate_power)) * bpr_power_scale_pc_central_weight_factors_choice_valuation_candidate_power) + (S (bpr_prefix_index_pc_central_weight_factors))))) /\ (exists ff_u_pc_central_weight_factors_choice_valuation_candidate_power_product ff_v_pc_central_weight_factors_choice_valuation_candidate_power_product. ((((exists ff_h_pc_central_weight_factors_choice_valuation_candidate_power_product_start. ff_h_pc_central_weight_factors_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_pc_central_weight_factors_choice_valuation_candidate_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_valuation_candidate_power_product_start. ff_u_pc_central_weight_factors_choice_valuation_candidate_power_product = ff_q_pc_central_weight_factors_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_pc_central_weight_factors_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_pc_central_weight_factors_choice_valuation_candidate_power_product_terminal. ff_h_pc_central_weight_factors_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_pc_central_weight_factors_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_pc_central_weight_factors_choice_valuation)) * ff_v_pc_central_weight_factors_choice_valuation_candidate_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_valuation_candidate_power_product_terminal. ff_u_pc_central_weight_factors_choice_valuation_candidate_power_product = ff_q_pc_central_weight_factors_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_pc_central_weight_factors_choice_valuation)) * ff_v_pc_central_weight_factors_choice_valuation_candidate_power_product) + (bpr_power_value_pc_central_weight_factors_choice_valuation_candidate))) /\ forall ff_i_pc_central_weight_factors_choice_valuation_candidate_power_product. (exists ff_lt_pc_central_weight_factors_choice_valuation_candidate_power_product_bound. ff_lt_pc_central_weight_factors_choice_valuation_candidate_power_product_bound + S ff_i_pc_central_weight_factors_choice_valuation_candidate_power_product = bpr_valuation_candidate_pc_central_weight_factors_choice_valuation) -> exists ff_p_pc_central_weight_factors_choice_valuation_candidate_power_product ff_r_pc_central_weight_factors_choice_valuation_candidate_power_product ff_s_pc_central_weight_factors_choice_valuation_candidate_power_product. ((((exists ff_h_pc_central_weight_factors_choice_valuation_candidate_power_product_factor. ff_h_pc_central_weight_factors_choice_valuation_candidate_power_product_factor + S (ff_p_pc_central_weight_factors_choice_valuation_candidate_power_product) = S ((S (ff_i_pc_central_weight_factors_choice_valuation_candidate_power_product)) * bpr_power_scale_pc_central_weight_factors_choice_valuation_candidate_power)) /\ exists ff_q_pc_central_weight_factors_choice_valuation_candidate_power_product_factor. bpr_power_code_pc_central_weight_factors_choice_valuation_candidate_power = ff_q_pc_central_weight_factors_choice_valuation_candidate_power_product_factor * S ((S (ff_i_pc_central_weight_factors_choice_valuation_candidate_power_product)) * bpr_power_scale_pc_central_weight_factors_choice_valuation_candidate_power) + (ff_p_pc_central_weight_factors_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_pc_central_weight_factors_choice_valuation_candidate_power_product_partial. ff_h_pc_central_weight_factors_choice_valuation_candidate_power_product_partial + S (ff_r_pc_central_weight_factors_choice_valuation_candidate_power_product) = S ((S (ff_i_pc_central_weight_factors_choice_valuation_candidate_power_product)) * ff_v_pc_central_weight_factors_choice_valuation_candidate_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_valuation_candidate_power_product_partial. ff_u_pc_central_weight_factors_choice_valuation_candidate_power_product = ff_q_pc_central_weight_factors_choice_valuation_candidate_power_product_partial * S ((S (ff_i_pc_central_weight_factors_choice_valuation_candidate_power_product)) * ff_v_pc_central_weight_factors_choice_valuation_candidate_power_product) + (ff_r_pc_central_weight_factors_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_pc_central_weight_factors_choice_valuation_candidate_power_product_successor. ff_h_pc_central_weight_factors_choice_valuation_candidate_power_product_successor + S (ff_s_pc_central_weight_factors_choice_valuation_candidate_power_product) = S ((S (S ff_i_pc_central_weight_factors_choice_valuation_candidate_power_product)) * ff_v_pc_central_weight_factors_choice_valuation_candidate_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_valuation_candidate_power_product_successor. ff_u_pc_central_weight_factors_choice_valuation_candidate_power_product = ff_q_pc_central_weight_factors_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_pc_central_weight_factors_choice_valuation_candidate_power_product)) * ff_v_pc_central_weight_factors_choice_valuation_candidate_power_product) + (ff_s_pc_central_weight_factors_choice_valuation_candidate_power_product))) /\ ff_s_pc_central_weight_factors_choice_valuation_candidate_power_product = ff_r_pc_central_weight_factors_choice_valuation_candidate_power_product * ff_p_pc_central_weight_factors_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_pc_central_weight_factors_choice_valuation_candidate_divides. C = (bpr_power_value_pc_central_weight_factors_choice_valuation_candidate) * bpr_divides_quotient_pc_central_weight_factors_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_pc_central_weight_factors_choice_valuation_candidate_below. bpr_le_gap_pc_central_weight_factors_choice_valuation_candidate_below + (bpr_valuation_candidate_pc_central_weight_factors_choice_valuation) = (bpr_choice_exponent_pc_central_weight_factors_choice))) /\ (exists bpr_power_code_pc_central_weight_factors_choice_power bpr_power_scale_pc_central_weight_factors_choice_power. ((forall bpr_power_index_pc_central_weight_factors_choice_power. (exists bpr_gap_pc_central_weight_factors_choice_power_repeat_bound. bpr_gap_pc_central_weight_factors_choice_power_repeat_bound + S (bpr_power_index_pc_central_weight_factors_choice_power) = bpr_choice_exponent_pc_central_weight_factors_choice) -> (((exists bpr_height_pc_central_weight_factors_choice_power_repeat_entry. bpr_height_pc_central_weight_factors_choice_power_repeat_entry + S (S (bpr_prefix_index_pc_central_weight_factors)) = S ((S (bpr_power_index_pc_central_weight_factors_choice_power)) * bpr_power_scale_pc_central_weight_factors_choice_power)) /\ exists bpr_quotient_pc_central_weight_factors_choice_power_repeat_entry. bpr_power_code_pc_central_weight_factors_choice_power = bpr_quotient_pc_central_weight_factors_choice_power_repeat_entry * S ((S (bpr_power_index_pc_central_weight_factors_choice_power)) * bpr_power_scale_pc_central_weight_factors_choice_power) + (S (bpr_prefix_index_pc_central_weight_factors))))) /\ (exists ff_u_pc_central_weight_factors_choice_power_product ff_v_pc_central_weight_factors_choice_power_product. ((((exists ff_h_pc_central_weight_factors_choice_power_product_start. ff_h_pc_central_weight_factors_choice_power_product_start + S (1) = S ((S (0)) * ff_v_pc_central_weight_factors_choice_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_power_product_start. ff_u_pc_central_weight_factors_choice_power_product = ff_q_pc_central_weight_factors_choice_power_product_start * S ((S (0)) * ff_v_pc_central_weight_factors_choice_power_product) + (1))) /\ ((((exists ff_h_pc_central_weight_factors_choice_power_product_terminal. ff_h_pc_central_weight_factors_choice_power_product_terminal + S (bpr_prefix_value_pc_central_weight_factors) = S ((S (bpr_choice_exponent_pc_central_weight_factors_choice)) * ff_v_pc_central_weight_factors_choice_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_power_product_terminal. ff_u_pc_central_weight_factors_choice_power_product = ff_q_pc_central_weight_factors_choice_power_product_terminal * S ((S (bpr_choice_exponent_pc_central_weight_factors_choice)) * ff_v_pc_central_weight_factors_choice_power_product) + (bpr_prefix_value_pc_central_weight_factors))) /\ forall ff_i_pc_central_weight_factors_choice_power_product. (exists ff_lt_pc_central_weight_factors_choice_power_product_bound. ff_lt_pc_central_weight_factors_choice_power_product_bound + S ff_i_pc_central_weight_factors_choice_power_product = bpr_choice_exponent_pc_central_weight_factors_choice) -> exists ff_p_pc_central_weight_factors_choice_power_product ff_r_pc_central_weight_factors_choice_power_product ff_s_pc_central_weight_factors_choice_power_product. ((((exists ff_h_pc_central_weight_factors_choice_power_product_factor. ff_h_pc_central_weight_factors_choice_power_product_factor + S (ff_p_pc_central_weight_factors_choice_power_product) = S ((S (ff_i_pc_central_weight_factors_choice_power_product)) * bpr_power_scale_pc_central_weight_factors_choice_power)) /\ exists ff_q_pc_central_weight_factors_choice_power_product_factor. bpr_power_code_pc_central_weight_factors_choice_power = ff_q_pc_central_weight_factors_choice_power_product_factor * S ((S (ff_i_pc_central_weight_factors_choice_power_product)) * bpr_power_scale_pc_central_weight_factors_choice_power) + (ff_p_pc_central_weight_factors_choice_power_product))) /\ ((((exists ff_h_pc_central_weight_factors_choice_power_product_partial. ff_h_pc_central_weight_factors_choice_power_product_partial + S (ff_r_pc_central_weight_factors_choice_power_product) = S ((S (ff_i_pc_central_weight_factors_choice_power_product)) * ff_v_pc_central_weight_factors_choice_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_power_product_partial. ff_u_pc_central_weight_factors_choice_power_product = ff_q_pc_central_weight_factors_choice_power_product_partial * S ((S (ff_i_pc_central_weight_factors_choice_power_product)) * ff_v_pc_central_weight_factors_choice_power_product) + (ff_r_pc_central_weight_factors_choice_power_product))) /\ ((((exists ff_h_pc_central_weight_factors_choice_power_product_successor. ff_h_pc_central_weight_factors_choice_power_product_successor + S (ff_s_pc_central_weight_factors_choice_power_product) = S ((S (S ff_i_pc_central_weight_factors_choice_power_product)) * ff_v_pc_central_weight_factors_choice_power_product)) /\ exists ff_q_pc_central_weight_factors_choice_power_product_successor. ff_u_pc_central_weight_factors_choice_power_product = ff_q_pc_central_weight_factors_choice_power_product_successor * S ((S (S ff_i_pc_central_weight_factors_choice_power_product)) * ff_v_pc_central_weight_factors_choice_power_product) + (ff_s_pc_central_weight_factors_choice_power_product))) /\ ff_s_pc_central_weight_factors_choice_power_product = ff_r_pc_central_weight_factors_choice_power_product * ff_p_pc_central_weight_factors_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_pc_central_weight_factors) = 1) /\ forall bpr_left_pc_central_weight_factors_choice_prime bpr_right_pc_central_weight_factors_choice_prime. S (bpr_prefix_index_pc_central_weight_factors) = bpr_left_pc_central_weight_factors_choice_prime * bpr_right_pc_central_weight_factors_choice_prime -> bpr_left_pc_central_weight_factors_choice_prime = 1 \/ bpr_right_pc_central_weight_factors_choice_prime = 1)) /\ bpr_prefix_value_pc_central_weight_factors = 1))))) -> (forall pc_index_central_weight_mask. (exists pc_lt_central_weight_mask_bound. pc_lt_central_weight_mask_bound + S (pc_index_central_weight_mask) = (l)) -> exists pc_bit_central_weight_mask. (((exists fs_h_pc_central_weight_mask_entry. fs_h_pc_central_weight_mask_entry + S (pc_bit_central_weight_mask) = S ((S (pc_index_central_weight_mask)) * f)) /\ exists fs_q_pc_central_weight_mask_entry. d = fs_q_pc_central_weight_mask_entry * S ((S (pc_index_central_weight_mask)) * f) + (pc_bit_central_weight_mask))) /\ (((((~(S (pc_index_central_weight_mask) = 1) /\ forall bpr_left_pc_central_weight_mask_choice_prime bpr_right_pc_central_weight_mask_choice_prime. S (pc_index_central_weight_mask) = bpr_left_pc_central_weight_mask_choice_prime * bpr_right_pc_central_weight_mask_choice_prime -> bpr_left_pc_central_weight_mask_choice_prime = 1 \/ bpr_right_pc_central_weight_mask_choice_prime = 1)) /\ pc_bit_central_weight_mask = 1) \/ (~((~(S (pc_index_central_weight_mask) = 1) /\ forall bpr_left_pc_central_weight_mask_choice_prime bpr_right_pc_central_weight_mask_choice_prime. S (pc_index_central_weight_mask) = bpr_left_pc_central_weight_mask_choice_prime * bpr_right_pc_central_weight_mask_choice_prime -> bpr_left_pc_central_weight_mask_choice_prime = 1 \/ bpr_right_pc_central_weight_mask_choice_prime = 1)) /\ pc_bit_central_weight_mask = 0)))) -> (forall pc_index_central_weight_result pc_factor_central_weight_result pc_bit_central_weight_result. (exists pc_lt_central_weight_result_index. pc_lt_central_weight_result_index + S (pc_index_central_weight_result) = (l)) -> (((exists fs_h_pc_central_weight_result_factor. fs_h_pc_central_weight_result_factor + S (pc_factor_central_weight_result) = S ((S (pc_index_central_weight_result)) * c)) /\ exists fs_q_pc_central_weight_result_factor. b = fs_q_pc_central_weight_result_factor * S ((S (pc_index_central_weight_result)) * c) + (pc_factor_central_weight_result))) -> (((exists fs_h_pc_central_weight_result_bit. fs_h_pc_central_weight_result_bit + S (pc_bit_central_weight_result) = S ((S (pc_index_central_weight_result)) * f)) /\ exists fs_q_pc_central_weight_result_bit. d = fs_q_pc_central_weight_result_bit * S ((S (pc_index_central_weight_result)) * f) + (pc_bit_central_weight_result))) -> ((pc_bit_central_weight_result = 0 /\ (pc_factor_central_weight_result = 1)) \/ (pc_bit_central_weight_result = 1 /\ (exists pc_le_central_weight_result_one. pc_le_central_weight_result_one + (pc_factor_central_weight_result) = (n + n)))))

Complete tactic proof in conservative notation

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

73 script commands · 14 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 (2)
prime bit prefix entryprime contribution prefix decoded choice
01Fix variables and assumptionsL1–10

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

  1. L1
    intro n
  2. L2
    intro C
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro f
  7. L7
    intro l
  8. L8
    intro hn
  9. L9
    intro hC
  10. L10
    intro hf
02Fix variables and assumptionsL11–17

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

  1. L11
    intro hm
  2. L12
    intro i
  3. L13
    intro a
  4. L14
    intro e
  5. L15
    intro hi
  6. L16
    intro ha
  7. L17
    intro he
03Establish hbL18–27

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

  1. L18
    have hb : Prime(S i) ∧ e = 1 ∨ ¬Prime(S i) ∧ e = 0Definitions: Prime(S i)Original native command in the exact edition
  2. L19
    specialize prime_bit_prefix_entry d
  3. L20
    specialize prime_bit_prefix_entry f
  4. L21
    specialize prime_bit_prefix_entry l
  5. L22
    specialize prime_bit_prefix_entry i
  6. L23
    specialize prime_bit_prefix_entry e
  7. L24
    apply prime_bit_prefix_entry
  8. L25
    exact hm
  9. L26
    exact hi
  10. L27
    exact he
04Establish hvL28–37

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

  1. L28
    have hv : Prime(S i) ∧ (∃ x. Le(x,C) ∧ (∃ y. Pow(S i,x,y) ∧ (∃ z. C = y · z)) ∧ (∀ y. Le(y,C) → (∃ z. Pow(S i,y,z) ∧ (∃ n. C = z · n)) → Le(y,x)) ∧ Pow(S i,x,a)) ∨ ¬Prime(S i) ∧ a = 1Definitions: Prime(S i)Le(x,C)Pow(S i,x,y)Le(y,C)Pow(S i,y,z)Le(y,x)Pow(S i,x,a)Original native command in the exact edition
  2. L29
    specialize prime_contribution_prefix_decoded_choice C
  3. L30
    specialize prime_contribution_prefix_decoded_choice b
  4. L31
    specialize prime_contribution_prefix_decoded_choice c
  5. L32
    specialize prime_contribution_prefix_decoded_choice l
  6. L33
    specialize prime_contribution_prefix_decoded_choice i
  7. L34
    specialize prime_contribution_prefix_decoded_choice a
  8. L35
    apply prime_contribution_prefix_decoded_choice
  9. L36
    exact hf
  10. L37
    exact hi
05Use earlier factsL38–38

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

  1. L38
    exact ha
06Separate the logical casesL39–46

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

  1. L39
    cases hb
  2. L40
    cases hb_left
  3. L41
    cases hv
  4. L42
    cases hv_left
  5. L43
    cases hv_left_right
  6. L44
    cases hv_left_right_witness
  7. L45
    right
  8. L46
    split
07Use earlier factsL47–56

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

  1. L47
    exact hb_left_right
  2. L48
    specialize central_binom_prime_power_contribution_le_double (S i)
  3. L49
    specialize central_binom_prime_power_contribution_le_double n
  4. L50
    specialize central_binom_prime_power_contribution_le_double C
  5. L51
    specialize central_binom_prime_power_contribution_le_double x
  6. L52
    specialize central_binom_prime_power_contribution_le_double a
  7. L53
    apply central_binom_prime_power_contribution_le_double
  8. L54
    exact hb_left_left
  9. L55
    exact hn
  10. L56
    exact hC
08Use earlier factsL57–58

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

  1. L57
    exact hv_left_right_witness_left
  2. L58
    exact hv_left_right_witness_right
09Separate the logical casesL59–60

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

  1. L59
    cases hv_right
  2. L60
    exfalso
10Use earlier factsL61–62

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

  1. L61
    apply hv_right_left
  2. L62
    exact hb_left_left
11Separate the logical casesL63–66

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

  1. L63
    cases hb_right
  2. L64
    cases hv
  3. L65
    cases hv_left
  4. L66
    exfalso
12Use earlier factsL67–68

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

  1. L67
    apply hb_right_left
  2. L68
    exact hv_left_left
13Separate the logical casesL69–71

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

  1. L69
    cases hv_right
  2. L70
    left
  3. L71
    split
14Use earlier factsL72–73

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

  1. L72
    exact hb_right_right
  2. L73
    exact hv_right_right

Library-wide reading audit

Original defined command ledger · 73 lines
  1. 0001intro n
  2. 0002intro C
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro f
  7. 0007intro l
  8. 0008intro hn
  9. 0009intro hC
  10. 0010intro hf
  11. 0011intro hm
  12. 0012intro i
  13. 0013intro a
  14. 0014intro e
  15. 0015intro hi
  16. 0016intro ha
  17. 0017intro he
  18. 0018have hb : Prime(S i) ∧ e = 1 ∨ ¬Prime(S i) ∧ e = 0
  19. 0019specialize prime_bit_prefix_entry d
  20. 0020specialize prime_bit_prefix_entry f
  21. 0021specialize prime_bit_prefix_entry l
  22. 0022specialize prime_bit_prefix_entry i
  23. 0023specialize prime_bit_prefix_entry e
  24. 0024apply prime_bit_prefix_entry
  25. 0025exact hm
  26. 0026exact hi
  27. 0027exact he
  28. 0028have hv : Prime(S i) ∧ (∃ x. Le(x,C) ∧ (∃ y. Pow(S i,x,y) ∧ (∃ z. C = y · z)) ∧ (∀ y. Le(y,C) → (∃ z. Pow(S i,y,z) ∧ (∃ n. C = z · n)) → Le(y,x)) ∧ Pow(S i,x,a)) ∨ ¬Prime(S i) ∧ a = 1
  29. 0029specialize prime_contribution_prefix_decoded_choice C
  30. 0030specialize prime_contribution_prefix_decoded_choice b
  31. 0031specialize prime_contribution_prefix_decoded_choice c
  32. 0032specialize prime_contribution_prefix_decoded_choice l
  33. 0033specialize prime_contribution_prefix_decoded_choice i
  34. 0034specialize prime_contribution_prefix_decoded_choice a
  35. 0035apply prime_contribution_prefix_decoded_choice
  36. 0036exact hf
  37. 0037exact hi
  38. 0038exact ha
  39. 0039cases hb
  40. 0040cases hb_left
  41. 0041cases hv
  42. 0042cases hv_left
  43. 0043cases hv_left_right
  44. 0044cases hv_left_right_witness
  45. 0045right
  46. 0046split
  47. 0047exact hb_left_right
  48. 0048specialize central_binom_prime_power_contribution_le_double (S i)
  49. 0049specialize central_binom_prime_power_contribution_le_double n
  50. 0050specialize central_binom_prime_power_contribution_le_double C
  51. 0051specialize central_binom_prime_power_contribution_le_double x
  52. 0052specialize central_binom_prime_power_contribution_le_double a
  53. 0053apply central_binom_prime_power_contribution_le_double
  54. 0054exact hb_left_left
  55. 0055exact hn
  56. 0056exact hC
  57. 0057exact hv_left_right_witness_left
  58. 0058exact hv_left_right_witness_right
  59. 0059cases hv_right
  60. 0060exfalso
  61. 0061apply hv_right_left
  62. 0062exact hb_left_left
  63. 0063cases hb_right
  64. 0064cases hv
  65. 0065cases hv_left
  66. 0066exfalso
  67. 0067apply hb_right_left
  68. 0068exact hv_left_left
  69. 0069cases hv_right
  70. 0070left
  71. 0071split
  72. 0072exact hb_right_right
  73. 0073exact hv_right_right