PC0019

central_binom_dominates_pow_two

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

For n at least four, the central binomial coefficient dominates the actual 2^n value.

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 C v. (exists pc_le_central_lower_bound. pc_le_central_lower_bound + (4) = (n)) -> (((exists bcf_lt_gap_pc_central_lower_value_out_of_range. bcf_lt_gap_pc_central_lower_value_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_pc_central_lower_value_in_range. bcf_le_gap_pc_central_lower_value_in_range + (n) = n + n) /\ (exists bcf_row_code_code_pc_central_lower_value bcf_row_code_scale_pc_central_lower_value bcf_row_scale_code_pc_central_lower_value bcf_row_scale_scale_pc_central_lower_value bcf_row_code_pc_central_lower_value bcf_row_scale_pc_central_lower_value. ((forall bcf_row_index_pc_central_lower_value_table. (exists bcf_lt_gap_pc_central_lower_value_table_row_bound. bcf_lt_gap_pc_central_lower_value_table_row_bound + S (bcf_row_index_pc_central_lower_value_table) = S (n + n)) -> exists bcf_row_code_pc_central_lower_value_table bcf_row_scale_pc_central_lower_value_table. ((((exists bcf_height_pc_central_lower_value_table_decoded_row_code. bcf_height_pc_central_lower_value_table_decoded_row_code + S (bcf_row_code_pc_central_lower_value_table) = S ((S (bcf_row_index_pc_central_lower_value_table)) * bcf_row_code_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_table_decoded_row_code. bcf_row_code_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_table_decoded_row_code * S ((S (bcf_row_index_pc_central_lower_value_table)) * bcf_row_code_scale_pc_central_lower_value) + (bcf_row_code_pc_central_lower_value_table))) /\ ((((exists bcf_height_pc_central_lower_value_table_decoded_row_scale. bcf_height_pc_central_lower_value_table_decoded_row_scale + S (bcf_row_scale_pc_central_lower_value_table) = S ((S (bcf_row_index_pc_central_lower_value_table)) * bcf_row_scale_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_table_decoded_row_scale. bcf_row_scale_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_table_decoded_row_scale * S ((S (bcf_row_index_pc_central_lower_value_table)) * bcf_row_scale_scale_pc_central_lower_value) + (bcf_row_scale_pc_central_lower_value_table))) /\ ((bcf_row_index_pc_central_lower_value_table = 0 /\ (forall bcf_index_pc_central_lower_value_table_zero_row. (exists bcf_lt_gap_pc_central_lower_value_table_zero_row_bound. bcf_lt_gap_pc_central_lower_value_table_zero_row_bound + S (bcf_index_pc_central_lower_value_table_zero_row) = S (n + n)) -> exists bcf_value_pc_central_lower_value_table_zero_row. ((((exists bcf_height_pc_central_lower_value_table_zero_row_entry. bcf_height_pc_central_lower_value_table_zero_row_entry + S (bcf_value_pc_central_lower_value_table_zero_row) = S ((S (bcf_index_pc_central_lower_value_table_zero_row)) * bcf_row_scale_pc_central_lower_value_table)) /\ exists bcf_quotient_pc_central_lower_value_table_zero_row_entry. bcf_row_code_pc_central_lower_value_table = bcf_quotient_pc_central_lower_value_table_zero_row_entry * S ((S (bcf_index_pc_central_lower_value_table_zero_row)) * bcf_row_scale_pc_central_lower_value_table) + (bcf_value_pc_central_lower_value_table_zero_row))) /\ ((bcf_index_pc_central_lower_value_table_zero_row = 0 /\ bcf_value_pc_central_lower_value_table_zero_row = 1) \/ exists bcf_predecessor_pc_central_lower_value_table_zero_row. bcf_index_pc_central_lower_value_table_zero_row = S bcf_predecessor_pc_central_lower_value_table_zero_row /\ bcf_value_pc_central_lower_value_table_zero_row = 0)))) \/ exists bcf_predecessor_pc_central_lower_value_table bcf_previous_code_pc_central_lower_value_table bcf_previous_scale_pc_central_lower_value_table. bcf_row_index_pc_central_lower_value_table = S bcf_predecessor_pc_central_lower_value_table /\ ((((exists bcf_height_pc_central_lower_value_table_decoded_previous_code. bcf_height_pc_central_lower_value_table_decoded_previous_code + S (bcf_previous_code_pc_central_lower_value_table) = S ((S (bcf_predecessor_pc_central_lower_value_table)) * bcf_row_code_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_table_decoded_previous_code. bcf_row_code_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_table_decoded_previous_code * S ((S (bcf_predecessor_pc_central_lower_value_table)) * bcf_row_code_scale_pc_central_lower_value) + (bcf_previous_code_pc_central_lower_value_table))) /\ ((((exists bcf_height_pc_central_lower_value_table_decoded_previous_scale. bcf_height_pc_central_lower_value_table_decoded_previous_scale + S (bcf_previous_scale_pc_central_lower_value_table) = S ((S (bcf_predecessor_pc_central_lower_value_table)) * bcf_row_scale_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_table_decoded_previous_scale. bcf_row_scale_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_table_decoded_previous_scale * S ((S (bcf_predecessor_pc_central_lower_value_table)) * bcf_row_scale_scale_pc_central_lower_value) + (bcf_previous_scale_pc_central_lower_value_table))) /\ (forall bcf_index_pc_central_lower_value_table_row_step. (exists bcf_lt_gap_pc_central_lower_value_table_row_step_bound. bcf_lt_gap_pc_central_lower_value_table_row_step_bound + S (bcf_index_pc_central_lower_value_table_row_step) = S (n + n)) -> exists bcf_value_pc_central_lower_value_table_row_step. ((((exists bcf_height_pc_central_lower_value_table_row_step_entry. bcf_height_pc_central_lower_value_table_row_step_entry + S (bcf_value_pc_central_lower_value_table_row_step) = S ((S (bcf_index_pc_central_lower_value_table_row_step)) * bcf_row_scale_pc_central_lower_value_table)) /\ exists bcf_quotient_pc_central_lower_value_table_row_step_entry. bcf_row_code_pc_central_lower_value_table = bcf_quotient_pc_central_lower_value_table_row_step_entry * S ((S (bcf_index_pc_central_lower_value_table_row_step)) * bcf_row_scale_pc_central_lower_value_table) + (bcf_value_pc_central_lower_value_table_row_step))) /\ ((bcf_index_pc_central_lower_value_table_row_step = 0 /\ bcf_value_pc_central_lower_value_table_row_step = 1) \/ exists bcf_predecessor_pc_central_lower_value_table_row_step bcf_left_pc_central_lower_value_table_row_step bcf_right_pc_central_lower_value_table_row_step. bcf_index_pc_central_lower_value_table_row_step = S bcf_predecessor_pc_central_lower_value_table_row_step /\ ((((exists bcf_height_pc_central_lower_value_table_row_step_previous_left. bcf_height_pc_central_lower_value_table_row_step_previous_left + S (bcf_left_pc_central_lower_value_table_row_step) = S ((S (bcf_predecessor_pc_central_lower_value_table_row_step)) * bcf_previous_scale_pc_central_lower_value_table)) /\ exists bcf_quotient_pc_central_lower_value_table_row_step_previous_left. bcf_previous_code_pc_central_lower_value_table = bcf_quotient_pc_central_lower_value_table_row_step_previous_left * S ((S (bcf_predecessor_pc_central_lower_value_table_row_step)) * bcf_previous_scale_pc_central_lower_value_table) + (bcf_left_pc_central_lower_value_table_row_step))) /\ ((((exists bcf_height_pc_central_lower_value_table_row_step_previous_right. bcf_height_pc_central_lower_value_table_row_step_previous_right + S (bcf_right_pc_central_lower_value_table_row_step) = S ((S (S (bcf_predecessor_pc_central_lower_value_table_row_step))) * bcf_previous_scale_pc_central_lower_value_table)) /\ exists bcf_quotient_pc_central_lower_value_table_row_step_previous_right. bcf_previous_code_pc_central_lower_value_table = bcf_quotient_pc_central_lower_value_table_row_step_previous_right * S ((S (S (bcf_predecessor_pc_central_lower_value_table_row_step))) * bcf_previous_scale_pc_central_lower_value_table) + (bcf_right_pc_central_lower_value_table_row_step))) /\ bcf_value_pc_central_lower_value_table_row_step = bcf_left_pc_central_lower_value_table_row_step + bcf_right_pc_central_lower_value_table_row_step))))))))))) /\ ((((exists bcf_height_pc_central_lower_value_decoded_row_code. bcf_height_pc_central_lower_value_decoded_row_code + S (bcf_row_code_pc_central_lower_value) = S ((S (n + n)) * bcf_row_code_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_decoded_row_code. bcf_row_code_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_pc_central_lower_value) + (bcf_row_code_pc_central_lower_value))) /\ ((((exists bcf_height_pc_central_lower_value_decoded_row_scale. bcf_height_pc_central_lower_value_decoded_row_scale + S (bcf_row_scale_pc_central_lower_value) = S ((S (n + n)) * bcf_row_scale_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_decoded_row_scale. bcf_row_scale_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_pc_central_lower_value) + (bcf_row_scale_pc_central_lower_value))) /\ (((exists bcf_height_pc_central_lower_value_decoded_value. bcf_height_pc_central_lower_value_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_pc_central_lower_value)) /\ exists bcf_quotient_pc_central_lower_value_decoded_value. bcf_row_code_pc_central_lower_value = bcf_quotient_pc_central_lower_value_decoded_value * S ((S (n)) * bcf_row_scale_pc_central_lower_value) + (C))))))))) -> (exists pa_b_pc_central_lower_power pa_c_pc_central_lower_power. ((forall pa_i_pc_central_lower_power_repeat. (exists pa_lt_pc_central_lower_power_repeat_bound. pa_lt_pc_central_lower_power_repeat_bound + S pa_i_pc_central_lower_power_repeat = n) -> (((exists pa_h_pc_central_lower_power_repeat_decoded. pa_h_pc_central_lower_power_repeat_decoded + S (2) = S ((S (pa_i_pc_central_lower_power_repeat)) * pa_c_pc_central_lower_power)) /\ exists pa_q_pc_central_lower_power_repeat_decoded. pa_b_pc_central_lower_power = pa_q_pc_central_lower_power_repeat_decoded * S ((S (pa_i_pc_central_lower_power_repeat)) * pa_c_pc_central_lower_power) + (2)))) /\ (exists pa_u_pc_central_lower_power_product pa_v_pc_central_lower_power_product. ((((exists pa_h_pc_central_lower_power_product_start. pa_h_pc_central_lower_power_product_start + S (1) = S ((S (0)) * pa_v_pc_central_lower_power_product)) /\ exists pa_q_pc_central_lower_power_product_start. pa_u_pc_central_lower_power_product = pa_q_pc_central_lower_power_product_start * S ((S (0)) * pa_v_pc_central_lower_power_product) + (1))) /\ ((((exists pa_h_pc_central_lower_power_product_terminal. pa_h_pc_central_lower_power_product_terminal + S (v) = S ((S (n)) * pa_v_pc_central_lower_power_product)) /\ exists pa_q_pc_central_lower_power_product_terminal. pa_u_pc_central_lower_power_product = pa_q_pc_central_lower_power_product_terminal * S ((S (n)) * pa_v_pc_central_lower_power_product) + (v))) /\ forall pa_i_pc_central_lower_power_product. (exists pa_lt_pc_central_lower_power_product_bound. pa_lt_pc_central_lower_power_product_bound + S pa_i_pc_central_lower_power_product = n) -> exists pa_p_pc_central_lower_power_product pa_r_pc_central_lower_power_product pa_s_pc_central_lower_power_product. ((((exists pa_h_pc_central_lower_power_product_factor. pa_h_pc_central_lower_power_product_factor + S (pa_p_pc_central_lower_power_product) = S ((S (pa_i_pc_central_lower_power_product)) * pa_c_pc_central_lower_power)) /\ exists pa_q_pc_central_lower_power_product_factor. pa_b_pc_central_lower_power = pa_q_pc_central_lower_power_product_factor * S ((S (pa_i_pc_central_lower_power_product)) * pa_c_pc_central_lower_power) + (pa_p_pc_central_lower_power_product))) /\ ((((exists pa_h_pc_central_lower_power_product_partial. pa_h_pc_central_lower_power_product_partial + S (pa_r_pc_central_lower_power_product) = S ((S (pa_i_pc_central_lower_power_product)) * pa_v_pc_central_lower_power_product)) /\ exists pa_q_pc_central_lower_power_product_partial. pa_u_pc_central_lower_power_product = pa_q_pc_central_lower_power_product_partial * S ((S (pa_i_pc_central_lower_power_product)) * pa_v_pc_central_lower_power_product) + (pa_r_pc_central_lower_power_product))) /\ ((((exists pa_h_pc_central_lower_power_product_successor. pa_h_pc_central_lower_power_product_successor + S (pa_s_pc_central_lower_power_product) = S ((S (S pa_i_pc_central_lower_power_product)) * pa_v_pc_central_lower_power_product)) /\ exists pa_q_pc_central_lower_power_product_successor. pa_u_pc_central_lower_power_product = pa_q_pc_central_lower_power_product_successor * S ((S (S pa_i_pc_central_lower_power_product)) * pa_v_pc_central_lower_power_product) + (pa_s_pc_central_lower_power_product))) /\ pa_s_pc_central_lower_power_product = pa_r_pc_central_lower_power_product * pa_p_pc_central_lower_power_product)))))))) -> (exists pc_le_central_lower_result. pc_le_central_lower_result + (v) = (C))

Constructive proof overview

Generated structural guide

For n at least four, the central binomial coefficient dominates the actual 2^n value.

The unchanged tactic script uses 9 declared prerequisites and contains 65 exact native proof lines.

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

Proof neighborhood

Direct dependencies

pow_exists Stable theorem; checked-use authorized PC0018 pow_four_is_square_of_pow_two four_pow_lt_mul_central_binom Alpha theorem; checked-use authorized PC0015 binary_power_two_dominates_successor lt_to_le Stable theorem; checked-use authorized mul_le_mul_right Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized mul_le_cancel_left_nonzero Alpha theorem; checked-use authorized pow_nonzero_of_one_le Alpha theorem; checked-use authorized

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

65 script commands · 15 reading checkpoints · 6 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)
pow four is square of pow twobinary power two dominates successor

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

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

  1. L1
    intro n
  2. L2
    intro C
  3. L3
    intro v
  4. L4
    intro hn
  5. L5
    intro hC
  6. L6
    intro hv
02Establish hwL7–10

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

  1. L7
    have hw : ∃ w. Pow(4,n,w)Definitions: Pow
  2. L8
    specialize pow_exists 4
  3. L9
    specialize pow_exists n
  4. L10
    apply pow_exists
03Separate the logical casesL11–11

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

  1. L11
    cases hw
04Establish hsquareL12–18

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

  1. L12
    have hsquare : x = v * v
  2. L13
    specialize pow_four_is_square_of_pow_two n
  3. L14
    specialize pow_four_is_square_of_pow_two v
  4. L15
    specialize pow_four_is_square_of_pow_two x
  5. L16
    apply pow_four_is_square_of_pow_two
  6. L17
    exact hv
  7. L18
    exact hw_witness
05Establish hlowerL19–26

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

  1. L19
    have hlower : exists g. g + S x = n * C
  2. L20
    specialize four_pow_lt_mul_central_binom n
  3. L21
    specialize four_pow_lt_mul_central_binom x
  4. L22
    specialize four_pow_lt_mul_central_binom C
  5. L23
    apply four_pow_lt_mul_central_binom
  6. L24
    exact hn
  7. L25
    exact hw_witness
  8. L26
    exact hC
06Establish hnsmallL27–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.

  1. L27
    have hnsmall : exists g. g + n = v
  2. L28
    specialize lt_to_le n
  3. L29
    specialize lt_to_le v
  4. L30
    apply lt_to_le
  5. L31
    specialize binary_power_two_dominates_successor n
  6. L32
    specialize binary_power_two_dominates_successor v
  7. L33
    apply binary_power_two_dominates_successor
  8. L34
    exact hv
07Establish hscaleL35–40

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul right.

  1. L35
    have hscale : exists g. g + n * C = v * C
  2. L36
    specialize mul_le_mul_right n
  3. L37
    specialize mul_le_mul_right v
  4. L38
    specialize mul_le_mul_right C
  5. L39
    apply mul_le_mul_right
  6. L40
    exact hnsmall
08Establish hfullL41–50

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

  1. L41
    have hfull : exists g. g + x = v * C
  2. L42
    specialize le_trans x
  3. L43
    specialize le_trans (n * C)
  4. L44
    specialize le_trans (v * C)
  5. L45
    apply le_trans
  6. L46
    specialize lt_to_le x
  7. L47
    specialize lt_to_le (n * C)
  8. L48
    apply lt_to_le
  9. L49
    exact hlower
  10. L50
    exact hscale
09Calculate and transport equalitiesL51–51

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

  1. L51
    rewrite hsquare at hfull
10Use earlier factsL52–55

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

  1. L52
    specialize mul_le_cancel_left_nonzero v
  2. L53
    specialize mul_le_cancel_left_nonzero v
  3. L54
    specialize mul_le_cancel_left_nonzero C
  4. L55
    apply mul_le_cancel_left_nonzero
11Fix variables and assumptionsL56–56

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

  1. L56
    intro hz
12Use earlier factsL57–60

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

  1. L57
    specialize pow_nonzero_of_one_le 2
  2. L58
    specialize pow_nonzero_of_one_le n
  3. L59
    specialize pow_nonzero_of_one_le v
  4. L60
    apply pow_nonzero_of_one_le
13Construct an explicit witnessL61–61

Supply the displayed value, then prove that it has the required property.

  1. L61
    exists 1
14Calculate and transport equalitiesL62–62

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

  1. L62
    norm_num
15Use earlier factsL63–65

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

  1. L63
    exact hv
  2. L64
    exact hz
  3. L65
    exact hfull

Library-wide reading audit

Original exact command ledger · 65 lines
  1. 0001intro n
  2. 0002intro C
  3. 0003intro v
  4. 0004intro hn
  5. 0005intro hC
  6. 0006intro hv
  7. 0007have hw : exists w. exists pa_b_pc_central_lower_four pa_c_pc_central_lower_four. ((forall pa_i_pc_central_lower_four_repeat. (exists pa_lt_pc_central_lower_four_repeat_bound. pa_lt_pc_central_lower_four_repeat_bound + S pa_i_pc_central_lower_four_repeat = n) -> (((exists pa_h_pc_central_lower_four_repeat_decoded. pa_h_pc_central_lower_four_repeat_decoded + S (4) = S ((S (pa_i_pc_central_lower_four_repeat)) * pa_c_pc_central_lower_four)) /\ exists pa_q_pc_central_lower_four_repeat_decoded. pa_b_pc_central_lower_four = pa_q_pc_central_lower_four_repeat_decoded * S ((S (pa_i_pc_central_lower_four_repeat)) * pa_c_pc_central_lower_four) + (4)))) /\ (exists pa_u_pc_central_lower_four_product pa_v_pc_central_lower_four_product. ((((exists pa_h_pc_central_lower_four_product_start. pa_h_pc_central_lower_four_product_start + S (1) = S ((S (0)) * pa_v_pc_central_lower_four_product)) /\ exists pa_q_pc_central_lower_four_product_start. pa_u_pc_central_lower_four_product = pa_q_pc_central_lower_four_product_start * S ((S (0)) * pa_v_pc_central_lower_four_product) + (1))) /\ ((((exists pa_h_pc_central_lower_four_product_terminal. pa_h_pc_central_lower_four_product_terminal + S (w) = S ((S (n)) * pa_v_pc_central_lower_four_product)) /\ exists pa_q_pc_central_lower_four_product_terminal. pa_u_pc_central_lower_four_product = pa_q_pc_central_lower_four_product_terminal * S ((S (n)) * pa_v_pc_central_lower_four_product) + (w))) /\ forall pa_i_pc_central_lower_four_product. (exists pa_lt_pc_central_lower_four_product_bound. pa_lt_pc_central_lower_four_product_bound + S pa_i_pc_central_lower_four_product = n) -> exists pa_p_pc_central_lower_four_product pa_r_pc_central_lower_four_product pa_s_pc_central_lower_four_product. ((((exists pa_h_pc_central_lower_four_product_factor. pa_h_pc_central_lower_four_product_factor + S (pa_p_pc_central_lower_four_product) = S ((S (pa_i_pc_central_lower_four_product)) * pa_c_pc_central_lower_four)) /\ exists pa_q_pc_central_lower_four_product_factor. pa_b_pc_central_lower_four = pa_q_pc_central_lower_four_product_factor * S ((S (pa_i_pc_central_lower_four_product)) * pa_c_pc_central_lower_four) + (pa_p_pc_central_lower_four_product))) /\ ((((exists pa_h_pc_central_lower_four_product_partial. pa_h_pc_central_lower_four_product_partial + S (pa_r_pc_central_lower_four_product) = S ((S (pa_i_pc_central_lower_four_product)) * pa_v_pc_central_lower_four_product)) /\ exists pa_q_pc_central_lower_four_product_partial. pa_u_pc_central_lower_four_product = pa_q_pc_central_lower_four_product_partial * S ((S (pa_i_pc_central_lower_four_product)) * pa_v_pc_central_lower_four_product) + (pa_r_pc_central_lower_four_product))) /\ ((((exists pa_h_pc_central_lower_four_product_successor. pa_h_pc_central_lower_four_product_successor + S (pa_s_pc_central_lower_four_product) = S ((S (S pa_i_pc_central_lower_four_product)) * pa_v_pc_central_lower_four_product)) /\ exists pa_q_pc_central_lower_four_product_successor. pa_u_pc_central_lower_four_product = pa_q_pc_central_lower_four_product_successor * S ((S (S pa_i_pc_central_lower_four_product)) * pa_v_pc_central_lower_four_product) + (pa_s_pc_central_lower_four_product))) /\ pa_s_pc_central_lower_four_product = pa_r_pc_central_lower_four_product * pa_p_pc_central_lower_four_product)))))))
  8. 0008specialize pow_exists 4
  9. 0009specialize pow_exists n
  10. 0010apply pow_exists
  11. 0011cases hw
  12. 0012have hsquare : x = v * v
  13. 0013specialize pow_four_is_square_of_pow_two n
  14. 0014specialize pow_four_is_square_of_pow_two v
  15. 0015specialize pow_four_is_square_of_pow_two x
  16. 0016apply pow_four_is_square_of_pow_two
  17. 0017exact hv
  18. 0018exact hw_witness
  19. 0019have hlower : exists g. g + S x = n * C
  20. 0020specialize four_pow_lt_mul_central_binom n
  21. 0021specialize four_pow_lt_mul_central_binom x
  22. 0022specialize four_pow_lt_mul_central_binom C
  23. 0023apply four_pow_lt_mul_central_binom
  24. 0024exact hn
  25. 0025exact hw_witness
  26. 0026exact hC
  27. 0027have hnsmall : exists g. g + n = v
  28. 0028specialize lt_to_le n
  29. 0029specialize lt_to_le v
  30. 0030apply lt_to_le
  31. 0031specialize binary_power_two_dominates_successor n
  32. 0032specialize binary_power_two_dominates_successor v
  33. 0033apply binary_power_two_dominates_successor
  34. 0034exact hv
  35. 0035have hscale : exists g. g + n * C = v * C
  36. 0036specialize mul_le_mul_right n
  37. 0037specialize mul_le_mul_right v
  38. 0038specialize mul_le_mul_right C
  39. 0039apply mul_le_mul_right
  40. 0040exact hnsmall
  41. 0041have hfull : exists g. g + x = v * C
  42. 0042specialize le_trans x
  43. 0043specialize le_trans (n * C)
  44. 0044specialize le_trans (v * C)
  45. 0045apply le_trans
  46. 0046specialize lt_to_le x
  47. 0047specialize lt_to_le (n * C)
  48. 0048apply lt_to_le
  49. 0049exact hlower
  50. 0050exact hscale
  51. 0051rewrite hsquare at hfull
  52. 0052specialize mul_le_cancel_left_nonzero v
  53. 0053specialize mul_le_cancel_left_nonzero v
  54. 0054specialize mul_le_cancel_left_nonzero C
  55. 0055apply mul_le_cancel_left_nonzero
  56. 0056intro hz
  57. 0057specialize pow_nonzero_of_one_le 2
  58. 0058specialize pow_nonzero_of_one_le n
  59. 0059specialize pow_nonzero_of_one_le v
  60. 0060apply pow_nonzero_of_one_le
  61. 0061exists 1
  62. 0062norm_num
  63. 0063exact hv
  64. 0064exact hz
  65. 0065exact hfull