BP0003

bertrand_window_central_valuation_at_most_one

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

Every central-binomial valuation at a Bertrand-window prime is at most one.

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 p C e. (exists bcf_lt_gap_bpc_index. bcf_lt_gap_bpc_index + S (1) = n) -> ((~(p = 1) /\ forall frm_prime_left_bpc_prime frm_prime_right_bpc_prime. p = frm_prime_left_bpc_prime * frm_prime_right_bpc_prime -> frm_prime_left_bpc_prime = 1 \/ frm_prime_right_bpc_prime = 1)) -> (exists bcf_lt_gap_bpc_lower. bcf_lt_gap_bpc_lower + S (n) = p) -> (((exists bcf_lt_gap_bpc_central_out_of_range. bcf_lt_gap_bpc_central_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_bpc_central_in_range. bcf_le_gap_bpc_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bpc_central bcf_row_code_scale_bpc_central bcf_row_scale_code_bpc_central bcf_row_scale_scale_bpc_central bcf_row_code_bpc_central bcf_row_scale_bpc_central. ((forall bcf_row_index_bpc_central_table. (exists bcf_lt_gap_bpc_central_table_row_bound. bcf_lt_gap_bpc_central_table_row_bound + S (bcf_row_index_bpc_central_table) = S (n + n)) -> exists bcf_row_code_bpc_central_table bcf_row_scale_bpc_central_table. ((((exists bcf_height_bpc_central_table_decoded_row_code. bcf_height_bpc_central_table_decoded_row_code + S (bcf_row_code_bpc_central_table) = S ((S (bcf_row_index_bpc_central_table)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_row_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_table_decoded_row_code * S ((S (bcf_row_index_bpc_central_table)) * bcf_row_code_scale_bpc_central) + (bcf_row_code_bpc_central_table))) /\ ((((exists bcf_height_bpc_central_table_decoded_row_scale. bcf_height_bpc_central_table_decoded_row_scale + S (bcf_row_scale_bpc_central_table) = S ((S (bcf_row_index_bpc_central_table)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_row_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_table_decoded_row_scale * S ((S (bcf_row_index_bpc_central_table)) * bcf_row_scale_scale_bpc_central) + (bcf_row_scale_bpc_central_table))) /\ ((bcf_row_index_bpc_central_table = 0 /\ (forall bcf_index_bpc_central_table_zero_row. (exists bcf_lt_gap_bpc_central_table_zero_row_bound. bcf_lt_gap_bpc_central_table_zero_row_bound + S (bcf_index_bpc_central_table_zero_row) = S (n + n)) -> exists bcf_value_bpc_central_table_zero_row. ((((exists bcf_height_bpc_central_table_zero_row_entry. bcf_height_bpc_central_table_zero_row_entry + S (bcf_value_bpc_central_table_zero_row) = S ((S (bcf_index_bpc_central_table_zero_row)) * bcf_row_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_zero_row_entry. bcf_row_code_bpc_central_table = bcf_quotient_bpc_central_table_zero_row_entry * S ((S (bcf_index_bpc_central_table_zero_row)) * bcf_row_scale_bpc_central_table) + (bcf_value_bpc_central_table_zero_row))) /\ ((bcf_index_bpc_central_table_zero_row = 0 /\ bcf_value_bpc_central_table_zero_row = 1) \/ exists bcf_predecessor_bpc_central_table_zero_row. bcf_index_bpc_central_table_zero_row = S bcf_predecessor_bpc_central_table_zero_row /\ bcf_value_bpc_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bpc_central_table bcf_previous_code_bpc_central_table bcf_previous_scale_bpc_central_table. bcf_row_index_bpc_central_table = S bcf_predecessor_bpc_central_table /\ ((((exists bcf_height_bpc_central_table_decoded_previous_code. bcf_height_bpc_central_table_decoded_previous_code + S (bcf_previous_code_bpc_central_table) = S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_previous_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_table_decoded_previous_code * S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_code_scale_bpc_central) + (bcf_previous_code_bpc_central_table))) /\ ((((exists bcf_height_bpc_central_table_decoded_previous_scale. bcf_height_bpc_central_table_decoded_previous_scale + S (bcf_previous_scale_bpc_central_table) = S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_table_decoded_previous_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bpc_central_table)) * bcf_row_scale_scale_bpc_central) + (bcf_previous_scale_bpc_central_table))) /\ (forall bcf_index_bpc_central_table_row_step. (exists bcf_lt_gap_bpc_central_table_row_step_bound. bcf_lt_gap_bpc_central_table_row_step_bound + S (bcf_index_bpc_central_table_row_step) = S (n + n)) -> exists bcf_value_bpc_central_table_row_step. ((((exists bcf_height_bpc_central_table_row_step_entry. bcf_height_bpc_central_table_row_step_entry + S (bcf_value_bpc_central_table_row_step) = S ((S (bcf_index_bpc_central_table_row_step)) * bcf_row_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_entry. bcf_row_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_entry * S ((S (bcf_index_bpc_central_table_row_step)) * bcf_row_scale_bpc_central_table) + (bcf_value_bpc_central_table_row_step))) /\ ((bcf_index_bpc_central_table_row_step = 0 /\ bcf_value_bpc_central_table_row_step = 1) \/ exists bcf_predecessor_bpc_central_table_row_step bcf_left_bpc_central_table_row_step bcf_right_bpc_central_table_row_step. bcf_index_bpc_central_table_row_step = S bcf_predecessor_bpc_central_table_row_step /\ ((((exists bcf_height_bpc_central_table_row_step_previous_left. bcf_height_bpc_central_table_row_step_previous_left + S (bcf_left_bpc_central_table_row_step) = S ((S (bcf_predecessor_bpc_central_table_row_step)) * bcf_previous_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_previous_left. bcf_previous_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_previous_left * S ((S (bcf_predecessor_bpc_central_table_row_step)) * bcf_previous_scale_bpc_central_table) + (bcf_left_bpc_central_table_row_step))) /\ ((((exists bcf_height_bpc_central_table_row_step_previous_right. bcf_height_bpc_central_table_row_step_previous_right + S (bcf_right_bpc_central_table_row_step) = S ((S (S (bcf_predecessor_bpc_central_table_row_step))) * bcf_previous_scale_bpc_central_table)) /\ exists bcf_quotient_bpc_central_table_row_step_previous_right. bcf_previous_code_bpc_central_table = bcf_quotient_bpc_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bpc_central_table_row_step))) * bcf_previous_scale_bpc_central_table) + (bcf_right_bpc_central_table_row_step))) /\ bcf_value_bpc_central_table_row_step = bcf_left_bpc_central_table_row_step + bcf_right_bpc_central_table_row_step))))))))))) /\ ((((exists bcf_height_bpc_central_decoded_row_code. bcf_height_bpc_central_decoded_row_code + S (bcf_row_code_bpc_central) = S ((S (n + n)) * bcf_row_code_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_row_code. bcf_row_code_code_bpc_central = bcf_quotient_bpc_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bpc_central) + (bcf_row_code_bpc_central))) /\ ((((exists bcf_height_bpc_central_decoded_row_scale. bcf_height_bpc_central_decoded_row_scale + S (bcf_row_scale_bpc_central) = S ((S (n + n)) * bcf_row_scale_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_row_scale. bcf_row_scale_code_bpc_central = bcf_quotient_bpc_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bpc_central) + (bcf_row_scale_bpc_central))) /\ (((exists bcf_height_bpc_central_decoded_value. bcf_height_bpc_central_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_bpc_central)) /\ exists bcf_quotient_bpc_central_decoded_value. bcf_row_code_bpc_central = bcf_quotient_bpc_central_decoded_value * S ((S (n)) * bcf_row_scale_bpc_central) + (C))))))))) -> (((exists bpv_gap_bpc_value_exponent_bound. bpv_gap_bpc_value_exponent_bound + e = C) /\ (exists bpv_result_bpc_value_selected. ((exists ff_b_bpc_value_selected_power ff_c_bpc_value_selected_power. ((forall ff_i_bpc_value_selected_power_repeat. (exists ff_lt_bpc_value_selected_power_repeat_bound. ff_lt_bpc_value_selected_power_repeat_bound + S ff_i_bpc_value_selected_power_repeat = e) -> (((exists ff_h_bpc_value_selected_power_repeat_decoded. ff_h_bpc_value_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bpc_value_selected_power_repeat)) * ff_c_bpc_value_selected_power)) /\ exists ff_q_bpc_value_selected_power_repeat_decoded. ff_b_bpc_value_selected_power = ff_q_bpc_value_selected_power_repeat_decoded * S ((S (ff_i_bpc_value_selected_power_repeat)) * ff_c_bpc_value_selected_power) + (p)))) /\ (exists ff_u_bpc_value_selected_power_product ff_v_bpc_value_selected_power_product. ((((exists ff_h_bpc_value_selected_power_product_start. ff_h_bpc_value_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_start. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_start * S ((S (0)) * ff_v_bpc_value_selected_power_product) + (1))) /\ ((((exists ff_h_bpc_value_selected_power_product_terminal. ff_h_bpc_value_selected_power_product_terminal + S (bpv_result_bpc_value_selected) = S ((S (e)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_terminal. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_terminal * S ((S (e)) * ff_v_bpc_value_selected_power_product) + (bpv_result_bpc_value_selected))) /\ forall ff_i_bpc_value_selected_power_product. (exists ff_lt_bpc_value_selected_power_product_bound. ff_lt_bpc_value_selected_power_product_bound + S ff_i_bpc_value_selected_power_product = e) -> exists ff_p_bpc_value_selected_power_product ff_r_bpc_value_selected_power_product ff_s_bpc_value_selected_power_product. ((((exists ff_h_bpc_value_selected_power_product_factor. ff_h_bpc_value_selected_power_product_factor + S (ff_p_bpc_value_selected_power_product) = S ((S (ff_i_bpc_value_selected_power_product)) * ff_c_bpc_value_selected_power)) /\ exists ff_q_bpc_value_selected_power_product_factor. ff_b_bpc_value_selected_power = ff_q_bpc_value_selected_power_product_factor * S ((S (ff_i_bpc_value_selected_power_product)) * ff_c_bpc_value_selected_power) + (ff_p_bpc_value_selected_power_product))) /\ ((((exists ff_h_bpc_value_selected_power_product_partial. ff_h_bpc_value_selected_power_product_partial + S (ff_r_bpc_value_selected_power_product) = S ((S (ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_partial. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_partial * S ((S (ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product) + (ff_r_bpc_value_selected_power_product))) /\ ((((exists ff_h_bpc_value_selected_power_product_successor. ff_h_bpc_value_selected_power_product_successor + S (ff_s_bpc_value_selected_power_product) = S ((S (S ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product)) /\ exists ff_q_bpc_value_selected_power_product_successor. ff_u_bpc_value_selected_power_product = ff_q_bpc_value_selected_power_product_successor * S ((S (S ff_i_bpc_value_selected_power_product)) * ff_v_bpc_value_selected_power_product) + (ff_s_bpc_value_selected_power_product))) /\ ff_s_bpc_value_selected_power_product = ff_r_bpc_value_selected_power_product * ff_p_bpc_value_selected_power_product)))))))) /\ (exists bpv_factor_bpc_value_selected_divides. C = bpv_result_bpc_value_selected * bpv_factor_bpc_value_selected_divides)))) /\ forall bpv_candidate_bpc_value. (exists bpv_gap_bpc_value_candidate_bound. bpv_gap_bpc_value_candidate_bound + bpv_candidate_bpc_value = C) -> (exists bpv_result_bpc_value_candidate. ((exists ff_b_bpc_value_candidate_power ff_c_bpc_value_candidate_power. ((forall ff_i_bpc_value_candidate_power_repeat. (exists ff_lt_bpc_value_candidate_power_repeat_bound. ff_lt_bpc_value_candidate_power_repeat_bound + S ff_i_bpc_value_candidate_power_repeat = bpv_candidate_bpc_value) -> (((exists ff_h_bpc_value_candidate_power_repeat_decoded. ff_h_bpc_value_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bpc_value_candidate_power_repeat)) * ff_c_bpc_value_candidate_power)) /\ exists ff_q_bpc_value_candidate_power_repeat_decoded. ff_b_bpc_value_candidate_power = ff_q_bpc_value_candidate_power_repeat_decoded * S ((S (ff_i_bpc_value_candidate_power_repeat)) * ff_c_bpc_value_candidate_power) + (p)))) /\ (exists ff_u_bpc_value_candidate_power_product ff_v_bpc_value_candidate_power_product. ((((exists ff_h_bpc_value_candidate_power_product_start. ff_h_bpc_value_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_start. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_start * S ((S (0)) * ff_v_bpc_value_candidate_power_product) + (1))) /\ ((((exists ff_h_bpc_value_candidate_power_product_terminal. ff_h_bpc_value_candidate_power_product_terminal + S (bpv_result_bpc_value_candidate) = S ((S (bpv_candidate_bpc_value)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_terminal. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_terminal * S ((S (bpv_candidate_bpc_value)) * ff_v_bpc_value_candidate_power_product) + (bpv_result_bpc_value_candidate))) /\ forall ff_i_bpc_value_candidate_power_product. (exists ff_lt_bpc_value_candidate_power_product_bound. ff_lt_bpc_value_candidate_power_product_bound + S ff_i_bpc_value_candidate_power_product = bpv_candidate_bpc_value) -> exists ff_p_bpc_value_candidate_power_product ff_r_bpc_value_candidate_power_product ff_s_bpc_value_candidate_power_product. ((((exists ff_h_bpc_value_candidate_power_product_factor. ff_h_bpc_value_candidate_power_product_factor + S (ff_p_bpc_value_candidate_power_product) = S ((S (ff_i_bpc_value_candidate_power_product)) * ff_c_bpc_value_candidate_power)) /\ exists ff_q_bpc_value_candidate_power_product_factor. ff_b_bpc_value_candidate_power = ff_q_bpc_value_candidate_power_product_factor * S ((S (ff_i_bpc_value_candidate_power_product)) * ff_c_bpc_value_candidate_power) + (ff_p_bpc_value_candidate_power_product))) /\ ((((exists ff_h_bpc_value_candidate_power_product_partial. ff_h_bpc_value_candidate_power_product_partial + S (ff_r_bpc_value_candidate_power_product) = S ((S (ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_partial. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_partial * S ((S (ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product) + (ff_r_bpc_value_candidate_power_product))) /\ ((((exists ff_h_bpc_value_candidate_power_product_successor. ff_h_bpc_value_candidate_power_product_successor + S (ff_s_bpc_value_candidate_power_product) = S ((S (S ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product)) /\ exists ff_q_bpc_value_candidate_power_product_successor. ff_u_bpc_value_candidate_power_product = ff_q_bpc_value_candidate_power_product_successor * S ((S (S ff_i_bpc_value_candidate_power_product)) * ff_v_bpc_value_candidate_power_product) + (ff_s_bpc_value_candidate_power_product))) /\ ff_s_bpc_value_candidate_power_product = ff_r_bpc_value_candidate_power_product * ff_p_bpc_value_candidate_power_product)))))))) /\ (exists bpv_factor_bpc_value_candidate_divides. C = bpv_result_bpc_value_candidate * bpv_factor_bpc_value_candidate_divides))) -> (exists bpv_gap_bpc_value_maximal. bpv_gap_bpc_value_maximal + bpv_candidate_bpc_value = e)) -> (exists bcf_le_gap_bpc_e_one. bcf_le_gap_bpc_e_one + (e) = 1)

Constructive proof overview

Generated structural guide

Every central-binomial valuation at a Bertrand-window prime is at most one.

The unchanged tactic script uses 5 declared prerequisites and contains 45 exact native proof lines.

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

Proof neighborhood

Direct dependencies

lt_to_le Stable theorem; checked-use authorized pow_exists Stable theorem; checked-use authorized pow_two Stable theorem; checked-use authorized BP0002 bertrand_window_prime_square_exceeds_double central_binom_prime_square_tail_valuation_le_one Alpha theorem; checked-use authorized

Direct dependents

BP0005 bertrand_window_central_valuation_equals_one

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

45 script commands · 7 reading checkpoints · 4 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 (1)
bertrand window prime square exceeds double

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

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

  1. L1
    intro n
  2. L2
    intro p
  3. L3
    intro C
  4. L4
    intro e
  5. L5
    intro hindex
  6. L6
    intro hprime
  7. L7
    intro hlower
  8. L8
    intro hcentral
  9. L9
    intro hvaluation
02Establish hpowerL10–13

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have hpower : ∃ s. Pow(p,2,s)Definitions: Pow
  2. L11
    specialize pow_exists p
  3. L12
    specialize pow_exists 2
  4. L13
    exact pow_exists
03Separate the logical casesL14–14

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

  1. L14
    cases hpower
04Establish hvalueL15–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two.

  1. L15
    have hvalue : x = p * p
  2. L16
    specialize pow_two p
  3. L17
    specialize pow_two 2
  4. L18
    specialize pow_two x
  5. L19
    apply pow_two
  6. L20
    refl
  7. L21
    exact hpower_witness
05Establish hsquareL22–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand window prime square exceeds double.

  1. L22
    have hsquare : exists bcf_lt_gap_bpc_square. bcf_lt_gap_bpc_square + S (n + n) = p * p
  2. L23
    specialize bertrand_window_prime_square_exceeds_double n
  3. L24
    specialize bertrand_window_prime_square_exceeds_double p
  4. L25
    apply bertrand_window_prime_square_exceeds_double
  5. L26
    exact hprime
  6. L27
    exact hlower
06Establish hstrictL28–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom prime square tail valuation le one.

  1. L28
    have hstrict : exists q. q + S (n + n) = x
  2. L29
    rewrite hvalue
  3. L30
    exact hsquare
  4. L31
    specialize central_binom_prime_square_tail_valuation_le_one p
  5. L32
    specialize central_binom_prime_square_tail_valuation_le_one n
  6. L33
    specialize central_binom_prime_square_tail_valuation_le_one C
  7. L34
    specialize central_binom_prime_square_tail_valuation_le_one e
  8. L35
    specialize central_binom_prime_square_tail_valuation_le_one x
  9. L36
    apply central_binom_prime_square_tail_valuation_le_one
  10. L37
    exact hprime
07Use earlier factsL38–45

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

  1. L38
    specialize lt_to_le 1
  2. L39
    specialize lt_to_le n
  3. L40
    apply lt_to_le
  4. L41
    exact hindex
  5. L42
    exact hcentral
  6. L43
    exact hvaluation
  7. L44
    exact hpower_witness
  8. L45
    exact hstrict

Library-wide reading audit

Original exact command ledger · 45 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro C
  4. 0004intro e
  5. 0005intro hindex
  6. 0006intro hprime
  7. 0007intro hlower
  8. 0008intro hcentral
  9. 0009intro hvaluation
  10. 0010have hpower : exists s. (exists bpvi_b_bpc_square_power bpvi_c_bpc_square_power. ((forall bpvi_i_bpc_square_power. (exists bpvi_repeat_gap_bpc_square_power. bpvi_repeat_gap_bpc_square_power + S bpvi_i_bpc_square_power = 2) -> (((exists bpvi_h_bpc_square_power_repeat. bpvi_h_bpc_square_power_repeat + S (p) = S ((S (bpvi_i_bpc_square_power)) * bpvi_c_bpc_square_power)) /\ exists bpvi_q_bpc_square_power_repeat. bpvi_b_bpc_square_power = bpvi_q_bpc_square_power_repeat * S ((S (bpvi_i_bpc_square_power)) * bpvi_c_bpc_square_power) + (p)))) /\ (exists bpvi_u_bpc_square_power bpvi_v_bpc_square_power. ((((exists bpvi_h_bpc_square_power_start. bpvi_h_bpc_square_power_start + S (1) = S ((S (0)) * bpvi_v_bpc_square_power)) /\ exists bpvi_q_bpc_square_power_start. bpvi_u_bpc_square_power = bpvi_q_bpc_square_power_start * S ((S (0)) * bpvi_v_bpc_square_power) + (1))) /\ ((((exists bpvi_h_bpc_square_power_terminal. bpvi_h_bpc_square_power_terminal + S (s) = S ((S (2)) * bpvi_v_bpc_square_power)) /\ exists bpvi_q_bpc_square_power_terminal. bpvi_u_bpc_square_power = bpvi_q_bpc_square_power_terminal * S ((S (2)) * bpvi_v_bpc_square_power) + (s))) /\ forall bpvi_j_bpc_square_power. (exists bpvi_product_gap_bpc_square_power. bpvi_product_gap_bpc_square_power + S bpvi_j_bpc_square_power = 2) -> exists bpvi_factor_bpc_square_power bpvi_partial_bpc_square_power bpvi_successor_bpc_square_power. ((((exists bpvi_h_bpc_square_power_factor. bpvi_h_bpc_square_power_factor + S (bpvi_factor_bpc_square_power) = S ((S (bpvi_j_bpc_square_power)) * bpvi_c_bpc_square_power)) /\ exists bpvi_q_bpc_square_power_factor. bpvi_b_bpc_square_power = bpvi_q_bpc_square_power_factor * S ((S (bpvi_j_bpc_square_power)) * bpvi_c_bpc_square_power) + (bpvi_factor_bpc_square_power))) /\ ((((exists bpvi_h_bpc_square_power_partial. bpvi_h_bpc_square_power_partial + S (bpvi_partial_bpc_square_power) = S ((S (bpvi_j_bpc_square_power)) * bpvi_v_bpc_square_power)) /\ exists bpvi_q_bpc_square_power_partial. bpvi_u_bpc_square_power = bpvi_q_bpc_square_power_partial * S ((S (bpvi_j_bpc_square_power)) * bpvi_v_bpc_square_power) + (bpvi_partial_bpc_square_power))) /\ ((((exists bpvi_h_bpc_square_power_successor. bpvi_h_bpc_square_power_successor + S (bpvi_successor_bpc_square_power) = S ((S (S bpvi_j_bpc_square_power)) * bpvi_v_bpc_square_power)) /\ exists bpvi_q_bpc_square_power_successor. bpvi_u_bpc_square_power = bpvi_q_bpc_square_power_successor * S ((S (S bpvi_j_bpc_square_power)) * bpvi_v_bpc_square_power) + (bpvi_successor_bpc_square_power))) /\ bpvi_successor_bpc_square_power = bpvi_partial_bpc_square_power * bpvi_factor_bpc_square_power))))))))
  11. 0011specialize pow_exists p
  12. 0012specialize pow_exists 2
  13. 0013exact pow_exists
  14. 0014cases hpower
  15. 0015have hvalue : x = p * p
  16. 0016specialize pow_two p
  17. 0017specialize pow_two 2
  18. 0018specialize pow_two x
  19. 0019apply pow_two
  20. 0020refl
  21. 0021exact hpower_witness
  22. 0022have hsquare : exists bcf_lt_gap_bpc_square. bcf_lt_gap_bpc_square + S (n + n) = p * p
  23. 0023specialize bertrand_window_prime_square_exceeds_double n
  24. 0024specialize bertrand_window_prime_square_exceeds_double p
  25. 0025apply bertrand_window_prime_square_exceeds_double
  26. 0026exact hprime
  27. 0027exact hlower
  28. 0028have hstrict : exists q. q + S (n + n) = x
  29. 0029rewrite hvalue
  30. 0030exact hsquare
  31. 0031specialize central_binom_prime_square_tail_valuation_le_one p
  32. 0032specialize central_binom_prime_square_tail_valuation_le_one n
  33. 0033specialize central_binom_prime_square_tail_valuation_le_one C
  34. 0034specialize central_binom_prime_square_tail_valuation_le_one e
  35. 0035specialize central_binom_prime_square_tail_valuation_le_one x
  36. 0036apply central_binom_prime_square_tail_valuation_le_one
  37. 0037exact hprime
  38. 0038specialize lt_to_le 1
  39. 0039specialize lt_to_le n
  40. 0040apply lt_to_le
  41. 0041exact hindex
  42. 0042exact hcentral
  43. 0043exact hvaluation
  44. 0044exact hpower_witness
  45. 0045exact hstrict