PC001F

central_binom_prime_count_power_bound

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

The actual central binomial coefficient is at most (2n)^pi(N) whenever 2n is at most N; all factors and prime counts are constructed.

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 N k C Q. (exists pc_le_central_count_positive. pc_le_central_count_positive + (1) = (n)) -> (exists pc_le_central_count_range. pc_le_central_count_range + (n + n) = (N)) -> (exists pc_code_central_count_count pc_scale_central_count_count. (forall pc_index_central_count_count_mask. (exists pc_lt_central_count_count_mask_bound. pc_lt_central_count_count_mask_bound + S (pc_index_central_count_count_mask) = (N)) -> exists pc_bit_central_count_count_mask. (((exists fs_h_pc_central_count_count_mask_entry. fs_h_pc_central_count_count_mask_entry + S (pc_bit_central_count_count_mask) = S ((S (pc_index_central_count_count_mask)) * pc_scale_central_count_count)) /\ exists fs_q_pc_central_count_count_mask_entry. pc_code_central_count_count = fs_q_pc_central_count_count_mask_entry * S ((S (pc_index_central_count_count_mask)) * pc_scale_central_count_count) + (pc_bit_central_count_count_mask))) /\ (((((~(S (pc_index_central_count_count_mask) = 1) /\ forall bpr_left_pc_central_count_count_mask_choice_prime bpr_right_pc_central_count_count_mask_choice_prime. S (pc_index_central_count_count_mask) = bpr_left_pc_central_count_count_mask_choice_prime * bpr_right_pc_central_count_count_mask_choice_prime -> bpr_left_pc_central_count_count_mask_choice_prime = 1 \/ bpr_right_pc_central_count_count_mask_choice_prime = 1)) /\ pc_bit_central_count_count_mask = 1) \/ (~((~(S (pc_index_central_count_count_mask) = 1) /\ forall bpr_left_pc_central_count_count_mask_choice_prime bpr_right_pc_central_count_count_mask_choice_prime. S (pc_index_central_count_count_mask) = bpr_left_pc_central_count_count_mask_choice_prime * bpr_right_pc_central_count_count_mask_choice_prime -> bpr_left_pc_central_count_count_mask_choice_prime = 1 \/ bpr_right_pc_central_count_count_mask_choice_prime = 1)) /\ pc_bit_central_count_count_mask = 0)))) /\ (exists fs_u_pc_central_count_count_sum fs_v_pc_central_count_count_sum. ((((exists fs_h_pc_central_count_count_sum_body_start. fs_h_pc_central_count_count_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_central_count_count_sum)) /\ exists fs_q_pc_central_count_count_sum_body_start. fs_u_pc_central_count_count_sum = fs_q_pc_central_count_count_sum_body_start * S ((S (0)) * fs_v_pc_central_count_count_sum) + (0))) /\ ((((exists fs_h_pc_central_count_count_sum_body_terminal. fs_h_pc_central_count_count_sum_body_terminal + S (k) = S ((S (N)) * fs_v_pc_central_count_count_sum)) /\ exists fs_q_pc_central_count_count_sum_body_terminal. fs_u_pc_central_count_count_sum = fs_q_pc_central_count_count_sum_body_terminal * S ((S (N)) * fs_v_pc_central_count_count_sum) + (k))) /\ forall fs_i_pc_central_count_count_sum_body_steps. (exists fs_lt_pc_central_count_count_sum_body_steps_bound. fs_lt_pc_central_count_count_sum_body_steps_bound + S fs_i_pc_central_count_count_sum_body_steps = N) -> exists fs_a_pc_central_count_count_sum_body_steps fs_r_pc_central_count_count_sum_body_steps fs_s_pc_central_count_count_sum_body_steps. ((((exists fs_h_pc_central_count_count_sum_body_steps_summand. fs_h_pc_central_count_count_sum_body_steps_summand + S (fs_a_pc_central_count_count_sum_body_steps) = S ((S (fs_i_pc_central_count_count_sum_body_steps)) * pc_scale_central_count_count)) /\ exists fs_q_pc_central_count_count_sum_body_steps_summand. pc_code_central_count_count = fs_q_pc_central_count_count_sum_body_steps_summand * S ((S (fs_i_pc_central_count_count_sum_body_steps)) * pc_scale_central_count_count) + (fs_a_pc_central_count_count_sum_body_steps))) /\ ((((exists fs_h_pc_central_count_count_sum_body_steps_partial. fs_h_pc_central_count_count_sum_body_steps_partial + S (fs_r_pc_central_count_count_sum_body_steps) = S ((S (fs_i_pc_central_count_count_sum_body_steps)) * fs_v_pc_central_count_count_sum)) /\ exists fs_q_pc_central_count_count_sum_body_steps_partial. fs_u_pc_central_count_count_sum = fs_q_pc_central_count_count_sum_body_steps_partial * S ((S (fs_i_pc_central_count_count_sum_body_steps)) * fs_v_pc_central_count_count_sum) + (fs_r_pc_central_count_count_sum_body_steps))) /\ ((((exists fs_h_pc_central_count_count_sum_body_steps_successor. fs_h_pc_central_count_count_sum_body_steps_successor + S (fs_s_pc_central_count_count_sum_body_steps) = S ((S (S fs_i_pc_central_count_count_sum_body_steps)) * fs_v_pc_central_count_count_sum)) /\ exists fs_q_pc_central_count_count_sum_body_steps_successor. fs_u_pc_central_count_count_sum = fs_q_pc_central_count_count_sum_body_steps_successor * S ((S (S fs_i_pc_central_count_count_sum_body_steps)) * fs_v_pc_central_count_count_sum) + (fs_s_pc_central_count_count_sum_body_steps))) /\ fs_s_pc_central_count_count_sum_body_steps = fs_r_pc_central_count_count_sum_body_steps + fs_a_pc_central_count_count_sum_body_steps))))))) -> (((exists bcf_lt_gap_pc_central_count_value_out_of_range. bcf_lt_gap_pc_central_count_value_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_pc_central_count_value_in_range. bcf_le_gap_pc_central_count_value_in_range + (n) = n + n) /\ (exists bcf_row_code_code_pc_central_count_value bcf_row_code_scale_pc_central_count_value bcf_row_scale_code_pc_central_count_value bcf_row_scale_scale_pc_central_count_value bcf_row_code_pc_central_count_value bcf_row_scale_pc_central_count_value. ((forall bcf_row_index_pc_central_count_value_table. (exists bcf_lt_gap_pc_central_count_value_table_row_bound. bcf_lt_gap_pc_central_count_value_table_row_bound + S (bcf_row_index_pc_central_count_value_table) = S (n + n)) -> exists bcf_row_code_pc_central_count_value_table bcf_row_scale_pc_central_count_value_table. ((((exists bcf_height_pc_central_count_value_table_decoded_row_code. bcf_height_pc_central_count_value_table_decoded_row_code + S (bcf_row_code_pc_central_count_value_table) = S ((S (bcf_row_index_pc_central_count_value_table)) * bcf_row_code_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_table_decoded_row_code. bcf_row_code_code_pc_central_count_value = bcf_quotient_pc_central_count_value_table_decoded_row_code * S ((S (bcf_row_index_pc_central_count_value_table)) * bcf_row_code_scale_pc_central_count_value) + (bcf_row_code_pc_central_count_value_table))) /\ ((((exists bcf_height_pc_central_count_value_table_decoded_row_scale. bcf_height_pc_central_count_value_table_decoded_row_scale + S (bcf_row_scale_pc_central_count_value_table) = S ((S (bcf_row_index_pc_central_count_value_table)) * bcf_row_scale_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_table_decoded_row_scale. bcf_row_scale_code_pc_central_count_value = bcf_quotient_pc_central_count_value_table_decoded_row_scale * S ((S (bcf_row_index_pc_central_count_value_table)) * bcf_row_scale_scale_pc_central_count_value) + (bcf_row_scale_pc_central_count_value_table))) /\ ((bcf_row_index_pc_central_count_value_table = 0 /\ (forall bcf_index_pc_central_count_value_table_zero_row. (exists bcf_lt_gap_pc_central_count_value_table_zero_row_bound. bcf_lt_gap_pc_central_count_value_table_zero_row_bound + S (bcf_index_pc_central_count_value_table_zero_row) = S (n + n)) -> exists bcf_value_pc_central_count_value_table_zero_row. ((((exists bcf_height_pc_central_count_value_table_zero_row_entry. bcf_height_pc_central_count_value_table_zero_row_entry + S (bcf_value_pc_central_count_value_table_zero_row) = S ((S (bcf_index_pc_central_count_value_table_zero_row)) * bcf_row_scale_pc_central_count_value_table)) /\ exists bcf_quotient_pc_central_count_value_table_zero_row_entry. bcf_row_code_pc_central_count_value_table = bcf_quotient_pc_central_count_value_table_zero_row_entry * S ((S (bcf_index_pc_central_count_value_table_zero_row)) * bcf_row_scale_pc_central_count_value_table) + (bcf_value_pc_central_count_value_table_zero_row))) /\ ((bcf_index_pc_central_count_value_table_zero_row = 0 /\ bcf_value_pc_central_count_value_table_zero_row = 1) \/ exists bcf_predecessor_pc_central_count_value_table_zero_row. bcf_index_pc_central_count_value_table_zero_row = S bcf_predecessor_pc_central_count_value_table_zero_row /\ bcf_value_pc_central_count_value_table_zero_row = 0)))) \/ exists bcf_predecessor_pc_central_count_value_table bcf_previous_code_pc_central_count_value_table bcf_previous_scale_pc_central_count_value_table. bcf_row_index_pc_central_count_value_table = S bcf_predecessor_pc_central_count_value_table /\ ((((exists bcf_height_pc_central_count_value_table_decoded_previous_code. bcf_height_pc_central_count_value_table_decoded_previous_code + S (bcf_previous_code_pc_central_count_value_table) = S ((S (bcf_predecessor_pc_central_count_value_table)) * bcf_row_code_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_table_decoded_previous_code. bcf_row_code_code_pc_central_count_value = bcf_quotient_pc_central_count_value_table_decoded_previous_code * S ((S (bcf_predecessor_pc_central_count_value_table)) * bcf_row_code_scale_pc_central_count_value) + (bcf_previous_code_pc_central_count_value_table))) /\ ((((exists bcf_height_pc_central_count_value_table_decoded_previous_scale. bcf_height_pc_central_count_value_table_decoded_previous_scale + S (bcf_previous_scale_pc_central_count_value_table) = S ((S (bcf_predecessor_pc_central_count_value_table)) * bcf_row_scale_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_table_decoded_previous_scale. bcf_row_scale_code_pc_central_count_value = bcf_quotient_pc_central_count_value_table_decoded_previous_scale * S ((S (bcf_predecessor_pc_central_count_value_table)) * bcf_row_scale_scale_pc_central_count_value) + (bcf_previous_scale_pc_central_count_value_table))) /\ (forall bcf_index_pc_central_count_value_table_row_step. (exists bcf_lt_gap_pc_central_count_value_table_row_step_bound. bcf_lt_gap_pc_central_count_value_table_row_step_bound + S (bcf_index_pc_central_count_value_table_row_step) = S (n + n)) -> exists bcf_value_pc_central_count_value_table_row_step. ((((exists bcf_height_pc_central_count_value_table_row_step_entry. bcf_height_pc_central_count_value_table_row_step_entry + S (bcf_value_pc_central_count_value_table_row_step) = S ((S (bcf_index_pc_central_count_value_table_row_step)) * bcf_row_scale_pc_central_count_value_table)) /\ exists bcf_quotient_pc_central_count_value_table_row_step_entry. bcf_row_code_pc_central_count_value_table = bcf_quotient_pc_central_count_value_table_row_step_entry * S ((S (bcf_index_pc_central_count_value_table_row_step)) * bcf_row_scale_pc_central_count_value_table) + (bcf_value_pc_central_count_value_table_row_step))) /\ ((bcf_index_pc_central_count_value_table_row_step = 0 /\ bcf_value_pc_central_count_value_table_row_step = 1) \/ exists bcf_predecessor_pc_central_count_value_table_row_step bcf_left_pc_central_count_value_table_row_step bcf_right_pc_central_count_value_table_row_step. bcf_index_pc_central_count_value_table_row_step = S bcf_predecessor_pc_central_count_value_table_row_step /\ ((((exists bcf_height_pc_central_count_value_table_row_step_previous_left. bcf_height_pc_central_count_value_table_row_step_previous_left + S (bcf_left_pc_central_count_value_table_row_step) = S ((S (bcf_predecessor_pc_central_count_value_table_row_step)) * bcf_previous_scale_pc_central_count_value_table)) /\ exists bcf_quotient_pc_central_count_value_table_row_step_previous_left. bcf_previous_code_pc_central_count_value_table = bcf_quotient_pc_central_count_value_table_row_step_previous_left * S ((S (bcf_predecessor_pc_central_count_value_table_row_step)) * bcf_previous_scale_pc_central_count_value_table) + (bcf_left_pc_central_count_value_table_row_step))) /\ ((((exists bcf_height_pc_central_count_value_table_row_step_previous_right. bcf_height_pc_central_count_value_table_row_step_previous_right + S (bcf_right_pc_central_count_value_table_row_step) = S ((S (S (bcf_predecessor_pc_central_count_value_table_row_step))) * bcf_previous_scale_pc_central_count_value_table)) /\ exists bcf_quotient_pc_central_count_value_table_row_step_previous_right. bcf_previous_code_pc_central_count_value_table = bcf_quotient_pc_central_count_value_table_row_step_previous_right * S ((S (S (bcf_predecessor_pc_central_count_value_table_row_step))) * bcf_previous_scale_pc_central_count_value_table) + (bcf_right_pc_central_count_value_table_row_step))) /\ bcf_value_pc_central_count_value_table_row_step = bcf_left_pc_central_count_value_table_row_step + bcf_right_pc_central_count_value_table_row_step))))))))))) /\ ((((exists bcf_height_pc_central_count_value_decoded_row_code. bcf_height_pc_central_count_value_decoded_row_code + S (bcf_row_code_pc_central_count_value) = S ((S (n + n)) * bcf_row_code_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_decoded_row_code. bcf_row_code_code_pc_central_count_value = bcf_quotient_pc_central_count_value_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_pc_central_count_value) + (bcf_row_code_pc_central_count_value))) /\ ((((exists bcf_height_pc_central_count_value_decoded_row_scale. bcf_height_pc_central_count_value_decoded_row_scale + S (bcf_row_scale_pc_central_count_value) = S ((S (n + n)) * bcf_row_scale_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_decoded_row_scale. bcf_row_scale_code_pc_central_count_value = bcf_quotient_pc_central_count_value_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_pc_central_count_value) + (bcf_row_scale_pc_central_count_value))) /\ (((exists bcf_height_pc_central_count_value_decoded_value. bcf_height_pc_central_count_value_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_pc_central_count_value)) /\ exists bcf_quotient_pc_central_count_value_decoded_value. bcf_row_code_pc_central_count_value = bcf_quotient_pc_central_count_value_decoded_value * S ((S (n)) * bcf_row_scale_pc_central_count_value) + (C))))))))) -> (exists pa_b_pc_central_count_power pa_c_pc_central_count_power. ((forall pa_i_pc_central_count_power_repeat. (exists pa_lt_pc_central_count_power_repeat_bound. pa_lt_pc_central_count_power_repeat_bound + S pa_i_pc_central_count_power_repeat = k) -> (((exists pa_h_pc_central_count_power_repeat_decoded. pa_h_pc_central_count_power_repeat_decoded + S (n + n) = S ((S (pa_i_pc_central_count_power_repeat)) * pa_c_pc_central_count_power)) /\ exists pa_q_pc_central_count_power_repeat_decoded. pa_b_pc_central_count_power = pa_q_pc_central_count_power_repeat_decoded * S ((S (pa_i_pc_central_count_power_repeat)) * pa_c_pc_central_count_power) + (n + n)))) /\ (exists pa_u_pc_central_count_power_product pa_v_pc_central_count_power_product. ((((exists pa_h_pc_central_count_power_product_start. pa_h_pc_central_count_power_product_start + S (1) = S ((S (0)) * pa_v_pc_central_count_power_product)) /\ exists pa_q_pc_central_count_power_product_start. pa_u_pc_central_count_power_product = pa_q_pc_central_count_power_product_start * S ((S (0)) * pa_v_pc_central_count_power_product) + (1))) /\ ((((exists pa_h_pc_central_count_power_product_terminal. pa_h_pc_central_count_power_product_terminal + S (Q) = S ((S (k)) * pa_v_pc_central_count_power_product)) /\ exists pa_q_pc_central_count_power_product_terminal. pa_u_pc_central_count_power_product = pa_q_pc_central_count_power_product_terminal * S ((S (k)) * pa_v_pc_central_count_power_product) + (Q))) /\ forall pa_i_pc_central_count_power_product. (exists pa_lt_pc_central_count_power_product_bound. pa_lt_pc_central_count_power_product_bound + S pa_i_pc_central_count_power_product = k) -> exists pa_p_pc_central_count_power_product pa_r_pc_central_count_power_product pa_s_pc_central_count_power_product. ((((exists pa_h_pc_central_count_power_product_factor. pa_h_pc_central_count_power_product_factor + S (pa_p_pc_central_count_power_product) = S ((S (pa_i_pc_central_count_power_product)) * pa_c_pc_central_count_power)) /\ exists pa_q_pc_central_count_power_product_factor. pa_b_pc_central_count_power = pa_q_pc_central_count_power_product_factor * S ((S (pa_i_pc_central_count_power_product)) * pa_c_pc_central_count_power) + (pa_p_pc_central_count_power_product))) /\ ((((exists pa_h_pc_central_count_power_product_partial. pa_h_pc_central_count_power_product_partial + S (pa_r_pc_central_count_power_product) = S ((S (pa_i_pc_central_count_power_product)) * pa_v_pc_central_count_power_product)) /\ exists pa_q_pc_central_count_power_product_partial. pa_u_pc_central_count_power_product = pa_q_pc_central_count_power_product_partial * S ((S (pa_i_pc_central_count_power_product)) * pa_v_pc_central_count_power_product) + (pa_r_pc_central_count_power_product))) /\ ((((exists pa_h_pc_central_count_power_product_successor. pa_h_pc_central_count_power_product_successor + S (pa_s_pc_central_count_power_product) = S ((S (S pa_i_pc_central_count_power_product)) * pa_v_pc_central_count_power_product)) /\ exists pa_q_pc_central_count_power_product_successor. pa_u_pc_central_count_power_product = pa_q_pc_central_count_power_product_successor * S ((S (S pa_i_pc_central_count_power_product)) * pa_v_pc_central_count_power_product) + (pa_s_pc_central_count_power_product))) /\ pa_s_pc_central_count_power_product = pa_r_pc_central_count_power_product * pa_p_pc_central_count_power_product)))))))) -> (exists pc_le_central_count_result. pc_le_central_count_result + (C) = (Q))

Constructive proof overview

Generated structural guide

The actual central binomial coefficient is at most (2n)^pi(N) whenever 2n is at most N; all factors and prime counts are constructed.

The unchanged tactic script uses 6 declared prerequisites and contains 75 exact native proof lines.

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

Proof neighborhood

Direct dependencies

central_binom_positive Alpha theorem; checked-use authorized prime_contribution_complete_exists Alpha theorem; checked-use authorized central_binom_prime_divisor_le_double Alpha theorem; checked-use authorized le_trans Stable theorem; checked-use authorized PC000C beta_product_bit_weighted_upper_power PC001D central_binom_prime_mask_weighted_upper

Direct dependents

PC002E central_binom_prime_count_exponent_bound

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

75 script commands · 16 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.

Named ingredients (2)
beta product bit weighted upper powercentral binom prime mask weighted upper

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–10

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

  1. L1
    intro n
  2. L2
    intro N
  3. L3
    intro k
  4. L4
    intro C
  5. L5
    intro Q
  6. L6
    intro hn
  7. L7
    intro hN
  8. L8
    intro hk
  9. L9
    intro hC
  10. L10
    intro hQ
02Separate the logical casesL11–13

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

  1. L11
    cases hk
  2. L12
    cases hk_witness
  3. L13
    cases hk_witness_witness
03Establish hcompleteL14–18

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

  1. L14
    have hcomplete : ∃ z. (∃ x. ∃ y. (∀ n. Lt(n,N) → ∃ m. BetaAt(x,y,n,m) ∧ (Prime(S n) ∧ (∃ k. Le(k,C) ∧ (∃ i. Pow(S n,k,i) ∧ (∃ j. C = i · j)) ∧ (∀ i. Le(i,C) → (∃ j. Pow(S n,i,j) ∧ (∃ u. C = j · u)) → Le(i,k)) ∧ Pow(S n,k,m)) ∨ ¬Prime(S n) ∧ m = 1)) ∧ Product(x,y,N,z)) ∧ C = zDefinitions: LeLtPrimeBetaAtProductPow
  2. L15
    specialize prime_contribution_complete_exists C
  3. L16
    specialize prime_contribution_complete_exists N
  4. L17
    apply prime_contribution_complete_exists
  5. L18
    intro hz
04Establish hpL19–23

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

  1. L19
    have hp : exists r. C = S r
  2. L20
    specialize central_binom_positive n
  3. L21
    specialize central_binom_positive C
  4. L22
    apply central_binom_positive
  5. L23
    exact hC
05Separate the logical casesL24–24

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

  1. L24
    cases hp
06Use earlier factsL25–25

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

  1. L25
    apply PA1
07Calculate and transport equalitiesL26–27

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

  1. L26
    trans C
  2. L27
    symm
08Use earlier factsL28–29

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

  1. L28
    exact hp_witness
  2. L29
    exact hz
09Fix variables and assumptionsL30–32

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

  1. L30
    intro p
  2. L31
    intro hp
  3. L32
    intro hd
10Use earlier factsL33–42

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

  1. L33
    specialize le_trans p
  2. L34
    specialize le_trans (n + n)
  3. L35
    specialize le_trans N
  4. L36
    apply le_trans
  5. L37
    specialize central_binom_prime_divisor_le_double n
  6. L38
    specialize central_binom_prime_divisor_le_double C
  7. L39
    specialize central_binom_prime_divisor_le_double p
  8. L40
    apply central_binom_prime_divisor_le_double
  9. L41
    exact hp
  10. L42
    exact hC
11Use earlier factsL43–44

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

  1. L43
    exact hd
  2. L44
    exact hN
12Separate the logical casesL45–49

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

  1. L45
    cases hcomplete
  2. L46
    cases hcomplete_witness
  3. L47
    cases hcomplete_witness_left
  4. L48
    cases hcomplete_witness_left_witness
  5. L49
    cases hcomplete_witness_left_witness_witness
13Calculate and transport equalitiesL50–50

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

  1. L50
    rewrite hcomplete_witness_right
14Use earlier factsL51–60

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

  1. L51
    specialize beta_product_bit_weighted_upper_power x3
  2. L52
    specialize beta_product_bit_weighted_upper_power x4
  3. L53
    specialize beta_product_bit_weighted_upper_power x
  4. L54
    specialize beta_product_bit_weighted_upper_power x1
  5. L55
    specialize beta_product_bit_weighted_upper_power (n + n)
  6. L56
    specialize beta_product_bit_weighted_upper_power N
  7. L57
    specialize beta_product_bit_weighted_upper_power x2
  8. L58
    specialize beta_product_bit_weighted_upper_power k
  9. L59
    specialize beta_product_bit_weighted_upper_power Q
  10. L60
    apply beta_product_bit_weighted_upper_power
15Use earlier factsL61–70

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

  1. L61
    specialize central_binom_prime_mask_weighted_upper n
  2. L62
    specialize central_binom_prime_mask_weighted_upper C
  3. L63
    specialize central_binom_prime_mask_weighted_upper x3
  4. L64
    specialize central_binom_prime_mask_weighted_upper x4
  5. L65
    specialize central_binom_prime_mask_weighted_upper x
  6. L66
    specialize central_binom_prime_mask_weighted_upper x1
  7. L67
    specialize central_binom_prime_mask_weighted_upper N
  8. L68
    apply central_binom_prime_mask_weighted_upper
  9. L69
    exact hn
  10. L70
    exact hC
16Use earlier factsL71–75

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

  1. L71
    exact hcomplete_witness_left_witness_witness_left
  2. L72
    exact hk_witness_witness_left
  3. L73
    exact hcomplete_witness_left_witness_witness_right
  4. L74
    exact hk_witness_witness_right
  5. L75
    exact hQ

Library-wide reading audit

Original exact command ledger · 75 lines
  1. 0001intro n
  2. 0002intro N
  3. 0003intro k
  4. 0004intro C
  5. 0005intro Q
  6. 0006intro hn
  7. 0007intro hN
  8. 0008intro hk
  9. 0009intro hC
  10. 0010intro hQ
  11. 0011cases hk
  12. 0012cases hk_witness
  13. 0013cases hk_witness_witness
  14. 0014have hcomplete : exists z. (exists bpr_product_code_pc_central_count_complete bpr_product_scale_pc_central_count_complete. ((forall bpr_prefix_index_pc_central_count_complete_prefix. (exists bpr_gap_pc_central_count_complete_prefix_bound. bpr_gap_pc_central_count_complete_prefix_bound + S (bpr_prefix_index_pc_central_count_complete_prefix) = N) -> exists bpr_prefix_value_pc_central_count_complete_prefix. ((((exists bpr_height_pc_central_count_complete_prefix_decoded. bpr_height_pc_central_count_complete_prefix_decoded + S (bpr_prefix_value_pc_central_count_complete_prefix) = S ((S (bpr_prefix_index_pc_central_count_complete_prefix)) * bpr_product_scale_pc_central_count_complete)) /\ exists bpr_quotient_pc_central_count_complete_prefix_decoded. bpr_product_code_pc_central_count_complete = bpr_quotient_pc_central_count_complete_prefix_decoded * S ((S (bpr_prefix_index_pc_central_count_complete_prefix)) * bpr_product_scale_pc_central_count_complete) + (bpr_prefix_value_pc_central_count_complete_prefix))) /\ (((((~(S (bpr_prefix_index_pc_central_count_complete_prefix) = 1) /\ forall bpr_left_pc_central_count_complete_prefix_choice_prime bpr_right_pc_central_count_complete_prefix_choice_prime. S (bpr_prefix_index_pc_central_count_complete_prefix) = bpr_left_pc_central_count_complete_prefix_choice_prime * bpr_right_pc_central_count_complete_prefix_choice_prime -> bpr_left_pc_central_count_complete_prefix_choice_prime = 1 \/ bpr_right_pc_central_count_complete_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_pc_central_count_complete_prefix_choice. ((((exists bpr_le_gap_pc_central_count_complete_prefix_choice_valuation_selected_bound. bpr_le_gap_pc_central_count_complete_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_pc_central_count_complete_prefix_choice) = (C)) /\ (exists bpr_power_value_pc_central_count_complete_prefix_choice_valuation_selected. ((exists bpr_power_code_pc_central_count_complete_prefix_choice_valuation_selected_power bpr_power_scale_pc_central_count_complete_prefix_choice_valuation_selected_power. ((forall bpr_power_index_pc_central_count_complete_prefix_choice_valuation_selected_power. (exists bpr_gap_pc_central_count_complete_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_pc_central_count_complete_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_pc_central_count_complete_prefix_choice_valuation_selected_power) = bpr_choice_exponent_pc_central_count_complete_prefix_choice) -> (((exists bpr_height_pc_central_count_complete_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_pc_central_count_complete_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_pc_central_count_complete_prefix)) = S ((S (bpr_power_index_pc_central_count_complete_prefix_choice_valuation_selected_power)) * bpr_power_scale_pc_central_count_complete_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_pc_central_count_complete_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_pc_central_count_complete_prefix_choice_valuation_selected_power = bpr_quotient_pc_central_count_complete_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_pc_central_count_complete_prefix_choice_valuation_selected_power)) * bpr_power_scale_pc_central_count_complete_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_pc_central_count_complete_prefix))))) /\ (exists ff_u_pc_central_count_complete_prefix_choice_valuation_selected_power_product ff_v_pc_central_count_complete_prefix_choice_valuation_selected_power_product. ((((exists ff_h_pc_central_count_complete_prefix_choice_valuation_selected_power_product_start. ff_h_pc_central_count_complete_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_pc_central_count_complete_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_valuation_selected_power_product_start. ff_u_pc_central_count_complete_prefix_choice_valuation_selected_power_product = ff_q_pc_central_count_complete_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_pc_central_count_complete_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_pc_central_count_complete_prefix_choice_valuation_selected_power_product_terminal. ff_h_pc_central_count_complete_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_pc_central_count_complete_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_pc_central_count_complete_prefix_choice)) * ff_v_pc_central_count_complete_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_valuation_selected_power_product_terminal. ff_u_pc_central_count_complete_prefix_choice_valuation_selected_power_product = ff_q_pc_central_count_complete_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_pc_central_count_complete_prefix_choice)) * ff_v_pc_central_count_complete_prefix_choice_valuation_selected_power_product) + (bpr_power_value_pc_central_count_complete_prefix_choice_valuation_selected))) /\ forall ff_i_pc_central_count_complete_prefix_choice_valuation_selected_power_product. (exists ff_lt_pc_central_count_complete_prefix_choice_valuation_selected_power_product_bound. ff_lt_pc_central_count_complete_prefix_choice_valuation_selected_power_product_bound + S ff_i_pc_central_count_complete_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_pc_central_count_complete_prefix_choice) -> exists ff_p_pc_central_count_complete_prefix_choice_valuation_selected_power_product ff_r_pc_central_count_complete_prefix_choice_valuation_selected_power_product ff_s_pc_central_count_complete_prefix_choice_valuation_selected_power_product. ((((exists ff_h_pc_central_count_complete_prefix_choice_valuation_selected_power_product_factor. ff_h_pc_central_count_complete_prefix_choice_valuation_selected_power_product_factor + S (ff_p_pc_central_count_complete_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_pc_central_count_complete_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_pc_central_count_complete_prefix_choice_valuation_selected_power)) /\ exists ff_q_pc_central_count_complete_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_pc_central_count_complete_prefix_choice_valuation_selected_power = ff_q_pc_central_count_complete_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_pc_central_count_complete_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_pc_central_count_complete_prefix_choice_valuation_selected_power) + (ff_p_pc_central_count_complete_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_pc_central_count_complete_prefix_choice_valuation_selected_power_product_partial. ff_h_pc_central_count_complete_prefix_choice_valuation_selected_power_product_partial + S (ff_r_pc_central_count_complete_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_pc_central_count_complete_prefix_choice_valuation_selected_power_product)) * ff_v_pc_central_count_complete_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_valuation_selected_power_product_partial. ff_u_pc_central_count_complete_prefix_choice_valuation_selected_power_product = ff_q_pc_central_count_complete_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_pc_central_count_complete_prefix_choice_valuation_selected_power_product)) * ff_v_pc_central_count_complete_prefix_choice_valuation_selected_power_product) + (ff_r_pc_central_count_complete_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_pc_central_count_complete_prefix_choice_valuation_selected_power_product_successor. ff_h_pc_central_count_complete_prefix_choice_valuation_selected_power_product_successor + S (ff_s_pc_central_count_complete_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_pc_central_count_complete_prefix_choice_valuation_selected_power_product)) * ff_v_pc_central_count_complete_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_valuation_selected_power_product_successor. ff_u_pc_central_count_complete_prefix_choice_valuation_selected_power_product = ff_q_pc_central_count_complete_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_pc_central_count_complete_prefix_choice_valuation_selected_power_product)) * ff_v_pc_central_count_complete_prefix_choice_valuation_selected_power_product) + (ff_s_pc_central_count_complete_prefix_choice_valuation_selected_power_product))) /\ ff_s_pc_central_count_complete_prefix_choice_valuation_selected_power_product = ff_r_pc_central_count_complete_prefix_choice_valuation_selected_power_product * ff_p_pc_central_count_complete_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_pc_central_count_complete_prefix_choice_valuation_selected_divides. C = (bpr_power_value_pc_central_count_complete_prefix_choice_valuation_selected) * bpr_divides_quotient_pc_central_count_complete_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_pc_central_count_complete_prefix_choice_valuation. (exists bpr_le_gap_pc_central_count_complete_prefix_choice_valuation_candidate_bound. bpr_le_gap_pc_central_count_complete_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_pc_central_count_complete_prefix_choice_valuation) = (C)) -> (exists bpr_power_value_pc_central_count_complete_prefix_choice_valuation_candidate. ((exists bpr_power_code_pc_central_count_complete_prefix_choice_valuation_candidate_power bpr_power_scale_pc_central_count_complete_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_pc_central_count_complete_prefix_choice_valuation_candidate_power. (exists bpr_gap_pc_central_count_complete_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_pc_central_count_complete_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_pc_central_count_complete_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_pc_central_count_complete_prefix_choice_valuation) -> (((exists bpr_height_pc_central_count_complete_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_pc_central_count_complete_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_pc_central_count_complete_prefix)) = S ((S (bpr_power_index_pc_central_count_complete_prefix_choice_valuation_candidate_power)) * bpr_power_scale_pc_central_count_complete_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_pc_central_count_complete_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_pc_central_count_complete_prefix_choice_valuation_candidate_power = bpr_quotient_pc_central_count_complete_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_pc_central_count_complete_prefix_choice_valuation_candidate_power)) * bpr_power_scale_pc_central_count_complete_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_pc_central_count_complete_prefix))))) /\ (exists ff_u_pc_central_count_complete_prefix_choice_valuation_candidate_power_product ff_v_pc_central_count_complete_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_start. ff_h_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_start. ff_u_pc_central_count_complete_prefix_choice_valuation_candidate_power_product = ff_q_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_pc_central_count_complete_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_terminal. ff_h_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_pc_central_count_complete_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_pc_central_count_complete_prefix_choice_valuation)) * ff_v_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_terminal. ff_u_pc_central_count_complete_prefix_choice_valuation_candidate_power_product = ff_q_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_pc_central_count_complete_prefix_choice_valuation)) * ff_v_pc_central_count_complete_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_pc_central_count_complete_prefix_choice_valuation_candidate))) /\ forall ff_i_pc_central_count_complete_prefix_choice_valuation_candidate_power_product. (exists ff_lt_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_bound. ff_lt_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_bound + S ff_i_pc_central_count_complete_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_pc_central_count_complete_prefix_choice_valuation) -> exists ff_p_pc_central_count_complete_prefix_choice_valuation_candidate_power_product ff_r_pc_central_count_complete_prefix_choice_valuation_candidate_power_product ff_s_pc_central_count_complete_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_factor. ff_h_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_pc_central_count_complete_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_pc_central_count_complete_prefix_choice_valuation_candidate_power)) /\ exists ff_q_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_pc_central_count_complete_prefix_choice_valuation_candidate_power = ff_q_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_pc_central_count_complete_prefix_choice_valuation_candidate_power) + (ff_p_pc_central_count_complete_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_partial. ff_h_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_pc_central_count_complete_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)) * ff_v_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_partial. ff_u_pc_central_count_complete_prefix_choice_valuation_candidate_power_product = ff_q_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)) * ff_v_pc_central_count_complete_prefix_choice_valuation_candidate_power_product) + (ff_r_pc_central_count_complete_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_successor. ff_h_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_pc_central_count_complete_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)) * ff_v_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_successor. ff_u_pc_central_count_complete_prefix_choice_valuation_candidate_power_product = ff_q_pc_central_count_complete_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)) * ff_v_pc_central_count_complete_prefix_choice_valuation_candidate_power_product) + (ff_s_pc_central_count_complete_prefix_choice_valuation_candidate_power_product))) /\ ff_s_pc_central_count_complete_prefix_choice_valuation_candidate_power_product = ff_r_pc_central_count_complete_prefix_choice_valuation_candidate_power_product * ff_p_pc_central_count_complete_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_pc_central_count_complete_prefix_choice_valuation_candidate_divides. C = (bpr_power_value_pc_central_count_complete_prefix_choice_valuation_candidate) * bpr_divides_quotient_pc_central_count_complete_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_pc_central_count_complete_prefix_choice_valuation_candidate_below. bpr_le_gap_pc_central_count_complete_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_pc_central_count_complete_prefix_choice_valuation) = (bpr_choice_exponent_pc_central_count_complete_prefix_choice))) /\ (exists bpr_power_code_pc_central_count_complete_prefix_choice_power bpr_power_scale_pc_central_count_complete_prefix_choice_power. ((forall bpr_power_index_pc_central_count_complete_prefix_choice_power. (exists bpr_gap_pc_central_count_complete_prefix_choice_power_repeat_bound. bpr_gap_pc_central_count_complete_prefix_choice_power_repeat_bound + S (bpr_power_index_pc_central_count_complete_prefix_choice_power) = bpr_choice_exponent_pc_central_count_complete_prefix_choice) -> (((exists bpr_height_pc_central_count_complete_prefix_choice_power_repeat_entry. bpr_height_pc_central_count_complete_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_pc_central_count_complete_prefix)) = S ((S (bpr_power_index_pc_central_count_complete_prefix_choice_power)) * bpr_power_scale_pc_central_count_complete_prefix_choice_power)) /\ exists bpr_quotient_pc_central_count_complete_prefix_choice_power_repeat_entry. bpr_power_code_pc_central_count_complete_prefix_choice_power = bpr_quotient_pc_central_count_complete_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_pc_central_count_complete_prefix_choice_power)) * bpr_power_scale_pc_central_count_complete_prefix_choice_power) + (S (bpr_prefix_index_pc_central_count_complete_prefix))))) /\ (exists ff_u_pc_central_count_complete_prefix_choice_power_product ff_v_pc_central_count_complete_prefix_choice_power_product. ((((exists ff_h_pc_central_count_complete_prefix_choice_power_product_start. ff_h_pc_central_count_complete_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_pc_central_count_complete_prefix_choice_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_power_product_start. ff_u_pc_central_count_complete_prefix_choice_power_product = ff_q_pc_central_count_complete_prefix_choice_power_product_start * S ((S (0)) * ff_v_pc_central_count_complete_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_pc_central_count_complete_prefix_choice_power_product_terminal. ff_h_pc_central_count_complete_prefix_choice_power_product_terminal + S (bpr_prefix_value_pc_central_count_complete_prefix) = S ((S (bpr_choice_exponent_pc_central_count_complete_prefix_choice)) * ff_v_pc_central_count_complete_prefix_choice_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_power_product_terminal. ff_u_pc_central_count_complete_prefix_choice_power_product = ff_q_pc_central_count_complete_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_pc_central_count_complete_prefix_choice)) * ff_v_pc_central_count_complete_prefix_choice_power_product) + (bpr_prefix_value_pc_central_count_complete_prefix))) /\ forall ff_i_pc_central_count_complete_prefix_choice_power_product. (exists ff_lt_pc_central_count_complete_prefix_choice_power_product_bound. ff_lt_pc_central_count_complete_prefix_choice_power_product_bound + S ff_i_pc_central_count_complete_prefix_choice_power_product = bpr_choice_exponent_pc_central_count_complete_prefix_choice) -> exists ff_p_pc_central_count_complete_prefix_choice_power_product ff_r_pc_central_count_complete_prefix_choice_power_product ff_s_pc_central_count_complete_prefix_choice_power_product. ((((exists ff_h_pc_central_count_complete_prefix_choice_power_product_factor. ff_h_pc_central_count_complete_prefix_choice_power_product_factor + S (ff_p_pc_central_count_complete_prefix_choice_power_product) = S ((S (ff_i_pc_central_count_complete_prefix_choice_power_product)) * bpr_power_scale_pc_central_count_complete_prefix_choice_power)) /\ exists ff_q_pc_central_count_complete_prefix_choice_power_product_factor. bpr_power_code_pc_central_count_complete_prefix_choice_power = ff_q_pc_central_count_complete_prefix_choice_power_product_factor * S ((S (ff_i_pc_central_count_complete_prefix_choice_power_product)) * bpr_power_scale_pc_central_count_complete_prefix_choice_power) + (ff_p_pc_central_count_complete_prefix_choice_power_product))) /\ ((((exists ff_h_pc_central_count_complete_prefix_choice_power_product_partial. ff_h_pc_central_count_complete_prefix_choice_power_product_partial + S (ff_r_pc_central_count_complete_prefix_choice_power_product) = S ((S (ff_i_pc_central_count_complete_prefix_choice_power_product)) * ff_v_pc_central_count_complete_prefix_choice_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_power_product_partial. ff_u_pc_central_count_complete_prefix_choice_power_product = ff_q_pc_central_count_complete_prefix_choice_power_product_partial * S ((S (ff_i_pc_central_count_complete_prefix_choice_power_product)) * ff_v_pc_central_count_complete_prefix_choice_power_product) + (ff_r_pc_central_count_complete_prefix_choice_power_product))) /\ ((((exists ff_h_pc_central_count_complete_prefix_choice_power_product_successor. ff_h_pc_central_count_complete_prefix_choice_power_product_successor + S (ff_s_pc_central_count_complete_prefix_choice_power_product) = S ((S (S ff_i_pc_central_count_complete_prefix_choice_power_product)) * ff_v_pc_central_count_complete_prefix_choice_power_product)) /\ exists ff_q_pc_central_count_complete_prefix_choice_power_product_successor. ff_u_pc_central_count_complete_prefix_choice_power_product = ff_q_pc_central_count_complete_prefix_choice_power_product_successor * S ((S (S ff_i_pc_central_count_complete_prefix_choice_power_product)) * ff_v_pc_central_count_complete_prefix_choice_power_product) + (ff_s_pc_central_count_complete_prefix_choice_power_product))) /\ ff_s_pc_central_count_complete_prefix_choice_power_product = ff_r_pc_central_count_complete_prefix_choice_power_product * ff_p_pc_central_count_complete_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_pc_central_count_complete_prefix) = 1) /\ forall bpr_left_pc_central_count_complete_prefix_choice_prime bpr_right_pc_central_count_complete_prefix_choice_prime. S (bpr_prefix_index_pc_central_count_complete_prefix) = bpr_left_pc_central_count_complete_prefix_choice_prime * bpr_right_pc_central_count_complete_prefix_choice_prime -> bpr_left_pc_central_count_complete_prefix_choice_prime = 1 \/ bpr_right_pc_central_count_complete_prefix_choice_prime = 1)) /\ bpr_prefix_value_pc_central_count_complete_prefix = 1))))) /\ (exists ff_u_pc_central_count_complete_product ff_v_pc_central_count_complete_product. ((((exists ff_h_pc_central_count_complete_product_start. ff_h_pc_central_count_complete_product_start + S (1) = S ((S (0)) * ff_v_pc_central_count_complete_product)) /\ exists ff_q_pc_central_count_complete_product_start. ff_u_pc_central_count_complete_product = ff_q_pc_central_count_complete_product_start * S ((S (0)) * ff_v_pc_central_count_complete_product) + (1))) /\ ((((exists ff_h_pc_central_count_complete_product_terminal. ff_h_pc_central_count_complete_product_terminal + S (z) = S ((S (N)) * ff_v_pc_central_count_complete_product)) /\ exists ff_q_pc_central_count_complete_product_terminal. ff_u_pc_central_count_complete_product = ff_q_pc_central_count_complete_product_terminal * S ((S (N)) * ff_v_pc_central_count_complete_product) + (z))) /\ forall ff_i_pc_central_count_complete_product. (exists ff_lt_pc_central_count_complete_product_bound. ff_lt_pc_central_count_complete_product_bound + S ff_i_pc_central_count_complete_product = N) -> exists ff_p_pc_central_count_complete_product ff_r_pc_central_count_complete_product ff_s_pc_central_count_complete_product. ((((exists ff_h_pc_central_count_complete_product_factor. ff_h_pc_central_count_complete_product_factor + S (ff_p_pc_central_count_complete_product) = S ((S (ff_i_pc_central_count_complete_product)) * bpr_product_scale_pc_central_count_complete)) /\ exists ff_q_pc_central_count_complete_product_factor. bpr_product_code_pc_central_count_complete = ff_q_pc_central_count_complete_product_factor * S ((S (ff_i_pc_central_count_complete_product)) * bpr_product_scale_pc_central_count_complete) + (ff_p_pc_central_count_complete_product))) /\ ((((exists ff_h_pc_central_count_complete_product_partial. ff_h_pc_central_count_complete_product_partial + S (ff_r_pc_central_count_complete_product) = S ((S (ff_i_pc_central_count_complete_product)) * ff_v_pc_central_count_complete_product)) /\ exists ff_q_pc_central_count_complete_product_partial. ff_u_pc_central_count_complete_product = ff_q_pc_central_count_complete_product_partial * S ((S (ff_i_pc_central_count_complete_product)) * ff_v_pc_central_count_complete_product) + (ff_r_pc_central_count_complete_product))) /\ ((((exists ff_h_pc_central_count_complete_product_successor. ff_h_pc_central_count_complete_product_successor + S (ff_s_pc_central_count_complete_product) = S ((S (S ff_i_pc_central_count_complete_product)) * ff_v_pc_central_count_complete_product)) /\ exists ff_q_pc_central_count_complete_product_successor. ff_u_pc_central_count_complete_product = ff_q_pc_central_count_complete_product_successor * S ((S (S ff_i_pc_central_count_complete_product)) * ff_v_pc_central_count_complete_product) + (ff_s_pc_central_count_complete_product))) /\ ff_s_pc_central_count_complete_product = ff_r_pc_central_count_complete_product * ff_p_pc_central_count_complete_product)))))))) /\ C = z
  15. 0015specialize prime_contribution_complete_exists C
  16. 0016specialize prime_contribution_complete_exists N
  17. 0017apply prime_contribution_complete_exists
  18. 0018intro hz
  19. 0019have hp : exists r. C = S r
  20. 0020specialize central_binom_positive n
  21. 0021specialize central_binom_positive C
  22. 0022apply central_binom_positive
  23. 0023exact hC
  24. 0024cases hp
  25. 0025apply PA1
  26. 0026trans C
  27. 0027symm
  28. 0028exact hp_witness
  29. 0029exact hz
  30. 0030intro p
  31. 0031intro hp
  32. 0032intro hd
  33. 0033specialize le_trans p
  34. 0034specialize le_trans (n + n)
  35. 0035specialize le_trans N
  36. 0036apply le_trans
  37. 0037specialize central_binom_prime_divisor_le_double n
  38. 0038specialize central_binom_prime_divisor_le_double C
  39. 0039specialize central_binom_prime_divisor_le_double p
  40. 0040apply central_binom_prime_divisor_le_double
  41. 0041exact hp
  42. 0042exact hC
  43. 0043exact hd
  44. 0044exact hN
  45. 0045cases hcomplete
  46. 0046cases hcomplete_witness
  47. 0047cases hcomplete_witness_left
  48. 0048cases hcomplete_witness_left_witness
  49. 0049cases hcomplete_witness_left_witness_witness
  50. 0050rewrite hcomplete_witness_right
  51. 0051specialize beta_product_bit_weighted_upper_power x3
  52. 0052specialize beta_product_bit_weighted_upper_power x4
  53. 0053specialize beta_product_bit_weighted_upper_power x
  54. 0054specialize beta_product_bit_weighted_upper_power x1
  55. 0055specialize beta_product_bit_weighted_upper_power (n + n)
  56. 0056specialize beta_product_bit_weighted_upper_power N
  57. 0057specialize beta_product_bit_weighted_upper_power x2
  58. 0058specialize beta_product_bit_weighted_upper_power k
  59. 0059specialize beta_product_bit_weighted_upper_power Q
  60. 0060apply beta_product_bit_weighted_upper_power
  61. 0061specialize central_binom_prime_mask_weighted_upper n
  62. 0062specialize central_binom_prime_mask_weighted_upper C
  63. 0063specialize central_binom_prime_mask_weighted_upper x3
  64. 0064specialize central_binom_prime_mask_weighted_upper x4
  65. 0065specialize central_binom_prime_mask_weighted_upper x
  66. 0066specialize central_binom_prime_mask_weighted_upper x1
  67. 0067specialize central_binom_prime_mask_weighted_upper N
  68. 0068apply central_binom_prime_mask_weighted_upper
  69. 0069exact hn
  70. 0070exact hC
  71. 0071exact hcomplete_witness_left_witness_witness_left
  72. 0072exact hk_witness_witness_left
  73. 0073exact hcomplete_witness_left_witness_witness_right
  74. 0074exact hk_witness_witness_right
  75. 0075exact hQ