PC002E

central_binom_prime_count_exponent_bound

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

Central-binomial growth and actual prime contributions force floor(N/2) <= BitLen(N)*pi(N) whenever the half is at least four.

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

Constructive proof overview

Generated structural guide

Central-binomial growth and actual prime contributions force floor(N/2) <= BitLen(N)*pi(N) whenever the half is at least four.

The unchanged tactic script uses 10 declared prerequisites and contains 117 exact native proof lines.

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

Proof neighborhood

Direct dependencies

central_binom_exists Alpha theorem; checked-use authorized pow_exists Stable theorem; checked-use authorized binary_length_upper_power_bound Alpha theorem; checked-use authorized PC001F central_binom_prime_count_power_bound PC0019 central_binom_dominates_pow_two le_trans Stable theorem; checked-use authorized lt_to_le Stable theorem; checked-use authorized pow_base_monotone Alpha theorem; checked-use authorized pow_mul_exp Stable theorem; checked-use authorized PC0016 binary_power_two_order_reflects_exponent

Direct dependents

PC002F prime_count_chebyshev_lower_large

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

117 script commands · 27 reading checkpoints · 11 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (3)
central binom prime count power boundcentral binom dominates pow twobinary power two order reflects exponent

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

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

  1. L1
    intro N
  2. L2
    intro ell
  3. L3
    intro k
  4. L4
    intro h
  5. L5
    intro hh
  6. L6
    intro hN
  7. L7
    intro hl
  8. L8
    intro hk
02Establish hCL9–11

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

  1. L9
    have hC : ∃ C. CentralBinom(h,C)Definitions: CentralBinom
  2. L10
    specialize central_binom_exists h
  3. L11
    apply central_binom_exists
03Separate the logical casesL12–12

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

  1. L12
    cases hC
04Establish hVL13–16

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

  1. L13
    have hV : ∃ V. PowTwo(h,V)Definitions: PowTwo
  2. L14
    specialize pow_exists 2
  3. L15
    specialize pow_exists h
  4. L16
    apply pow_exists
05Separate the logical casesL17–17

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

  1. L17
    cases hV
06Establish hWL18–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary length upper power bound.

  1. L18
    have hW : ∃ W. PowTwo(ell,W) ∧ Lt(N,W)Definitions: PowTwoLt
  2. L19
    specialize binary_length_upper_power_bound N
  3. L20
    specialize binary_length_upper_power_bound ell
  4. L21
    apply binary_length_upper_power_bound
  5. L22
    exact hl
07Separate the logical casesL23–24

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

  1. L23
    cases hW
  2. L24
    cases hW_witness
08Establish hQL25–28

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

  1. L25
    have hQ : ∃ Q. Pow(h + h,k,Q)Definitions: Pow
  2. L26
    specialize pow_exists (h + h)
  3. L27
    specialize pow_exists k
  4. L28
    apply pow_exists
09Separate the logical casesL29–29

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

  1. L29
    cases hQ
10Establish hRL30–33

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

  1. L30
    have hR : ∃ R. Pow(x2,k,R)Definitions: Pow
  2. L31
    specialize pow_exists x2
  3. L32
    specialize pow_exists k
  4. L33
    apply pow_exists
11Separate the logical casesL34–34

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

  1. L34
    cases hR
12Establish hTL35–38

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

  1. L35
    have hT : ∃ T. PowTwo(ell · k,T)Definitions: PowTwo
  2. L36
    specialize pow_exists 2
  3. L37
    specialize pow_exists (ell * k)
  4. L38
    apply pow_exists
13Separate the logical casesL39–39

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

  1. L39
    cases hT
14Establish hCboundL40–49

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

  1. L40
    have hCbound : exists g. g + x = x3
  2. L41
    specialize central_binom_prime_count_power_bound h
  3. L42
    specialize central_binom_prime_count_power_bound N
  4. L43
    specialize central_binom_prime_count_power_bound k
  5. L44
    specialize central_binom_prime_count_power_bound x
  6. L45
    specialize central_binom_prime_count_power_bound x3
  7. L46
    apply central_binom_prime_count_power_bound
  8. L47
    specialize le_trans 1
  9. L48
    specialize le_trans 4
  10. L49
    specialize le_trans h
15Use earlier factsL50–50

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

  1. L50
    apply le_trans
16Construct an explicit witnessL51–51

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

  1. L51
    exists 3
17Calculate and transport equalitiesL52–52

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

  1. L52
    norm_num
18Use earlier factsL53–57

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

  1. L53
    exact hh
  2. L54
    exact hN
  3. L55
    exact hk
  4. L56
    exact hC_witness
  5. L57
    exact hQ_witness
19Establish hVboundL58–67

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

  1. L58
    have hVbound : exists g. g + x1 = x3
  2. L59
    specialize le_trans x1
  3. L60
    specialize le_trans x
  4. L61
    specialize le_trans x3
  5. L62
    apply le_trans
  6. L63
    specialize central_binom_dominates_pow_two h
  7. L64
    specialize central_binom_dominates_pow_two x
  8. L65
    specialize central_binom_dominates_pow_two x1
  9. L66
    apply central_binom_dominates_pow_two
  10. L67
    exact hh
20Use earlier factsL68–70

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

  1. L68
    exact hC_witness
  2. L69
    exact hV_witness
  3. L70
    exact hCbound
21Establish hbaseL71–80

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

  1. L71
    have hbase : exists g. g + (h + h) = x2
  2. L72
    specialize le_trans (h + h)
  3. L73
    specialize le_trans N
  4. L74
    specialize le_trans x2
  5. L75
    apply le_trans
  6. L76
    exact hN
  7. L77
    specialize lt_to_le N
  8. L78
    specialize lt_to_le x2
  9. L79
    apply lt_to_le
  10. L80
    exact hW_witness_right
