PC002A

prime_count_chebyshev_upper

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

The exact effective Chebyshev upper bound pi(N)*BitLen(N) <= 8N, including every N at least two.

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. (exists pc_le_cheb_upper_positive. pc_le_cheb_upper_positive + (2) = (N)) -> ((((N) = 0 /\ (ell) = 1) \/ exists ff_exponent_bl_pc_cheb_upper_length ff_lower_bl_pc_cheb_upper_length ff_upper_bl_pc_cheb_upper_length. (((ell) = S ff_exponent_bl_pc_cheb_upper_length) /\ ((exists ff_positive_bl_pc_cheb_upper_length. ff_positive_bl_pc_cheb_upper_length + 1 = (N)) /\ ((exists pa_b_bl_pc_cheb_upper_length_lower pa_c_bl_pc_cheb_upper_length_lower. ((forall pa_i_bl_pc_cheb_upper_length_lower_repeat. (exists pa_lt_bl_pc_cheb_upper_length_lower_repeat_bound. pa_lt_bl_pc_cheb_upper_length_lower_repeat_bound + S pa_i_bl_pc_cheb_upper_length_lower_repeat = ff_exponent_bl_pc_cheb_upper_length) -> (((exists pa_h_bl_pc_cheb_upper_length_lower_repeat_decoded. pa_h_bl_pc_cheb_upper_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_cheb_upper_length_lower_repeat)) * pa_c_bl_pc_cheb_upper_length_lower)) /\ exists pa_q_bl_pc_cheb_upper_length_lower_repeat_decoded. pa_b_bl_pc_cheb_upper_length_lower = pa_q_bl_pc_cheb_upper_length_lower_repeat_decoded * S ((S (pa_i_bl_pc_cheb_upper_length_lower_repeat)) * pa_c_bl_pc_cheb_upper_length_lower) + (2)))) /\ (exists pa_u_bl_pc_cheb_upper_length_lower_product pa_v_bl_pc_cheb_upper_length_lower_product. ((((exists pa_h_bl_pc_cheb_upper_length_lower_product_start. pa_h_bl_pc_cheb_upper_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_cheb_upper_length_lower_product)) /\ exists pa_q_bl_pc_cheb_upper_length_lower_product_start. pa_u_bl_pc_cheb_upper_length_lower_product = pa_q_bl_pc_cheb_upper_length_lower_product_start * S ((S (0)) * pa_v_bl_pc_cheb_upper_length_lower_product) + (1))) /\ ((((exists pa_h_bl_pc_cheb_upper_length_lower_product_terminal. pa_h_bl_pc_cheb_upper_length_lower_product_terminal + S (ff_lower_bl_pc_cheb_upper_length) = S ((S (ff_exponent_bl_pc_cheb_upper_length)) * pa_v_bl_pc_cheb_upper_length_lower_product)) /\ exists pa_q_bl_pc_cheb_upper_length_lower_product_terminal. pa_u_bl_pc_cheb_upper_length_lower_product = pa_q_bl_pc_cheb_upper_length_lower_product_terminal * S ((S (ff_exponent_bl_pc_cheb_upper_length)) * pa_v_bl_pc_cheb_upper_length_lower_product) + (ff_lower_bl_pc_cheb_upper_length))) /\ forall pa_i_bl_pc_cheb_upper_length_lower_product. (exists pa_lt_bl_pc_cheb_upper_length_lower_product_bound. pa_lt_bl_pc_cheb_upper_length_lower_product_bound + S pa_i_bl_pc_cheb_upper_length_lower_product = ff_exponent_bl_pc_cheb_upper_length) -> exists pa_p_bl_pc_cheb_upper_length_lower_product pa_r_bl_pc_cheb_upper_length_lower_product pa_s_bl_pc_cheb_upper_length_lower_product. ((((exists pa_h_bl_pc_cheb_upper_length_lower_product_factor. pa_h_bl_pc_cheb_upper_length_lower_product_factor + S (pa_p_bl_pc_cheb_upper_length_lower_product) = S ((S (pa_i_bl_pc_cheb_upper_length_lower_product)) * pa_c_bl_pc_cheb_upper_length_lower)) /\ exists pa_q_bl_pc_cheb_upper_length_lower_product_factor. pa_b_bl_pc_cheb_upper_length_lower = pa_q_bl_pc_cheb_upper_length_lower_product_factor * S ((S (pa_i_bl_pc_cheb_upper_length_lower_product)) * pa_c_bl_pc_cheb_upper_length_lower) + (pa_p_bl_pc_cheb_upper_length_lower_product))) /\ ((((exists pa_h_bl_pc_cheb_upper_length_lower_product_partial. pa_h_bl_pc_cheb_upper_length_lower_product_partial + S (pa_r_bl_pc_cheb_upper_length_lower_product) = S ((S (pa_i_bl_pc_cheb_upper_length_lower_product)) * pa_v_bl_pc_cheb_upper_length_lower_product)) /\ exists pa_q_bl_pc_cheb_upper_length_lower_product_partial. pa_u_bl_pc_cheb_upper_length_lower_product = pa_q_bl_pc_cheb_upper_length_lower_product_partial * S ((S (pa_i_bl_pc_cheb_upper_length_lower_product)) * pa_v_bl_pc_cheb_upper_length_lower_product) + (pa_r_bl_pc_cheb_upper_length_lower_product))) /\ ((((exists pa_h_bl_pc_cheb_upper_length_lower_product_successor. pa_h_bl_pc_cheb_upper_length_lower_product_successor + S (pa_s_bl_pc_cheb_upper_length_lower_product) = S ((S (S pa_i_bl_pc_cheb_upper_length_lower_product)) * pa_v_bl_pc_cheb_upper_length_lower_product)) /\ exists pa_q_bl_pc_cheb_upper_length_lower_product_successor. pa_u_bl_pc_cheb_upper_length_lower_product = pa_q_bl_pc_cheb_upper_length_lower_product_successor * S ((S (S pa_i_bl_pc_cheb_upper_length_lower_product)) * pa_v_bl_pc_cheb_upper_length_lower_product) + (pa_s_bl_pc_cheb_upper_length_lower_product))) /\ pa_s_bl_pc_cheb_upper_length_lower_product = pa_r_bl_pc_cheb_upper_length_lower_product * pa_p_bl_pc_cheb_upper_length_lower_product)))))))) /\ ((exists pa_b_bl_pc_cheb_upper_length_upper pa_c_bl_pc_cheb_upper_length_upper. ((forall pa_i_bl_pc_cheb_upper_length_upper_repeat. (exists pa_lt_bl_pc_cheb_upper_length_upper_repeat_bound. pa_lt_bl_pc_cheb_upper_length_upper_repeat_bound + S pa_i_bl_pc_cheb_upper_length_upper_repeat = ell) -> (((exists pa_h_bl_pc_cheb_upper_length_upper_repeat_decoded. pa_h_bl_pc_cheb_upper_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_cheb_upper_length_upper_repeat)) * pa_c_bl_pc_cheb_upper_length_upper)) /\ exists pa_q_bl_pc_cheb_upper_length_upper_repeat_decoded. pa_b_bl_pc_cheb_upper_length_upper = pa_q_bl_pc_cheb_upper_length_upper_repeat_decoded * S ((S (pa_i_bl_pc_cheb_upper_length_upper_repeat)) * pa_c_bl_pc_cheb_upper_length_upper) + (2)))) /\ (exists pa_u_bl_pc_cheb_upper_length_upper_product pa_v_bl_pc_cheb_upper_length_upper_product. ((((exists pa_h_bl_pc_cheb_upper_length_upper_product_start. pa_h_bl_pc_cheb_upper_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_cheb_upper_length_upper_product)) /\ exists pa_q_bl_pc_cheb_upper_length_upper_product_start. pa_u_bl_pc_cheb_upper_length_upper_product = pa_q_bl_pc_cheb_upper_length_upper_product_start * S ((S (0)) * pa_v_bl_pc_cheb_upper_length_upper_product) + (1))) /\ ((((exists pa_h_bl_pc_cheb_upper_length_upper_product_terminal. pa_h_bl_pc_cheb_upper_length_upper_product_terminal + S (ff_upper_bl_pc_cheb_upper_length) = S ((S (ell)) * pa_v_bl_pc_cheb_upper_length_upper_product)) /\ exists pa_q_bl_pc_cheb_upper_length_upper_product_terminal. pa_u_bl_pc_cheb_upper_length_upper_product = pa_q_bl_pc_cheb_upper_length_upper_product_terminal * S ((S (ell)) * pa_v_bl_pc_cheb_upper_length_upper_product) + (ff_upper_bl_pc_cheb_upper_length))) /\ forall pa_i_bl_pc_cheb_upper_length_upper_product. (exists pa_lt_bl_pc_cheb_upper_length_upper_product_bound. pa_lt_bl_pc_cheb_upper_length_upper_product_bound + S pa_i_bl_pc_cheb_upper_length_upper_product = ell) -> exists pa_p_bl_pc_cheb_upper_length_upper_product pa_r_bl_pc_cheb_upper_length_upper_product pa_s_bl_pc_cheb_upper_length_upper_product. ((((exists pa_h_bl_pc_cheb_upper_length_upper_product_factor. pa_h_bl_pc_cheb_upper_length_upper_product_factor + S (pa_p_bl_pc_cheb_upper_length_upper_product) = S ((S (pa_i_bl_pc_cheb_upper_length_upper_product)) * pa_c_bl_pc_cheb_upper_length_upper)) /\ exists pa_q_bl_pc_cheb_upper_length_upper_product_factor. pa_b_bl_pc_cheb_upper_length_upper = pa_q_bl_pc_cheb_upper_length_upper_product_factor * S ((S (pa_i_bl_pc_cheb_upper_length_upper_product)) * pa_c_bl_pc_cheb_upper_length_upper) + (pa_p_bl_pc_cheb_upper_length_upper_product))) /\ ((((exists pa_h_bl_pc_cheb_upper_length_upper_product_partial. pa_h_bl_pc_cheb_upper_length_upper_product_partial + S (pa_r_bl_pc_cheb_upper_length_upper_product) = S ((S (pa_i_bl_pc_cheb_upper_length_upper_product)) * pa_v_bl_pc_cheb_upper_length_upper_product)) /\ exists pa_q_bl_pc_cheb_upper_length_upper_product_partial. pa_u_bl_pc_cheb_upper_length_upper_product = pa_q_bl_pc_cheb_upper_length_upper_product_partial * S ((S (pa_i_bl_pc_cheb_upper_length_upper_product)) * pa_v_bl_pc_cheb_upper_length_upper_product) + (pa_r_bl_pc_cheb_upper_length_upper_product))) /\ ((((exists pa_h_bl_pc_cheb_upper_length_upper_product_successor. pa_h_bl_pc_cheb_upper_length_upper_product_successor + S (pa_s_bl_pc_cheb_upper_length_upper_product) = S ((S (S pa_i_bl_pc_cheb_upper_length_upper_product)) * pa_v_bl_pc_cheb_upper_length_upper_product)) /\ exists pa_q_bl_pc_cheb_upper_length_upper_product_successor. pa_u_bl_pc_cheb_upper_length_upper_product = pa_q_bl_pc_cheb_upper_length_upper_product_successor * S ((S (S pa_i_bl_pc_cheb_upper_length_upper_product)) * pa_v_bl_pc_cheb_upper_length_upper_product) + (pa_s_bl_pc_cheb_upper_length_upper_product))) /\ pa_s_bl_pc_cheb_upper_length_upper_product = pa_r_bl_pc_cheb_upper_length_upper_product * pa_p_bl_pc_cheb_upper_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_pc_cheb_upper_length. ff_lower_gap_bl_pc_cheb_upper_length + (ff_lower_bl_pc_cheb_upper_length) = (N)) /\ (exists ff_upper_gap_bl_pc_cheb_upper_length. ff_upper_gap_bl_pc_cheb_upper_length + S (N) = (ff_upper_bl_pc_cheb_upper_length))))))))) -> (exists pc_code_cheb_upper_count pc_scale_cheb_upper_count. (forall pc_index_cheb_upper_count_mask. (exists pc_lt_cheb_upper_count_mask_bound. pc_lt_cheb_upper_count_mask_bound + S (pc_index_cheb_upper_count_mask) = (N)) -> exists pc_bit_cheb_upper_count_mask. (((exists fs_h_pc_cheb_upper_count_mask_entry. fs_h_pc_cheb_upper_count_mask_entry + S (pc_bit_cheb_upper_count_mask) = S ((S (pc_index_cheb_upper_count_mask)) * pc_scale_cheb_upper_count)) /\ exists fs_q_pc_cheb_upper_count_mask_entry. pc_code_cheb_upper_count = fs_q_pc_cheb_upper_count_mask_entry * S ((S (pc_index_cheb_upper_count_mask)) * pc_scale_cheb_upper_count) + (pc_bit_cheb_upper_count_mask))) /\ (((((~(S (pc_index_cheb_upper_count_mask) = 1) /\ forall bpr_left_pc_cheb_upper_count_mask_choice_prime bpr_right_pc_cheb_upper_count_mask_choice_prime. S (pc_index_cheb_upper_count_mask) = bpr_left_pc_cheb_upper_count_mask_choice_prime * bpr_right_pc_cheb_upper_count_mask_choice_prime -> bpr_left_pc_cheb_upper_count_mask_choice_prime = 1 \/ bpr_right_pc_cheb_upper_count_mask_choice_prime = 1)) /\ pc_bit_cheb_upper_count_mask = 1) \/ (~((~(S (pc_index_cheb_upper_count_mask) = 1) /\ forall bpr_left_pc_cheb_upper_count_mask_choice_prime bpr_right_pc_cheb_upper_count_mask_choice_prime. S (pc_index_cheb_upper_count_mask) = bpr_left_pc_cheb_upper_count_mask_choice_prime * bpr_right_pc_cheb_upper_count_mask_choice_prime -> bpr_left_pc_cheb_upper_count_mask_choice_prime = 1 \/ bpr_right_pc_cheb_upper_count_mask_choice_prime = 1)) /\ pc_bit_cheb_upper_count_mask = 0)))) /\ (exists fs_u_pc_cheb_upper_count_sum fs_v_pc_cheb_upper_count_sum. ((((exists fs_h_pc_cheb_upper_count_sum_body_start. fs_h_pc_cheb_upper_count_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_cheb_upper_count_sum)) /\ exists fs_q_pc_cheb_upper_count_sum_body_start. fs_u_pc_cheb_upper_count_sum = fs_q_pc_cheb_upper_count_sum_body_start * S ((S (0)) * fs_v_pc_cheb_upper_count_sum) + (0))) /\ ((((exists fs_h_pc_cheb_upper_count_sum_body_terminal. fs_h_pc_cheb_upper_count_sum_body_terminal + S (k) = S ((S (N)) * fs_v_pc_cheb_upper_count_sum)) /\ exists fs_q_pc_cheb_upper_count_sum_body_terminal. fs_u_pc_cheb_upper_count_sum = fs_q_pc_cheb_upper_count_sum_body_terminal * S ((S (N)) * fs_v_pc_cheb_upper_count_sum) + (k))) /\ forall fs_i_pc_cheb_upper_count_sum_body_steps. (exists fs_lt_pc_cheb_upper_count_sum_body_steps_bound. fs_lt_pc_cheb_upper_count_sum_body_steps_bound + S fs_i_pc_cheb_upper_count_sum_body_steps = N) -> exists fs_a_pc_cheb_upper_count_sum_body_steps fs_r_pc_cheb_upper_count_sum_body_steps fs_s_pc_cheb_upper_count_sum_body_steps. ((((exists fs_h_pc_cheb_upper_count_sum_body_steps_summand. fs_h_pc_cheb_upper_count_sum_body_steps_summand + S (fs_a_pc_cheb_upper_count_sum_body_steps) = S ((S (fs_i_pc_cheb_upper_count_sum_body_steps)) * pc_scale_cheb_upper_count)) /\ exists fs_q_pc_cheb_upper_count_sum_body_steps_summand. pc_code_cheb_upper_count = fs_q_pc_cheb_upper_count_sum_body_steps_summand * S ((S (fs_i_pc_cheb_upper_count_sum_body_steps)) * pc_scale_cheb_upper_count) + (fs_a_pc_cheb_upper_count_sum_body_steps))) /\ ((((exists fs_h_pc_cheb_upper_count_sum_body_steps_partial. fs_h_pc_cheb_upper_count_sum_body_steps_partial + S (fs_r_pc_cheb_upper_count_sum_body_steps) = S ((S (fs_i_pc_cheb_upper_count_sum_body_steps)) * fs_v_pc_cheb_upper_count_sum)) /\ exists fs_q_pc_cheb_upper_count_sum_body_steps_partial. fs_u_pc_cheb_upper_count_sum = fs_q_pc_cheb_upper_count_sum_body_steps_partial * S ((S (fs_i_pc_cheb_upper_count_sum_body_steps)) * fs_v_pc_cheb_upper_count_sum) + (fs_r_pc_cheb_upper_count_sum_body_steps))) /\ ((((exists fs_h_pc_cheb_upper_count_sum_body_steps_successor. fs_h_pc_cheb_upper_count_sum_body_steps_successor + S (fs_s_pc_cheb_upper_count_sum_body_steps) = S ((S (S fs_i_pc_cheb_upper_count_sum_body_steps)) * fs_v_pc_cheb_upper_count_sum)) /\ exists fs_q_pc_cheb_upper_count_sum_body_steps_successor. fs_u_pc_cheb_upper_count_sum = fs_q_pc_cheb_upper_count_sum_body_steps_successor * S ((S (S fs_i_pc_cheb_upper_count_sum_body_steps)) * fs_v_pc_cheb_upper_count_sum) + (fs_s_pc_cheb_upper_count_sum_body_steps))) /\ fs_s_pc_cheb_upper_count_sum_body_steps = fs_r_pc_cheb_upper_count_sum_body_steps + fs_a_pc_cheb_upper_count_sum_body_steps))))))) -> (exists pc_le_cheb_upper_result. pc_le_cheb_upper_result + (k * ell) = (8 * N))