22Establish hQboundL81–90

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

  1. L81
    have hQbound : exists g. g + x3 = x4
  2. L82
    specialize pow_base_monotone (h + h)
  3. L83
    specialize pow_base_monotone x2
  4. L84
    specialize pow_base_monotone k
  5. L85
    specialize pow_base_monotone x3
  6. L86
    specialize pow_base_monotone x4
  7. L87
    apply pow_base_monotone
  8. L88
    exact hbase
  9. L89
    exact hQ_witness
  10. L90
    exact hR_witness
23Establish hflatL91–100

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

  1. L91
    have hflat : x4 = x5
  2. L92
    specialize pow_mul_exp 2
  3. L93
    specialize pow_mul_exp ell
  4. L94
    specialize pow_mul_exp k
  5. L95
    specialize pow_mul_exp (ell * k)
  6. L96
    specialize pow_mul_exp x2
  7. L97
    specialize pow_mul_exp x4
  8. L98
    specialize pow_mul_exp x5
  9. L99
    apply pow_mul_exp
  10. L100
    refl
24Use earlier factsL101–103

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

  1. L101
    exact hW_witness_left
  2. L102
    exact hR_witness
  3. L103
    exact hT_witness
25Calculate and transport equalitiesL104–104

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

  1. L104
    rewrite hflat at hQbound
26Use earlier factsL105–114

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

  1. L105
    specialize binary_power_two_order_reflects_exponent h
  2. L106
    specialize binary_power_two_order_reflects_exponent (ell * k)
  3. L107
    specialize binary_power_two_order_reflects_exponent x1
  4. L108
    specialize binary_power_two_order_reflects_exponent x5
  5. L109
    apply binary_power_two_order_reflects_exponent
  6. L110
    exact hV_witness
  7. L111
    exact hT_witness
  8. L112
    specialize le_trans x1
  9. L113
    specialize le_trans x3
  10. L114
    specialize le_trans x5
27Use earlier factsL115–117

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

  1. L115
    apply le_trans
  2. L116
    exact hVbound
  3. L117
    exact hQbound

Library-wide reading audit