Constructive proof overview

Generated structural guide

The exact effective Chebyshev upper bound pi(N)*BitLen(N) <= 8N, including every N at least two.

The unchanged tactic script uses 17 declared prerequisites and contains 145 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_or_lt Stable theorem; checked-use authorized PC0009 prime_count_bounded mul_le_mul Alpha theorem; checked-use authorized mul_le_mul_left Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized PC0025 binary_length_nonzero_components le_zero Stable theorem; checked-use authorized binary_exponent_split_exists Alpha theorem; checked-use authorized pow_exists Stable theorem; checked-use authorized PC0026 binary_half_scale_bounds PC0013 beta_cutoff_prefix_exists beta_sum_exists Stable theorem; checked-use authorized PC0014 beta_cutoff_count_comparison PC0007 prime_bit_prefix_all_bits PC0028 prime_cutoff_exponent_bound PC0029 chebyshev_upper_arithmetic

Direct dependents

PC0031 prime_count_chebyshev_bounds

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

145 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 (8)
prime count boundedbinary length nonzero componentsbinary half scale boundsbeta cutoff prefix existsbeta cutoff count comparisonprime bit prefix all bitsprime cutoff exponent boundchebyshev upper arithmetic

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 ell
  3. L3
    intro k
  4. L4
    intro hN
  5. L5
    intro hl
  6. L6
    intro hk
02Establish hcL7–10

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

  1. L7
    have hc : (exists g. g + ell = 4) \/ (exists g. g + S 4 = ell)
  2. L8
    specialize le_or_lt ell
  3. L9
    specialize le_or_lt 4
  4. L10
    apply le_or_lt
03Separate the logical casesL11–11

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

  1. L11
    cases hc
04Establish hsmallL12–21

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

  1. L12
    have hsmall : exists g. g + k * ell = N * 4
  2. L13
    specialize mul_le_mul k
  3. L14
    specialize mul_le_mul N
  4. L15
    specialize mul_le_mul ell
  5. L16
    specialize mul_le_mul 4
  6. L17
    apply mul_le_mul
  7. L18
    specialize prime_count_bounded N
  8. L19
    specialize prime_count_bounded k
  9. L20
    apply prime_count_bounded
  10. L21
    exact hk
05Use earlier factsL22–22

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

  1. L22
    exact hc_left
06Establish hscaleL23–27

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

  1. L23
    have hscale : exists g. g + N * 4 = N * 8
  2. L24
    specialize mul_le_mul_left 4
  3. L25
    specialize mul_le_mul_left 8
  4. L26
    specialize mul_le_mul_left N
  5. L27
    apply mul_le_mul_left
07Construct an explicit witnessL28–28

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

  1. L28
    exists 4
08Calculate and transport equalitiesL29–29

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

  1. L29
    norm_num