Original exact command ledger · 117 lines
  1. 0001intro N
  2. 0002intro ell
  3. 0003intro k
  4. 0004intro h
  5. 0005intro hh
  6. 0006intro hN
  7. 0007intro hl
  8. 0008intro hk
  9. 0009have hC : exists C. ((exists bcf_lt_gap_pc_central_exp_central_out_of_range. bcf_lt_gap_pc_central_exp_central_out_of_range + S (h + h) = h) /\ C = 0) \/ ((exists bcf_le_gap_pc_central_exp_central_in_range. bcf_le_gap_pc_central_exp_central_in_range + (h) = h + h) /\ (exists bcf_row_code_code_pc_central_exp_central bcf_row_code_scale_pc_central_exp_central bcf_row_scale_code_pc_central_exp_central bcf_row_scale_scale_pc_central_exp_central bcf_row_code_pc_central_exp_central bcf_row_scale_pc_central_exp_central. ((forall bcf_row_index_pc_central_exp_central_table. (exists bcf_lt_gap_pc_central_exp_central_table_row_bound. bcf_lt_gap_pc_central_exp_central_table_row_bound + S (bcf_row_index_pc_central_exp_central_table) = S (h + h)) -> exists bcf_row_code_pc_central_exp_central_table bcf_row_scale_pc_central_exp_central_table. ((((exists bcf_height_pc_central_exp_central_table_decoded_row_code. bcf_height_pc_central_exp_central_table_decoded_row_code + S (bcf_row_code_pc_central_exp_central_table) = S ((S (bcf_row_index_pc_central_exp_central_table)) * bcf_row_code_scale_pc_central_exp_central)) /\ exists bcf_quotient_pc_central_exp_central_table_decoded_row_code. bcf_row_code_code_pc_central_exp_central = bcf_quotient_pc_central_exp_central_table_decoded_row_code * S ((S (bcf_row_index_pc_central_exp_central_table)) * bcf_row_code_scale_pc_central_exp_central) + (bcf_row_code_pc_central_exp_central_table))) /\ ((((exists bcf_height_pc_central_exp_central_table_decoded_row_scale. bcf_height_pc_central_exp_central_table_decoded_row_scale + S (bcf_row_scale_pc_central_exp_central_table) = S ((S (bcf_row_index_pc_central_exp_central_table)) * bcf_row_scale_scale_pc_central_exp_central)) /\ exists bcf_quotient_pc_central_exp_central_table_decoded_row_scale. bcf_row_scale_code_pc_central_exp_central = bcf_quotient_pc_central_exp_central_table_decoded_row_scale * S ((S (bcf_row_index_pc_central_exp_central_table)) * bcf_row_scale_scale_pc_central_exp_central) + (bcf_row_scale_pc_central_exp_central_table))) /\ ((bcf_row_index_pc_central_exp_central_table = 0 /\ (forall bcf_index_pc_central_exp_central_table_zero_row. (exists bcf_lt_gap_pc_central_exp_central_table_zero_row_bound. bcf_lt_gap_pc_central_exp_central_table_zero_row_bound + S (bcf_index_pc_central_exp_central_table_zero_row) = S (h + h)) -> exists bcf_value_pc_central_exp_central_table_zero_row. ((((exists bcf_height_pc_central_exp_central_table_zero_row_entry. bcf_height_pc_central_exp_central_table_zero_row_entry + S (bcf_value_pc_central_exp_central_table_zero_row) = S ((S (bcf_index_pc_central_exp_central_table_zero_row)) * bcf_row_scale_pc_central_exp_central_table)) /\ exists bcf_quotient_pc_central_exp_central_table_zero_row_entry. bcf_row_code_pc_central_exp_central_table = bcf_quotient_pc_central_exp_central_table_zero_row_entry * S ((S (bcf_index_pc_central_exp_central_table_zero_row)) * bcf_row_scale_pc_central_exp_central_table) + (bcf_value_pc_central_exp_central_table_zero_row))) /\ ((bcf_index_pc_central_exp_central_table_zero_row = 0 /\ bcf_value_pc_central_exp_central_table_zero_row = 1) \/ exists bcf_predecessor_pc_central_exp_central_table_zero_row. bcf_index_pc_central_exp_central_table_zero_row = S bcf_predecessor_pc_central_exp_central_table_zero_row /\ bcf_value_pc_central_exp_central_table_zero_row = 0)))) \/ exists bcf_predecessor_pc_central_exp_central_table bcf_previous_code_pc_central_exp_central_table bcf_previous_scale_pc_central_exp_central_table. bcf_row_index_pc_central_exp_central_table = S bcf_predecessor_pc_central_exp_central_table /\ ((((exists bcf_height_pc_central_exp_central_table_decoded_previous_code. bcf_height_pc_central_exp_central_table_decoded_previous_code + S (bcf_previous_code_pc_central_exp_central_table) = S ((S (bcf_predecessor_pc_central_exp_central_table)) * bcf_row_code_scale_pc_central_exp_central)) /\ exists bcf_quotient_pc_central_exp_central_table_decoded_previous_code. bcf_row_code_code_pc_central_exp_central = bcf_quotient_pc_central_exp_central_table_decoded_previous_code * S ((S (bcf_predecessor_pc_central_exp_central_table)) * bcf_row_code_scale_pc_central_exp_central) + (bcf_previous_code_pc_central_exp_central_table))) /\ ((((exists bcf_height_pc_central_exp_central_table_decoded_previous_scale. bcf_height_pc_central_exp_central_table_decoded_previous_scale + S (bcf_previous_scale_pc_central_exp_central_table) = S ((S (bcf_predecessor_pc_central_exp_central_table)) * bcf_row_scale_scale_pc_central_exp_central)) /\ exists bcf_quotient_pc_central_exp_central_table_decoded_previous_scale. bcf_row_scale_code_pc_central_exp_central = bcf_quotient_pc_central_exp_central_table_decoded_previous_scale * S ((S (bcf_predecessor_pc_central_exp_central_table)) * bcf_row_scale_scale_pc_central_exp_central) + (bcf_previous_scale_pc_central_exp_central_table))) /\ (forall bcf_index_pc_central_exp_central_table_row_step. (exists bcf_lt_gap_pc_central_exp_central_table_row_step_bound. bcf_lt_gap_pc_central_exp_central_table_row_step_bound + S (bcf_index_pc_central_exp_central_table_row_step) = S (h + h)) -> exists bcf_value_pc_central_exp_central_table_row_step. ((((exists bcf_height_pc_central_exp_central_table_row_step_entry. bcf_height_pc_central_exp_central_table_row_step_entry + S (bcf_value_pc_central_exp_central_table_row_step) = S ((S (bcf_index_pc_central_exp_central_table_row_step)) * bcf_row_scale_pc_central_exp_central_table)) /\ exists bcf_quotient_pc_central_exp_central_table_row_step_entry. bcf_row_code_pc_central_exp_central_table = bcf_quotient_pc_central_exp_central_table_row_step_entry * S ((S (bcf_index_pc_central_exp_central_table_row_step)) * bcf_row_scale_pc_central_exp_central_table) + (bcf_value_pc_central_exp_central_table_row_step))) /\ ((bcf_index_pc_central_exp_central_table_row_step = 0 /\ bcf_value_pc_central_exp_central_table_row_step = 1) \/ exists bcf_predecessor_pc_central_exp_central_table_row_step bcf_left_pc_central_exp_central_table_row_step bcf_right_pc_central_exp_central_table_row_step. bcf_index_pc_central_exp_central_table_row_step = S bcf_predecessor_pc_central_exp_central_table_row_step /\ ((((exists bcf_height_pc_central_exp_central_table_row_step_previous_left. bcf_height_pc_central_exp_central_table_row_step_previous_left + S (bcf_left_pc_central_exp_central_table_row_step) = S ((S (bcf_predecessor_pc_central_exp_central_table_row_step)) * bcf_previous_scale_pc_central_exp_central_table)) /\ exists bcf_quotient_pc_central_exp_central_table_row_step_previous_left. bcf_previous_code_pc_central_exp_central_table = bcf_quotient_pc_central_exp_central_table_row_step_previous_left * S ((S (bcf_predecessor_pc_central_exp_central_table_row_step)) * bcf_previous_scale_pc_central_exp_central_table) + (bcf_left_pc_central_exp_central_table_row_step))) /\ ((((exists bcf_height_pc_central_exp_central_table_row_step_previous_right. bcf_height_pc_central_exp_central_table_row_step_previous_right + S (bcf_right_pc_central_exp_central_table_row_step) = S ((S (S (bcf_predecessor_pc_central_exp_central_table_row_step))) * bcf_previous_scale_pc_central_exp_central_table)) /\ exists bcf_quotient_pc_central_exp_central_table_row_step_previous_right. bcf_previous_code_pc_central_exp_central_table = bcf_quotient_pc_central_exp_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_pc_central_exp_central_table_row_step))) * bcf_previous_scale_pc_central_exp_central_table) + (bcf_right_pc_central_exp_central_table_row_step))) /\ bcf_value_pc_central_exp_central_table_row_step = bcf_left_pc_central_exp_central_table_row_step + bcf_right_pc_central_exp_central_table_row_step))))))))))) /\ ((((exists bcf_height_pc_central_exp_central_decoded_row_code. bcf_height_pc_central_exp_central_decoded_row_code + S (bcf_row_code_pc_central_exp_central) = S ((S (h + h)) * bcf_row_code_scale_pc_central_exp_central)) /\ exists bcf_quotient_pc_central_exp_central_decoded_row_code. bcf_row_code_code_pc_central_exp_central = bcf_quotient_pc_central_exp_central_decoded_row_code * S ((S (h + h)) * bcf_row_code_scale_pc_central_exp_central) + (bcf_row_code_pc_central_exp_central))) /\ ((((exists bcf_height_pc_central_exp_central_decoded_row_scale. bcf_height_pc_central_exp_central_decoded_row_scale + S (bcf_row_scale_pc_central_exp_central) = S ((S (h + h)) * bcf_row_scale_scale_pc_central_exp_central)) /\ exists bcf_quotient_pc_central_exp_central_decoded_row_scale. bcf_row_scale_code_pc_central_exp_central = bcf_quotient_pc_central_exp_central_decoded_row_scale * S ((S (h + h)) * bcf_row_scale_scale_pc_central_exp_central) + (bcf_row_scale_pc_central_exp_central))) /\ (((exists bcf_height_pc_central_exp_central_decoded_value. bcf_height_pc_central_exp_central_decoded_value + S (C) = S ((S (h)) * bcf_row_scale_pc_central_exp_central)) /\ exists bcf_quotient_pc_central_exp_central_decoded_value. bcf_row_code_pc_central_exp_central = bcf_quotient_pc_central_exp_central_decoded_value * S ((S (h)) * bcf_row_scale_pc_central_exp_central) + (C))))))))
  10. 0010specialize central_binom_exists h
  11. 0011apply central_binom_exists
  12. 0012cases hC
  13. 0013have hV : exists V. exists pa_b_pc_central_exp_half_power pa_c_pc_central_exp_half_power. ((forall pa_i_pc_central_exp_half_power_repeat. (exists pa_lt_pc_central_exp_half_power_repeat_bound. pa_lt_pc_central_exp_half_power_repeat_bound + S pa_i_pc_central_exp_half_power_repeat = h) -> (((exists pa_h_pc_central_exp_half_power_repeat_decoded. pa_h_pc_central_exp_half_power_repeat_decoded + S (2) = S ((S (pa_i_pc_central_exp_half_power_repeat)) * pa_c_pc_central_exp_half_power)) /\ exists pa_q_pc_central_exp_half_power_repeat_decoded. pa_b_pc_central_exp_half_power = pa_q_pc_central_exp_half_power_repeat_decoded * S ((S (pa_i_pc_central_exp_half_power_repeat)) * pa_c_pc_central_exp_half_power) + (2)))) /\ (exists pa_u_pc_central_exp_half_power_product pa_v_pc_central_exp_half_power_product. ((((exists pa_h_pc_central_exp_half_power_product_start. pa_h_pc_central_exp_half_power_product_start + S (1) = S ((S (0)) * pa_v_pc_central_exp_half_power_product)) /\ exists pa_q_pc_central_exp_half_power_product_start. pa_u_pc_central_exp_half_power_product = pa_q_pc_central_exp_half_power_product_start * S ((S (0)) * pa_v_pc_central_exp_half_power_product) + (1))) /\ ((((exists pa_h_pc_central_exp_half_power_product_terminal. pa_h_pc_central_exp_half_power_product_terminal + S (V) = S ((S (h)) * pa_v_pc_central_exp_half_power_product)) /\ exists pa_q_pc_central_exp_half_power_product_terminal. pa_u_pc_central_exp_half_power_product = pa_q_pc_central_exp_half_power_product_terminal * S ((S (h)) * pa_v_pc_central_exp_half_power_product) + (V))) /\ forall pa_i_pc_central_exp_half_power_product. (exists pa_lt_pc_central_exp_half_power_product_bound. pa_lt_pc_central_exp_half_power_product_bound + S pa_i_pc_central_exp_half_power_product = h) -> exists pa_p_pc_central_exp_half_power_product pa_r_pc_central_exp_half_power_product pa_s_pc_central_exp_half_power_product. ((((exists pa_h_pc_central_exp_half_power_product_factor. pa_h_pc_central_exp_half_power_product_factor + S (pa_p_pc_central_exp_half_power_product) = S ((S (pa_i_pc_central_exp_half_power_product)) * pa_c_pc_central_exp_half_power)) /\ exists pa_q_pc_central_exp_half_power_product_factor. pa_b_pc_central_exp_half_power = pa_q_pc_central_exp_half_power_product_factor * S ((S (pa_i_pc_central_exp_half_power_product)) * pa_c_pc_central_exp_half_power) + (pa_p_pc_central_exp_half_power_product))) /\ ((((exists pa_h_pc_central_exp_half_power_product_partial. pa_h_pc_central_exp_half_power_product_partial + S (pa_r_pc_central_exp_half_power_product) = S ((S (pa_i_pc_central_exp_half_power_product)) * pa_v_pc_central_exp_half_power_product)) /\ exists pa_q_pc_central_exp_half_power_product_partial. pa_u_pc_central_exp_half_power_product = pa_q_pc_central_exp_half_power_product_partial * S ((S (pa_i_pc_central_exp_half_power_product)) * pa_v_pc_central_exp_half_power_product) + (pa_r_pc_central_exp_half_power_product))) /\ ((((exists pa_h_pc_central_exp_half_power_product_successor. pa_h_pc_central_exp_half_power_product_successor + S (pa_s_pc_central_exp_half_power_product) = S ((S (S pa_i_pc_central_exp_half_power_product)) * pa_v_pc_central_exp_half_power_product)) /\ exists pa_q_pc_central_exp_half_power_product_successor. pa_u_pc_central_exp_half_power_product = pa_q_pc_central_exp_half_power_product_successor * S ((S (S pa_i_pc_central_exp_half_power_product)) * pa_v_pc_central_exp_half_power_product) + (pa_s_pc_central_exp_half_power_product))) /\ pa_s_pc_central_exp_half_power_product = pa_r_pc_central_exp_half_power_product * pa_p_pc_central_exp_half_power_product)))))))
  14. 0014specialize pow_exists 2
  15. 0015specialize pow_exists h
  16. 0016apply pow_exists
  17. 0017cases hV
  18. 0018have hW : exists W. (exists pa_b_pc_central_exp_upper_power pa_c_pc_central_exp_upper_power. ((forall pa_i_pc_central_exp_upper_power_repeat. (exists pa_lt_pc_central_exp_upper_power_repeat_bound. pa_lt_pc_central_exp_upper_power_repeat_bound + S pa_i_pc_central_exp_upper_power_repeat = ell) -> (((exists pa_h_pc_central_exp_upper_power_repeat_decoded. pa_h_pc_central_exp_upper_power_repeat_decoded + S (2) = S ((S (pa_i_pc_central_exp_upper_power_repeat)) * pa_c_pc_central_exp_upper_power)) /\ exists pa_q_pc_central_exp_upper_power_repeat_decoded. pa_b_pc_central_exp_upper_power = pa_q_pc_central_exp_upper_power_repeat_decoded * S ((S (pa_i_pc_central_exp_upper_power_repeat)) * pa_c_pc_central_exp_upper_power) + (2)))) /\ (exists pa_u_pc_central_exp_upper_power_product pa_v_pc_central_exp_upper_power_product. ((((exists pa_h_pc_central_exp_upper_power_product_start. pa_h_pc_central_exp_upper_power_product_start + S (1) = S ((S (0)) * pa_v_pc_central_exp_upper_power_product)) /\ exists pa_q_pc_central_exp_upper_power_product_start. pa_u_pc_central_exp_upper_power_product = pa_q_pc_central_exp_upper_power_product_start * S ((S (0)) * pa_v_pc_central_exp_upper_power_product) + (1))) /\ ((((exists pa_h_pc_central_exp_upper_power_product_terminal. pa_h_pc_central_exp_upper_power_product_terminal + S (W) = S ((S (ell)) * pa_v_pc_central_exp_upper_power_product)) /\ exists pa_q_pc_central_exp_upper_power_product_terminal. pa_u_pc_central_exp_upper_power_product = pa_q_pc_central_exp_upper_power_product_terminal * S ((S (ell)) * pa_v_pc_central_exp_upper_power_product) + (W))) /\ forall pa_i_pc_central_exp_upper_power_product. (exists pa_lt_pc_central_exp_upper_power_product_bound. pa_lt_pc_central_exp_upper_power_product_bound + S pa_i_pc_central_exp_upper_power_product = ell) -> exists pa_p_pc_central_exp_upper_power_product pa_r_pc_central_exp_upper_power_product pa_s_pc_central_exp_upper_power_product. ((((exists pa_h_pc_central_exp_upper_power_product_factor. pa_h_pc_central_exp_upper_power_product_factor + S (pa_p_pc_central_exp_upper_power_product) = S ((S (pa_i_pc_central_exp_upper_power_product)) * pa_c_pc_central_exp_upper_power)) /\ exists pa_q_pc_central_exp_upper_power_product_factor. pa_b_pc_central_exp_upper_power = pa_q_pc_central_exp_upper_power_product_factor * S ((S (pa_i_pc_central_exp_upper_power_product)) * pa_c_pc_central_exp_upper_power) + (pa_p_pc_central_exp_upper_power_product))) /\ ((((exists pa_h_pc_central_exp_upper_power_product_partial. pa_h_pc_central_exp_upper_power_product_partial + S (pa_r_pc_central_exp_upper_power_product) = S ((S (pa_i_pc_central_exp_upper_power_product)) * pa_v_pc_central_exp_upper_power_product)) /\ exists pa_q_pc_central_exp_upper_power_product_partial. pa_u_pc_central_exp_upper_power_product = pa_q_pc_central_exp_upper_power_product_partial * S ((S (pa_i_pc_central_exp_upper_power_product)) * pa_v_pc_central_exp_upper_power_product) + (pa_r_pc_central_exp_upper_power_product))) /\ ((((exists pa_h_pc_central_exp_upper_power_product_successor. pa_h_pc_central_exp_upper_power_product_successor + S (pa_s_pc_central_exp_upper_power_product) = S ((S (S pa_i_pc_central_exp_upper_power_product)) * pa_v_pc_central_exp_upper_power_product)) /\ exists pa_q_pc_central_exp_upper_power_product_successor. pa_u_pc_central_exp_upper_power_product = pa_q_pc_central_exp_upper_power_product_successor * S ((S (S pa_i_pc_central_exp_upper_power_product)) * pa_v_pc_central_exp_upper_power_product) + (pa_s_pc_central_exp_upper_power_product))) /\ pa_s_pc_central_exp_upper_power_product = pa_r_pc_central_exp_upper_power_product * pa_p_pc_central_exp_upper_power_product)))))))) /\ (exists pc_lt_central_exp_upper_bound. pc_lt_central_exp_upper_bound + S (N) = (W))
  19. 0019specialize binary_length_upper_power_bound N
  20. 0020specialize binary_length_upper_power_bound ell
  21. 0021apply binary_length_upper_power_bound
  22. 0022exact hl
  23. 0023cases hW
  24. 0024cases hW_witness
  25. 0025have hQ : exists Q. exists pa_b_pc_central_exp_factor_power pa_c_pc_central_exp_factor_power. ((forall pa_i_pc_central_exp_factor_power_repeat. (exists pa_lt_pc_central_exp_factor_power_repeat_bound. pa_lt_pc_central_exp_factor_power_repeat_bound + S pa_i_pc_central_exp_factor_power_repeat = k) -> (((exists pa_h_pc_central_exp_factor_power_repeat_decoded. pa_h_pc_central_exp_factor_power_repeat_decoded + S (h + h) = S ((S (pa_i_pc_central_exp_factor_power_repeat)) * pa_c_pc_central_exp_factor_power)) /\ exists pa_q_pc_central_exp_factor_power_repeat_decoded. pa_b_pc_central_exp_factor_power = pa_q_pc_central_exp_factor_power_repeat_decoded * S ((S (pa_i_pc_central_exp_factor_power_repeat)) * pa_c_pc_central_exp_factor_power) + (h + h)))) /\ (exists pa_u_pc_central_exp_factor_power_product pa_v_pc_central_exp_factor_power_product. ((((exists pa_h_pc_central_exp_factor_power_product_start. pa_h_pc_central_exp_factor_power_product_start + S (1) = S ((S (0)) * pa_v_pc_central_exp_factor_power_product)) /\ exists pa_q_pc_central_exp_factor_power_product_start. pa_u_pc_central_exp_factor_power_product = pa_q_pc_central_exp_factor_power_product_start * S ((S (0)) * pa_v_pc_central_exp_factor_power_product) + (1))) /\ ((((exists pa_h_pc_central_exp_factor_power_product_terminal. pa_h_pc_central_exp_factor_power_product_terminal + S (Q) = S ((S (k)) * pa_v_pc_central_exp_factor_power_product)) /\ exists pa_q_pc_central_exp_factor_power_product_terminal. pa_u_pc_central_exp_factor_power_product = pa_q_pc_central_exp_factor_power_product_terminal * S ((S (k)) * pa_v_pc_central_exp_factor_power_product) + (Q))) /\ forall pa_i_pc_central_exp_factor_power_product. (exists pa_lt_pc_central_exp_factor_power_product_bound. pa_lt_pc_central_exp_factor_power_product_bound + S pa_i_pc_central_exp_factor_power_product = k) -> exists pa_p_pc_central_exp_factor_power_product pa_r_pc_central_exp_factor_power_product pa_s_pc_central_exp_factor_power_product. ((((exists pa_h_pc_central_exp_factor_power_product_factor. pa_h_pc_central_exp_factor_power_product_factor + S (pa_p_pc_central_exp_factor_power_product) = S ((S (pa_i_pc_central_exp_factor_power_product)) * pa_c_pc_central_exp_factor_power)) /\ exists pa_q_pc_central_exp_factor_power_product_factor. pa_b_pc_central_exp_factor_power = pa_q_pc_central_exp_factor_power_product_factor * S ((S (pa_i_pc_central_exp_factor_power_product)) * pa_c_pc_central_exp_factor_power) + (pa_p_pc_central_exp_factor_power_product))) /\ ((((exists pa_h_pc_central_exp_factor_power_product_partial. pa_h_pc_central_exp_factor_power_product_partial + S (pa_r_pc_central_exp_factor_power_product) = S ((S (pa_i_pc_central_exp_factor_power_product)) * pa_v_pc_central_exp_factor_power_product)) /\ exists pa_q_pc_central_exp_factor_power_product_partial. pa_u_pc_central_exp_factor_power_product = pa_q_pc_central_exp_factor_power_product_partial * S ((S (pa_i_pc_central_exp_factor_power_product)) * pa_v_pc_central_exp_factor_power_product) + (pa_r_pc_central_exp_factor_power_product))) /\ ((((exists pa_h_pc_central_exp_factor_power_product_successor. pa_h_pc_central_exp_factor_power_product_successor + S (pa_s_pc_central_exp_factor_power_product) = S ((S (S pa_i_pc_central_exp_factor_power_product)) * pa_v_pc_central_exp_factor_power_product)) /\ exists pa_q_pc_central_exp_factor_power_product_successor. pa_u_pc_central_exp_factor_power_product = pa_q_pc_central_exp_factor_power_product_successor * S ((S (S pa_i_pc_central_exp_factor_power_product)) * pa_v_pc_central_exp_factor_power_product) + (pa_s_pc_central_exp_factor_power_product))) /\ pa_s_pc_central_exp_factor_power_product = pa_r_pc_central_exp_factor_power_product * pa_p_pc_central_exp_factor_power_product)))))))
  26. 0026specialize pow_exists (h + h)
  27. 0027specialize pow_exists k
  28. 0028apply pow_exists
  29. 0029cases hQ
  30. 0030have hR : exists R. exists pa_b_pc_central_exp_outer_power pa_c_pc_central_exp_outer_power. ((forall pa_i_pc_central_exp_outer_power_repeat. (exists pa_lt_pc_central_exp_outer_power_repeat_bound. pa_lt_pc_central_exp_outer_power_repeat_bound + S pa_i_pc_central_exp_outer_power_repeat = k) -> (((exists pa_h_pc_central_exp_outer_power_repeat_decoded. pa_h_pc_central_exp_outer_power_repeat_decoded + S (x2) = S ((S (pa_i_pc_central_exp_outer_power_repeat)) * pa_c_pc_central_exp_outer_power)) /\ exists pa_q_pc_central_exp_outer_power_repeat_decoded. pa_b_pc_central_exp_outer_power = pa_q_pc_central_exp_outer_power_repeat_decoded * S ((S (pa_i_pc_central_exp_outer_power_repeat)) * pa_c_pc_central_exp_outer_power) + (x2)))) /\ (exists pa_u_pc_central_exp_outer_power_product pa_v_pc_central_exp_outer_power_product. ((((exists pa_h_pc_central_exp_outer_power_product_start. pa_h_pc_central_exp_outer_power_product_start + S (1) = S ((S (0)) * pa_v_pc_central_exp_outer_power_product)) /\ exists pa_q_pc_central_exp_outer_power_product_start. pa_u_pc_central_exp_outer_power_product = pa_q_pc_central_exp_outer_power_product_start * S ((S (0)) * pa_v_pc_central_exp_outer_power_product) + (1))) /\ ((((exists pa_h_pc_central_exp_outer_power_product_terminal. pa_h_pc_central_exp_outer_power_product_terminal + S (R) = S ((S (k)) * pa_v_pc_central_exp_outer_power_product)) /\ exists pa_q_pc_central_exp_outer_power_product_terminal. pa_u_pc_central_exp_outer_power_product = pa_q_pc_central_exp_outer_power_product_terminal * S ((S (k)) * pa_v_pc_central_exp_outer_power_product) + (R))) /\ forall pa_i_pc_central_exp_outer_power_product. (exists pa_lt_pc_central_exp_outer_power_product_bound. pa_lt_pc_central_exp_outer_power_product_bound + S pa_i_pc_central_exp_outer_power_product = k) -> exists pa_p_pc_central_exp_outer_power_product pa_r_pc_central_exp_outer_power_product pa_s_pc_central_exp_outer_power_product. ((((exists pa_h_pc_central_exp_outer_power_product_factor. pa_h_pc_central_exp_outer_power_product_factor + S (pa_p_pc_central_exp_outer_power_product) = S ((S (pa_i_pc_central_exp_outer_power_product)) * pa_c_pc_central_exp_outer_power)) /\ exists pa_q_pc_central_exp_outer_power_product_factor. pa_b_pc_central_exp_outer_power = pa_q_pc_central_exp_outer_power_product_factor * S ((S (pa_i_pc_central_exp_outer_power_product)) * pa_c_pc_central_exp_outer_power) + (pa_p_pc_central_exp_outer_power_product))) /\ ((((exists pa_h_pc_central_exp_outer_power_product_partial. pa_h_pc_central_exp_outer_power_product_partial + S (pa_r_pc_central_exp_outer_power_product) = S ((S (pa_i_pc_central_exp_outer_power_product)) * pa_v_pc_central_exp_outer_power_product)) /\ exists pa_q_pc_central_exp_outer_power_product_partial. pa_u_pc_central_exp_outer_power_product = pa_q_pc_central_exp_outer_power_product_partial * S ((S (pa_i_pc_central_exp_outer_power_product)) * pa_v_pc_central_exp_outer_power_product) + (pa_r_pc_central_exp_outer_power_product))) /\ ((((exists pa_h_pc_central_exp_outer_power_product_successor. pa_h_pc_central_exp_outer_power_product_successor + S (pa_s_pc_central_exp_outer_power_product) = S ((S (S pa_i_pc_central_exp_outer_power_product)) * pa_v_pc_central_exp_outer_power_product)) /\ exists pa_q_pc_central_exp_outer_power_product_successor. pa_u_pc_central_exp_outer_power_product = pa_q_pc_central_exp_outer_power_product_successor * S ((S (S pa_i_pc_central_exp_outer_power_product)) * pa_v_pc_central_exp_outer_power_product) + (pa_s_pc_central_exp_outer_power_product))) /\ pa_s_pc_central_exp_outer_power_product = pa_r_pc_central_exp_outer_power_product * pa_p_pc_central_exp_outer_power_product)))))))
  31. 0031specialize pow_exists x2
  32. 0032specialize pow_exists k
  33. 0033apply pow_exists
  34. 0034cases hR
  35. 0035have hT : exists T. exists pa_b_pc_central_exp_flat_power pa_c_pc_central_exp_flat_power. ((forall pa_i_pc_central_exp_flat_power_repeat. (exists pa_lt_pc_central_exp_flat_power_repeat_bound. pa_lt_pc_central_exp_flat_power_repeat_bound + S pa_i_pc_central_exp_flat_power_repeat = ell * k) -> (((exists pa_h_pc_central_exp_flat_power_repeat_decoded. pa_h_pc_central_exp_flat_power_repeat_decoded + S (2) = S ((S (pa_i_pc_central_exp_flat_power_repeat)) * pa_c_pc_central_exp_flat_power)) /\ exists pa_q_pc_central_exp_flat_power_repeat_decoded. pa_b_pc_central_exp_flat_power = pa_q_pc_central_exp_flat_power_repeat_decoded * S ((S (pa_i_pc_central_exp_flat_power_repeat)) * pa_c_pc_central_exp_flat_power) + (2)))) /\ (exists pa_u_pc_central_exp_flat_power_product pa_v_pc_central_exp_flat_power_product. ((((exists pa_h_pc_central_exp_flat_power_product_start. pa_h_pc_central_exp_flat_power_product_start + S (1) = S ((S (0)) * pa_v_pc_central_exp_flat_power_product)) /\ exists pa_q_pc_central_exp_flat_power_product_start. pa_u_pc_central_exp_flat_power_product = pa_q_pc_central_exp_flat_power_product_start * S ((S (0)) * pa_v_pc_central_exp_flat_power_product) + (1))) /\ ((((exists pa_h_pc_central_exp_flat_power_product_terminal. pa_h_pc_central_exp_flat_power_product_terminal + S (T) = S ((S (ell * k)) * pa_v_pc_central_exp_flat_power_product)) /\ exists pa_q_pc_central_exp_flat_power_product_terminal. pa_u_pc_central_exp_flat_power_product = pa_q_pc_central_exp_flat_power_product_terminal * S ((S (ell * k)) * pa_v_pc_central_exp_flat_power_product) + (T))) /\ forall pa_i_pc_central_exp_flat_power_product. (exists pa_lt_pc_central_exp_flat_power_product_bound. pa_lt_pc_central_exp_flat_power_product_bound + S pa_i_pc_central_exp_flat_power_product = ell * k) -> exists pa_p_pc_central_exp_flat_power_product pa_r_pc_central_exp_flat_power_product pa_s_pc_central_exp_flat_power_product. ((((exists pa_h_pc_central_exp_flat_power_product_factor. pa_h_pc_central_exp_flat_power_product_factor + S (pa_p_pc_central_exp_flat_power_product) = S ((S (pa_i_pc_central_exp_flat_power_product)) * pa_c_pc_central_exp_flat_power)) /\ exists pa_q_pc_central_exp_flat_power_product_factor. pa_b_pc_central_exp_flat_power = pa_q_pc_central_exp_flat_power_product_factor * S ((S (pa_i_pc_central_exp_flat_power_product)) * pa_c_pc_central_exp_flat_power) + (pa_p_pc_central_exp_flat_power_product))) /\ ((((exists pa_h_pc_central_exp_flat_power_product_partial. pa_h_pc_central_exp_flat_power_product_partial + S (pa_r_pc_central_exp_flat_power_product) = S ((S (pa_i_pc_central_exp_flat_power_product)) * pa_v_pc_central_exp_flat_power_product)) /\ exists pa_q_pc_central_exp_flat_power_product_partial. pa_u_pc_central_exp_flat_power_product = pa_q_pc_central_exp_flat_power_product_partial * S ((S (pa_i_pc_central_exp_flat_power_product)) * pa_v_pc_central_exp_flat_power_product) + (pa_r_pc_central_exp_flat_power_product))) /\ ((((exists pa_h_pc_central_exp_flat_power_product_successor. pa_h_pc_central_exp_flat_power_product_successor + S (pa_s_pc_central_exp_flat_power_product) = S ((S (S pa_i_pc_central_exp_flat_power_product)) * pa_v_pc_central_exp_flat_power_product)) /\ exists pa_q_pc_central_exp_flat_power_product_successor. pa_u_pc_central_exp_flat_power_product = pa_q_pc_central_exp_flat_power_product_successor * S ((S (S pa_i_pc_central_exp_flat_power_product)) * pa_v_pc_central_exp_flat_power_product) + (pa_s_pc_central_exp_flat_power_product))) /\ pa_s_pc_central_exp_flat_power_product = pa_r_pc_central_exp_flat_power_product * pa_p_pc_central_exp_flat_power_product)))))))
  36. 0036specialize pow_exists 2
  37. 0037specialize pow_exists (ell * k)
  38. 0038apply pow_exists
  39. 0039cases hT
  40. 0040have hCbound : exists g. g + x = x3
  41. 0041specialize central_binom_prime_count_power_bound h
  42. 0042specialize central_binom_prime_count_power_bound N
  43. 0043specialize central_binom_prime_count_power_bound k
  44. 0044specialize central_binom_prime_count_power_bound x
  45. 0045specialize central_binom_prime_count_power_bound x3
  46. 0046apply central_binom_prime_count_power_bound
  47. 0047specialize le_trans 1
  48. 0048specialize le_trans 4
  49. 0049specialize le_trans h
  50. 0050apply le_trans
  51. 0051exists 3
  52. 0052norm_num
  53. 0053exact hh
  54. 0054exact hN
  55. 0055exact hk
  56. 0056exact hC_witness
  57. 0057exact hQ_witness
  58. 0058have hVbound : exists g. g + x1 = x3
  59. 0059specialize le_trans x1
  60. 0060specialize le_trans x
  61. 0061specialize le_trans x3
  62. 0062apply le_trans
  63. 0063specialize central_binom_dominates_pow_two h
  64. 0064specialize central_binom_dominates_pow_two x
  65. 0065specialize central_binom_dominates_pow_two x1
  66. 0066apply central_binom_dominates_pow_two
  67. 0067exact hh
  68. 0068exact hC_witness
  69. 0069exact hV_witness
  70. 0070exact hCbound
  71. 0071have hbase : exists g. g + (h + h) = x2
  72. 0072specialize le_trans (h + h)
  73. 0073specialize le_trans N
  74. 0074specialize le_trans x2
  75. 0075apply le_trans
  76. 0076exact hN
  77. 0077specialize lt_to_le N
  78. 0078specialize lt_to_le x2
  79. 0079apply lt_to_le
  80. 0080exact hW_witness_right
  81. 0081have hQbound : exists g. g + x3 = x4
  82. 0082specialize pow_base_monotone (h + h)
  83. 0083specialize pow_base_monotone x2
  84. 0084specialize pow_base_monotone k
  85. 0085specialize pow_base_monotone x3
  86. 0086specialize pow_base_monotone x4
  87. 0087apply pow_base_monotone
  88. 0088exact hbase
  89. 0089exact hQ_witness
  90. 0090exact hR_witness
  91. 0091have hflat : x4 = x5
  92. 0092specialize pow_mul_exp 2
  93. 0093specialize pow_mul_exp ell
  94. 0094specialize pow_mul_exp k
  95. 0095specialize pow_mul_exp (ell * k)
  96. 0096specialize pow_mul_exp x2
  97. 0097specialize pow_mul_exp x4
  98. 0098specialize pow_mul_exp x5
  99. 0099apply pow_mul_exp
  100. 0100refl
  101. 0101exact hW_witness_left
  102. 0102exact hR_witness
  103. 0103exact hT_witness
  104. 0104rewrite hflat at hQbound
  105. 0105specialize binary_power_two_order_reflects_exponent h
  106. 0106specialize binary_power_two_order_reflects_exponent (ell * k)
  107. 0107specialize binary_power_two_order_reflects_exponent x1
  108. 0108specialize binary_power_two_order_reflects_exponent x5
  109. 0109apply binary_power_two_order_reflects_exponent
  110. 0110exact hV_witness
  111. 0111exact hT_witness
  112. 0112specialize le_trans x1
  113. 0113specialize le_trans x3
  114. 0114specialize le_trans x5
  115. 0115apply le_trans
  116. 0116exact hVbound
  117. 0117exact hQbound