09Establish hswapL30–38

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

  1. L30
    have hswap : N * 8 = 8 * N
  2. L31
    apply mul_comm
  3. L32
    rewrite hswap at hscale
  4. L33
    specialize le_trans (k * ell)
  5. L34
    specialize le_trans (N * 4)
  6. L35
    specialize le_trans (8 * N)
  7. L36
    apply le_trans
  8. L37
    exact hsmall
  9. L38
    exact hscale
10Establish hdataL39–43

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

  1. L39
    have hdata : ∃ e. ∃ v. ∃ w. ell = S e ∧ (PowTwo(e,v) ∧ (PowTwo(ell,w) ∧ (Le(v,N) ∧ Lt(N,w))))Definitions: PowTwoLeLt
  2. L40
    specialize binary_length_nonzero_components N
  3. L41
    specialize binary_length_nonzero_components ell
  4. L42
    apply binary_length_nonzero_components
  5. L43
    intro hz
11Establish hbadL44–51

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

  1. L44
    have hbad : exists g. g + 2 = 0
  2. L45
    rewrite hz at hN
  3. L46
    exact hN
  4. L47
    apply PA1
  5. L48
    specialize le_zero 2
  6. L49
    apply le_zero
  7. L50
    exact hbad
  8. L51
    exact hl
12Separate the logical casesL52–58

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

  1. L52
    cases hdata
  2. L53
    cases hdata_witness
  3. L54
    cases hdata_witness_witness
  4. L55
    cases hdata_witness_witness_witness
  5. L56
    cases hdata_witness_witness_witness_right
  6. L57
    cases hdata_witness_witness_witness_right_right
  7. L58
    cases hdata_witness_witness_witness_right_right_right
13Establish hsplitL59–61

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

  1. L59
    have hsplit : exists h d. (d = 0 \/ d = 1) /\ x = (h + h) + d
  2. L60
    specialize binary_exponent_split_exists x
  3. L61
    apply binary_exponent_split_exists
14Separate the logical casesL62–64

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

  1. L62
    cases hsplit
  2. L63
    cases hsplit_witness
  3. L64
    cases hsplit_witness_witness
15Establish hUL65–68

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

  1. L65
    have hU : ∃ U. PowTwo(x3,U)Definitions: PowTwo
  2. L66
    specialize pow_exists 2
  3. L67
    specialize pow_exists x3
  4. L68
    apply pow_exists
16Separate the logical casesL69–69

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

  1. L69
    cases hU
17Establish hscaleL70–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary half scale bounds.

  1. L70
    have hscale : (exists g. g + 2 = x3) /\ ((exists g. g + x5 * x5 = N) /\ ((exists g. g + ell = 2 * x5) /\ (exists g. g + ell = 3 * x3)))
  2. L71
    specialize binary_half_scale_bounds N
  3. L72
    specialize binary_half_scale_bounds ell
  4. L73
    specialize binary_half_scale_bounds x
  5. L74
    specialize binary_half_scale_bounds x3
  6. L75
    specialize binary_half_scale_bounds x4
  7. L76
    specialize binary_half_scale_bounds x5
  8. L77
    specialize binary_half_scale_bounds x1
  9. L78
    apply binary_half_scale_bounds
  10. L79
    exact hdata_witness_witness_witness_left
18Use earlier factsL80–85

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

  1. L80
    exact hsplit_witness_witness_right
  2. L81
    exact hsplit_witness_witness_left
  3. L82
    exact hc_right
  4. L83
    exact hU_witness
  5. L84
    exact hdata_witness_witness_witness_right_left
  6. L85
    exact hdata_witness_witness_witness_right_right_right_left
19Separate the logical casesL86–91

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

  1. L86
    cases hscale
  2. L87
    cases hscale_right
  3. L88
    cases hscale_right_right
  4. L89
    cases hk
  5. L90
    cases hk_witness
  6. L91
    cases hk_witness_witness
20Establish hcutL92–97

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

  1. L92
    have hcut : ∃ d. ∃ f. BetaCutoffPrefix(x5,x6,x7,d,f,N)Definitions: BetaCutoffPrefix
  2. L93
    specialize beta_cutoff_prefix_exists x5
  3. L94
    specialize beta_cutoff_prefix_exists x6
  4. L95
    specialize beta_cutoff_prefix_exists x7
  5. L96
    specialize beta_cutoff_prefix_exists N
  6. L97
    apply beta_cutoff_prefix_exists
21Separate the logical casesL98–99

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

  1. L98
    cases hcut
  2. L99
    cases hcut_witness
22Establish hsumL100–104

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

  1. L100
    have hsum : ∃ L. Sum(x8,x9,N,L)Definitions: Sum
  2. L101
    specialize beta_sum_exists x8
  3. L102
    specialize beta_sum_exists x9
  4. L103
    specialize beta_sum_exists N
  5. L104
    apply beta_sum_exists
23Separate the logical casesL105–105

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

  1. L105
    cases hsum
24Use earlier factsL106–115

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

  1. L106
    specialize chebyshev_upper_arithmetic N
  2. L107
    specialize chebyshev_upper_arithmetic ell
  3. L108
    specialize chebyshev_upper_arithmetic k
  4. L109
    specialize chebyshev_upper_arithmetic x3
  5. L110
    specialize chebyshev_upper_arithmetic x5
  6. L111
    specialize chebyshev_upper_arithmetic x10
  7. L112
    apply chebyshev_upper_arithmetic
  8. L113
    specialize beta_cutoff_count_comparison x5
  9. L114
    specialize beta_cutoff_count_comparison x6
  10. L115
    specialize beta_cutoff_count_comparison x7
25Use earlier factsL116–125

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

  1. L116
    specialize beta_cutoff_count_comparison x8
  2. L117
    specialize beta_cutoff_count_comparison x9
  3. L118
    specialize beta_cutoff_count_comparison N
  4. L119
    specialize beta_cutoff_count_comparison k
  5. L120
    specialize beta_cutoff_count_comparison x10
  6. L121
    apply beta_cutoff_count_comparison
  7. L122
    specialize prime_bit_prefix_all_bits x6
  8. L123
    specialize prime_bit_prefix_all_bits x7
  9. L124
    specialize prime_bit_prefix_all_bits N
  10. L125
    apply prime_bit_prefix_all_bits
26Use earlier factsL126–135

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

  1. L126
    exact hk_witness_witness_left
  2. L127
    exact hcut_witness_witness
  3. L128
    exact hk_witness_witness_right
  4. L129
    exact hsum_witness
  5. L130
    exact hscale_right_left
  6. L131
    exact hscale_right_right_left
  7. L132
    exact hscale_right_right_right
  8. L133
    specialize prime_cutoff_exponent_bound N
  9. L134
    specialize prime_cutoff_exponent_bound x3
  10. L135
    specialize prime_cutoff_exponent_bound x5
27Use earlier factsL136–145

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

  1. L136
    specialize prime_cutoff_exponent_bound x6
  2. L137
    specialize prime_cutoff_exponent_bound x7
  3. L138
    specialize prime_cutoff_exponent_bound x8
  4. L139
    specialize prime_cutoff_exponent_bound x9
  5. L140
    specialize prime_cutoff_exponent_bound x10
  6. L141
    apply prime_cutoff_exponent_bound
  7. L142
    exact hU_witness
  8. L143
    exact hk_witness_witness_left
  9. L144
    exact hcut_witness_witness
  10. L145
    exact hsum_witness

Library-wide reading audit

Original exact command ledger · 145 lines
  1. 0001intro N
  2. 0002intro ell
  3. 0003intro k
  4. 0004intro hN
  5. 0005intro hl
  6. 0006intro hk
  7. 0007have hc : (exists g. g + ell = 4) \/ (exists g. g + S 4 = ell)
  8. 0008specialize le_or_lt ell
  9. 0009specialize le_or_lt 4
  10. 0010apply le_or_lt
  11. 0011cases hc
  12. 0012have hsmall : exists g. g + k * ell = N * 4
  13. 0013specialize mul_le_mul k
  14. 0014specialize mul_le_mul N
  15. 0015specialize mul_le_mul ell
  16. 0016specialize mul_le_mul 4
  17. 0017apply mul_le_mul
  18. 0018specialize prime_count_bounded N
  19. 0019specialize prime_count_bounded k
  20. 0020apply prime_count_bounded
  21. 0021exact hk
  22. 0022exact hc_left
  23. 0023have hscale : exists g. g + N * 4 = N * 8
  24. 0024specialize mul_le_mul_left 4
  25. 0025specialize mul_le_mul_left 8
  26. 0026specialize mul_le_mul_left N
  27. 0027apply mul_le_mul_left
  28. 0028exists 4
  29. 0029norm_num
  30. 0030have hswap : N * 8 = 8 * N
  31. 0031apply mul_comm
  32. 0032rewrite hswap at hscale
  33. 0033specialize le_trans (k * ell)
  34. 0034specialize le_trans (N * 4)
  35. 0035specialize le_trans (8 * N)
  36. 0036apply le_trans
  37. 0037exact hsmall
  38. 0038exact hscale
  39. 0039have hdata : exists e v w. ell = S e /\ ((exists pa_b_pc_cheb_upper_lower_power pa_c_pc_cheb_upper_lower_power. ((forall pa_i_pc_cheb_upper_lower_power_repeat. (exists pa_lt_pc_cheb_upper_lower_power_repeat_bound. pa_lt_pc_cheb_upper_lower_power_repeat_bound + S pa_i_pc_cheb_upper_lower_power_repeat = e) -> (((exists pa_h_pc_cheb_upper_lower_power_repeat_decoded. pa_h_pc_cheb_upper_lower_power_repeat_decoded + S (2) = S ((S (pa_i_pc_cheb_upper_lower_power_repeat)) * pa_c_pc_cheb_upper_lower_power)) /\ exists pa_q_pc_cheb_upper_lower_power_repeat_decoded. pa_b_pc_cheb_upper_lower_power = pa_q_pc_cheb_upper_lower_power_repeat_decoded * S ((S (pa_i_pc_cheb_upper_lower_power_repeat)) * pa_c_pc_cheb_upper_lower_power) + (2)))) /\ (exists pa_u_pc_cheb_upper_lower_power_product pa_v_pc_cheb_upper_lower_power_product. ((((exists pa_h_pc_cheb_upper_lower_power_product_start. pa_h_pc_cheb_upper_lower_power_product_start + S (1) = S ((S (0)) * pa_v_pc_cheb_upper_lower_power_product)) /\ exists pa_q_pc_cheb_upper_lower_power_product_start. pa_u_pc_cheb_upper_lower_power_product = pa_q_pc_cheb_upper_lower_power_product_start * S ((S (0)) * pa_v_pc_cheb_upper_lower_power_product) + (1))) /\ ((((exists pa_h_pc_cheb_upper_lower_power_product_terminal. pa_h_pc_cheb_upper_lower_power_product_terminal + S (v) = S ((S (e)) * pa_v_pc_cheb_upper_lower_power_product)) /\ exists pa_q_pc_cheb_upper_lower_power_product_terminal. pa_u_pc_cheb_upper_lower_power_product = pa_q_pc_cheb_upper_lower_power_product_terminal * S ((S (e)) * pa_v_pc_cheb_upper_lower_power_product) + (v))) /\ forall pa_i_pc_cheb_upper_lower_power_product. (exists pa_lt_pc_cheb_upper_lower_power_product_bound. pa_lt_pc_cheb_upper_lower_power_product_bound + S pa_i_pc_cheb_upper_lower_power_product = e) -> exists pa_p_pc_cheb_upper_lower_power_product pa_r_pc_cheb_upper_lower_power_product pa_s_pc_cheb_upper_lower_power_product. ((((exists pa_h_pc_cheb_upper_lower_power_product_factor. pa_h_pc_cheb_upper_lower_power_product_factor + S (pa_p_pc_cheb_upper_lower_power_product) = S ((S (pa_i_pc_cheb_upper_lower_power_product)) * pa_c_pc_cheb_upper_lower_power)) /\ exists pa_q_pc_cheb_upper_lower_power_product_factor. pa_b_pc_cheb_upper_lower_power = pa_q_pc_cheb_upper_lower_power_product_factor * S ((S (pa_i_pc_cheb_upper_lower_power_product)) * pa_c_pc_cheb_upper_lower_power) + (pa_p_pc_cheb_upper_lower_power_product))) /\ ((((exists pa_h_pc_cheb_upper_lower_power_product_partial. pa_h_pc_cheb_upper_lower_power_product_partial + S (pa_r_pc_cheb_upper_lower_power_product) = S ((S (pa_i_pc_cheb_upper_lower_power_product)) * pa_v_pc_cheb_upper_lower_power_product)) /\ exists pa_q_pc_cheb_upper_lower_power_product_partial. pa_u_pc_cheb_upper_lower_power_product = pa_q_pc_cheb_upper_lower_power_product_partial * S ((S (pa_i_pc_cheb_upper_lower_power_product)) * pa_v_pc_cheb_upper_lower_power_product) + (pa_r_pc_cheb_upper_lower_power_product))) /\ ((((exists pa_h_pc_cheb_upper_lower_power_product_successor. pa_h_pc_cheb_upper_lower_power_product_successor + S (pa_s_pc_cheb_upper_lower_power_product) = S ((S (S pa_i_pc_cheb_upper_lower_power_product)) * pa_v_pc_cheb_upper_lower_power_product)) /\ exists pa_q_pc_cheb_upper_lower_power_product_successor. pa_u_pc_cheb_upper_lower_power_product = pa_q_pc_cheb_upper_lower_power_product_successor * S ((S (S pa_i_pc_cheb_upper_lower_power_product)) * pa_v_pc_cheb_upper_lower_power_product) + (pa_s_pc_cheb_upper_lower_power_product))) /\ pa_s_pc_cheb_upper_lower_power_product = pa_r_pc_cheb_upper_lower_power_product * pa_p_pc_cheb_upper_lower_power_product)))))))) /\ ((exists pa_b_pc_cheb_upper_upper_power pa_c_pc_cheb_upper_upper_power. ((forall pa_i_pc_cheb_upper_upper_power_repeat. (exists pa_lt_pc_cheb_upper_upper_power_repeat_bound. pa_lt_pc_cheb_upper_upper_power_repeat_bound + S pa_i_pc_cheb_upper_upper_power_repeat = ell) -> (((exists pa_h_pc_cheb_upper_upper_power_repeat_decoded. pa_h_pc_cheb_upper_upper_power_repeat_decoded + S (2) = S ((S (pa_i_pc_cheb_upper_upper_power_repeat)) * pa_c_pc_cheb_upper_upper_power)) /\ exists pa_q_pc_cheb_upper_upper_power_repeat_decoded. pa_b_pc_cheb_upper_upper_power = pa_q_pc_cheb_upper_upper_power_repeat_decoded * S ((S (pa_i_pc_cheb_upper_upper_power_repeat)) * pa_c_pc_cheb_upper_upper_power) + (2)))) /\ (exists pa_u_pc_cheb_upper_upper_power_product pa_v_pc_cheb_upper_upper_power_product. ((((exists pa_h_pc_cheb_upper_upper_power_product_start. pa_h_pc_cheb_upper_upper_power_product_start + S (1) = S ((S (0)) * pa_v_pc_cheb_upper_upper_power_product)) /\ exists pa_q_pc_cheb_upper_upper_power_product_start. pa_u_pc_cheb_upper_upper_power_product = pa_q_pc_cheb_upper_upper_power_product_start * S ((S (0)) * pa_v_pc_cheb_upper_upper_power_product) + (1))) /\ ((((exists pa_h_pc_cheb_upper_upper_power_product_terminal. pa_h_pc_cheb_upper_upper_power_product_terminal + S (w) = S ((S (ell)) * pa_v_pc_cheb_upper_upper_power_product)) /\ exists pa_q_pc_cheb_upper_upper_power_product_terminal. pa_u_pc_cheb_upper_upper_power_product = pa_q_pc_cheb_upper_upper_power_product_terminal * S ((S (ell)) * pa_v_pc_cheb_upper_upper_power_product) + (w))) /\ forall pa_i_pc_cheb_upper_upper_power_product. (exists pa_lt_pc_cheb_upper_upper_power_product_bound. pa_lt_pc_cheb_upper_upper_power_product_bound + S pa_i_pc_cheb_upper_upper_power_product = ell) -> exists pa_p_pc_cheb_upper_upper_power_product pa_r_pc_cheb_upper_upper_power_product pa_s_pc_cheb_upper_upper_power_product. ((((exists pa_h_pc_cheb_upper_upper_power_product_factor. pa_h_pc_cheb_upper_upper_power_product_factor + S (pa_p_pc_cheb_upper_upper_power_product) = S ((S (pa_i_pc_cheb_upper_upper_power_product)) * pa_c_pc_cheb_upper_upper_power)) /\ exists pa_q_pc_cheb_upper_upper_power_product_factor. pa_b_pc_cheb_upper_upper_power = pa_q_pc_cheb_upper_upper_power_product_factor * S ((S (pa_i_pc_cheb_upper_upper_power_product)) * pa_c_pc_cheb_upper_upper_power) + (pa_p_pc_cheb_upper_upper_power_product))) /\ ((((exists pa_h_pc_cheb_upper_upper_power_product_partial. pa_h_pc_cheb_upper_upper_power_product_partial + S (pa_r_pc_cheb_upper_upper_power_product) = S ((S (pa_i_pc_cheb_upper_upper_power_product)) * pa_v_pc_cheb_upper_upper_power_product)) /\ exists pa_q_pc_cheb_upper_upper_power_product_partial. pa_u_pc_cheb_upper_upper_power_product = pa_q_pc_cheb_upper_upper_power_product_partial * S ((S (pa_i_pc_cheb_upper_upper_power_product)) * pa_v_pc_cheb_upper_upper_power_product) + (pa_r_pc_cheb_upper_upper_power_product))) /\ ((((exists pa_h_pc_cheb_upper_upper_power_product_successor. pa_h_pc_cheb_upper_upper_power_product_successor + S (pa_s_pc_cheb_upper_upper_power_product) = S ((S (S pa_i_pc_cheb_upper_upper_power_product)) * pa_v_pc_cheb_upper_upper_power_product)) /\ exists pa_q_pc_cheb_upper_upper_power_product_successor. pa_u_pc_cheb_upper_upper_power_product = pa_q_pc_cheb_upper_upper_power_product_successor * S ((S (S pa_i_pc_cheb_upper_upper_power_product)) * pa_v_pc_cheb_upper_upper_power_product) + (pa_s_pc_cheb_upper_upper_power_product))) /\ pa_s_pc_cheb_upper_upper_power_product = pa_r_pc_cheb_upper_upper_power_product * pa_p_pc_cheb_upper_upper_power_product)))))))) /\ ((exists pc_le_cheb_upper_lower_value. pc_le_cheb_upper_lower_value + (v) = (N)) /\ (exists pc_lt_cheb_upper_upper_value. pc_lt_cheb_upper_upper_value + S (N) = (w)))))
  40. 0040specialize binary_length_nonzero_components N
  41. 0041specialize binary_length_nonzero_components ell
  42. 0042apply binary_length_nonzero_components
  43. 0043intro hz
  44. 0044have hbad : exists g. g + 2 = 0
  45. 0045rewrite hz at hN
  46. 0046exact hN
  47. 0047apply PA1
  48. 0048specialize le_zero 2
  49. 0049apply le_zero
  50. 0050exact hbad
  51. 0051exact hl
  52. 0052cases hdata
  53. 0053cases hdata_witness
  54. 0054cases hdata_witness_witness
  55. 0055cases hdata_witness_witness_witness
  56. 0056cases hdata_witness_witness_witness_right
  57. 0057cases hdata_witness_witness_witness_right_right
  58. 0058cases hdata_witness_witness_witness_right_right_right
  59. 0059have hsplit : exists h d. (d = 0 \/ d = 1) /\ x = (h + h) + d
  60. 0060specialize binary_exponent_split_exists x
  61. 0061apply binary_exponent_split_exists
  62. 0062cases hsplit
  63. 0063cases hsplit_witness
  64. 0064cases hsplit_witness_witness
  65. 0065have hU : exists U. exists pa_b_pc_cheb_upper_threshold pa_c_pc_cheb_upper_threshold. ((forall pa_i_pc_cheb_upper_threshold_repeat. (exists pa_lt_pc_cheb_upper_threshold_repeat_bound. pa_lt_pc_cheb_upper_threshold_repeat_bound + S pa_i_pc_cheb_upper_threshold_repeat = x3) -> (((exists pa_h_pc_cheb_upper_threshold_repeat_decoded. pa_h_pc_cheb_upper_threshold_repeat_decoded + S (2) = S ((S (pa_i_pc_cheb_upper_threshold_repeat)) * pa_c_pc_cheb_upper_threshold)) /\ exists pa_q_pc_cheb_upper_threshold_repeat_decoded. pa_b_pc_cheb_upper_threshold = pa_q_pc_cheb_upper_threshold_repeat_decoded * S ((S (pa_i_pc_cheb_upper_threshold_repeat)) * pa_c_pc_cheb_upper_threshold) + (2)))) /\ (exists pa_u_pc_cheb_upper_threshold_product pa_v_pc_cheb_upper_threshold_product. ((((exists pa_h_pc_cheb_upper_threshold_product_start. pa_h_pc_cheb_upper_threshold_product_start + S (1) = S ((S (0)) * pa_v_pc_cheb_upper_threshold_product)) /\ exists pa_q_pc_cheb_upper_threshold_product_start. pa_u_pc_cheb_upper_threshold_product = pa_q_pc_cheb_upper_threshold_product_start * S ((S (0)) * pa_v_pc_cheb_upper_threshold_product) + (1))) /\ ((((exists pa_h_pc_cheb_upper_threshold_product_terminal. pa_h_pc_cheb_upper_threshold_product_terminal + S (U) = S ((S (x3)) * pa_v_pc_cheb_upper_threshold_product)) /\ exists pa_q_pc_cheb_upper_threshold_product_terminal. pa_u_pc_cheb_upper_threshold_product = pa_q_pc_cheb_upper_threshold_product_terminal * S ((S (x3)) * pa_v_pc_cheb_upper_threshold_product) + (U))) /\ forall pa_i_pc_cheb_upper_threshold_product. (exists pa_lt_pc_cheb_upper_threshold_product_bound. pa_lt_pc_cheb_upper_threshold_product_bound + S pa_i_pc_cheb_upper_threshold_product = x3) -> exists pa_p_pc_cheb_upper_threshold_product pa_r_pc_cheb_upper_threshold_product pa_s_pc_cheb_upper_threshold_product. ((((exists pa_h_pc_cheb_upper_threshold_product_factor. pa_h_pc_cheb_upper_threshold_product_factor + S (pa_p_pc_cheb_upper_threshold_product) = S ((S (pa_i_pc_cheb_upper_threshold_product)) * pa_c_pc_cheb_upper_threshold)) /\ exists pa_q_pc_cheb_upper_threshold_product_factor. pa_b_pc_cheb_upper_threshold = pa_q_pc_cheb_upper_threshold_product_factor * S ((S (pa_i_pc_cheb_upper_threshold_product)) * pa_c_pc_cheb_upper_threshold) + (pa_p_pc_cheb_upper_threshold_product))) /\ ((((exists pa_h_pc_cheb_upper_threshold_product_partial. pa_h_pc_cheb_upper_threshold_product_partial + S (pa_r_pc_cheb_upper_threshold_product) = S ((S (pa_i_pc_cheb_upper_threshold_product)) * pa_v_pc_cheb_upper_threshold_product)) /\ exists pa_q_pc_cheb_upper_threshold_product_partial. pa_u_pc_cheb_upper_threshold_product = pa_q_pc_cheb_upper_threshold_product_partial * S ((S (pa_i_pc_cheb_upper_threshold_product)) * pa_v_pc_cheb_upper_threshold_product) + (pa_r_pc_cheb_upper_threshold_product))) /\ ((((exists pa_h_pc_cheb_upper_threshold_product_successor. pa_h_pc_cheb_upper_threshold_product_successor + S (pa_s_pc_cheb_upper_threshold_product) = S ((S (S pa_i_pc_cheb_upper_threshold_product)) * pa_v_pc_cheb_upper_threshold_product)) /\ exists pa_q_pc_cheb_upper_threshold_product_successor. pa_u_pc_cheb_upper_threshold_product = pa_q_pc_cheb_upper_threshold_product_successor * S ((S (S pa_i_pc_cheb_upper_threshold_product)) * pa_v_pc_cheb_upper_threshold_product) + (pa_s_pc_cheb_upper_threshold_product))) /\ pa_s_pc_cheb_upper_threshold_product = pa_r_pc_cheb_upper_threshold_product * pa_p_pc_cheb_upper_threshold_product)))))))
  66. 0066specialize pow_exists 2
  67. 0067specialize pow_exists x3
  68. 0068apply pow_exists
  69. 0069cases hU
  70. 0070have hscale : (exists g. g + 2 = x3) /\ ((exists g. g + x5 * x5 = N) /\ ((exists g. g + ell = 2 * x5) /\ (exists g. g + ell = 3 * x3)))
  71. 0071specialize binary_half_scale_bounds N
  72. 0072specialize binary_half_scale_bounds ell
  73. 0073specialize binary_half_scale_bounds x
  74. 0074specialize binary_half_scale_bounds x3
  75. 0075specialize binary_half_scale_bounds x4
  76. 0076specialize binary_half_scale_bounds x5
  77. 0077specialize binary_half_scale_bounds x1
  78. 0078apply binary_half_scale_bounds
  79. 0079exact hdata_witness_witness_witness_left
  80. 0080exact hsplit_witness_witness_right
  81. 0081exact hsplit_witness_witness_left
  82. 0082exact hc_right
  83. 0083exact hU_witness
  84. 0084exact hdata_witness_witness_witness_right_left
  85. 0085exact hdata_witness_witness_witness_right_right_right_left
  86. 0086cases hscale
  87. 0087cases hscale_right
  88. 0088cases hscale_right_right
  89. 0089cases hk
  90. 0090cases hk_witness
  91. 0091cases hk_witness_witness
  92. 0092have hcut : exists d f. forall pc_index_cheb_upper_cutoff. (exists pc_lt_cheb_upper_cutoff_bound. pc_lt_cheb_upper_cutoff_bound + S (pc_index_cheb_upper_cutoff) = (N)) -> exists pc_bit_cheb_upper_cutoff. (((exists fs_h_pc_cheb_upper_cutoff_entry. fs_h_pc_cheb_upper_cutoff_entry + S (pc_bit_cheb_upper_cutoff) = S ((S (pc_index_cheb_upper_cutoff)) * f)) /\ exists fs_q_pc_cheb_upper_cutoff_entry. d = fs_q_pc_cheb_upper_cutoff_entry * S ((S (pc_index_cheb_upper_cutoff)) * f) + (pc_bit_cheb_upper_cutoff))) /\ ((((exists pc_lt_cheb_upper_cutoff_choice_below. pc_lt_cheb_upper_cutoff_choice_below + S (pc_index_cheb_upper_cutoff) = (x5)) /\ pc_bit_cheb_upper_cutoff = 0) \/ ((exists pc_le_cheb_upper_cutoff_choice_above. pc_le_cheb_upper_cutoff_choice_above + (x5) = (pc_index_cheb_upper_cutoff)) /\ (((exists fs_h_pc_cheb_upper_cutoff_choice_source. fs_h_pc_cheb_upper_cutoff_choice_source + S (pc_bit_cheb_upper_cutoff) = S ((S (pc_index_cheb_upper_cutoff)) * x7)) /\ exists fs_q_pc_cheb_upper_cutoff_choice_source. x6 = fs_q_pc_cheb_upper_cutoff_choice_source * S ((S (pc_index_cheb_upper_cutoff)) * x7) + (pc_bit_cheb_upper_cutoff))))))
  93. 0093specialize beta_cutoff_prefix_exists x5
  94. 0094specialize beta_cutoff_prefix_exists x6
  95. 0095specialize beta_cutoff_prefix_exists x7
  96. 0096specialize beta_cutoff_prefix_exists N
  97. 0097apply beta_cutoff_prefix_exists
  98. 0098cases hcut
  99. 0099cases hcut_witness
  100. 0100have hsum : exists L. exists fs_u_pc_cheb_upper_tail_count fs_v_pc_cheb_upper_tail_count. ((((exists fs_h_pc_cheb_upper_tail_count_body_start. fs_h_pc_cheb_upper_tail_count_body_start + S (0) = S ((S (0)) * fs_v_pc_cheb_upper_tail_count)) /\ exists fs_q_pc_cheb_upper_tail_count_body_start. fs_u_pc_cheb_upper_tail_count = fs_q_pc_cheb_upper_tail_count_body_start * S ((S (0)) * fs_v_pc_cheb_upper_tail_count) + (0))) /\ ((((exists fs_h_pc_cheb_upper_tail_count_body_terminal. fs_h_pc_cheb_upper_tail_count_body_terminal + S (L) = S ((S (N)) * fs_v_pc_cheb_upper_tail_count)) /\ exists fs_q_pc_cheb_upper_tail_count_body_terminal. fs_u_pc_cheb_upper_tail_count = fs_q_pc_cheb_upper_tail_count_body_terminal * S ((S (N)) * fs_v_pc_cheb_upper_tail_count) + (L))) /\ forall fs_i_pc_cheb_upper_tail_count_body_steps. (exists fs_lt_pc_cheb_upper_tail_count_body_steps_bound. fs_lt_pc_cheb_upper_tail_count_body_steps_bound + S fs_i_pc_cheb_upper_tail_count_body_steps = N) -> exists fs_a_pc_cheb_upper_tail_count_body_steps fs_r_pc_cheb_upper_tail_count_body_steps fs_s_pc_cheb_upper_tail_count_body_steps. ((((exists fs_h_pc_cheb_upper_tail_count_body_steps_summand. fs_h_pc_cheb_upper_tail_count_body_steps_summand + S (fs_a_pc_cheb_upper_tail_count_body_steps) = S ((S (fs_i_pc_cheb_upper_tail_count_body_steps)) * x9)) /\ exists fs_q_pc_cheb_upper_tail_count_body_steps_summand. x8 = fs_q_pc_cheb_upper_tail_count_body_steps_summand * S ((S (fs_i_pc_cheb_upper_tail_count_body_steps)) * x9) + (fs_a_pc_cheb_upper_tail_count_body_steps))) /\ ((((exists fs_h_pc_cheb_upper_tail_count_body_steps_partial. fs_h_pc_cheb_upper_tail_count_body_steps_partial + S (fs_r_pc_cheb_upper_tail_count_body_steps) = S ((S (fs_i_pc_cheb_upper_tail_count_body_steps)) * fs_v_pc_cheb_upper_tail_count)) /\ exists fs_q_pc_cheb_upper_tail_count_body_steps_partial. fs_u_pc_cheb_upper_tail_count = fs_q_pc_cheb_upper_tail_count_body_steps_partial * S ((S (fs_i_pc_cheb_upper_tail_count_body_steps)) * fs_v_pc_cheb_upper_tail_count) + (fs_r_pc_cheb_upper_tail_count_body_steps))) /\ ((((exists fs_h_pc_cheb_upper_tail_count_body_steps_successor. fs_h_pc_cheb_upper_tail_count_body_steps_successor + S (fs_s_pc_cheb_upper_tail_count_body_steps) = S ((S (S fs_i_pc_cheb_upper_tail_count_body_steps)) * fs_v_pc_cheb_upper_tail_count)) /\ exists fs_q_pc_cheb_upper_tail_count_body_steps_successor. fs_u_pc_cheb_upper_tail_count = fs_q_pc_cheb_upper_tail_count_body_steps_successor * S ((S (S fs_i_pc_cheb_upper_tail_count_body_steps)) * fs_v_pc_cheb_upper_tail_count) + (fs_s_pc_cheb_upper_tail_count_body_steps))) /\ fs_s_pc_cheb_upper_tail_count_body_steps = fs_r_pc_cheb_upper_tail_count_body_steps + fs_a_pc_cheb_upper_tail_count_body_steps)))))
  101. 0101specialize beta_sum_exists x8
  102. 0102specialize beta_sum_exists x9
  103. 0103specialize beta_sum_exists N
  104. 0104apply beta_sum_exists
  105. 0105cases hsum
  106. 0106specialize chebyshev_upper_arithmetic N
  107. 0107specialize chebyshev_upper_arithmetic ell
  108. 0108specialize chebyshev_upper_arithmetic k
  109. 0109specialize chebyshev_upper_arithmetic x3
  110. 0110specialize chebyshev_upper_arithmetic x5
  111. 0111specialize chebyshev_upper_arithmetic x10
  112. 0112apply chebyshev_upper_arithmetic
  113. 0113specialize beta_cutoff_count_comparison x5
  114. 0114specialize beta_cutoff_count_comparison x6
  115. 0115specialize beta_cutoff_count_comparison x7
  116. 0116specialize beta_cutoff_count_comparison x8
  117. 0117specialize beta_cutoff_count_comparison x9
  118. 0118specialize beta_cutoff_count_comparison N
  119. 0119specialize beta_cutoff_count_comparison k
  120. 0120specialize beta_cutoff_count_comparison x10
  121. 0121apply beta_cutoff_count_comparison
  122. 0122specialize prime_bit_prefix_all_bits x6
  123. 0123specialize prime_bit_prefix_all_bits x7
  124. 0124specialize prime_bit_prefix_all_bits N
  125. 0125apply prime_bit_prefix_all_bits
  126. 0126exact hk_witness_witness_left
  127. 0127exact hcut_witness_witness
  128. 0128exact hk_witness_witness_right
  129. 0129exact hsum_witness
  130. 0130exact hscale_right_left
  131. 0131exact hscale_right_right_left
  132. 0132exact hscale_right_right_right
  133. 0133specialize prime_cutoff_exponent_bound N
  134. 0134specialize prime_cutoff_exponent_bound x3
  135. 0135specialize prime_cutoff_exponent_bound x5
  136. 0136specialize prime_cutoff_exponent_bound x6
  137. 0137specialize prime_cutoff_exponent_bound x7
  138. 0138specialize prime_cutoff_exponent_bound x8
  139. 0139specialize prime_cutoff_exponent_bound x9
  140. 0140specialize prime_cutoff_exponent_bound x10
  141. 0141apply prime_cutoff_exponent_bound
  142. 0142exact hU_witness
  143. 0143exact hk_witness_witness_left
  144. 0144exact hcut_witness_witness
  145. 0145exact hsum_witness