PC002A

prime_count_chebyshev_upper

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

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

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.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ N. ∀ ell. ∀ k. Lt(1,N) → BitLen(N,ell) → PrimeCount(N,k) → Le(k · ell,8 · N)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PowTwo(e,p) · 3BitLen(n,ell) · 1PrimeCount(x,z) · 1BetaCutoffPrefix(u,b,c,d,f,l) · 1Le(a,b) · 8Lt(a,b) · 5Sum(b,c,l,z) · 1

Actual proof prerequisites

le_or_lt · checked external prerequisiteprime_count_boundedmul_le_mul · checked external prerequisitemul_le_mul_left · checked external prerequisitemul_comm · checked external prerequisitele_trans · checked external prerequisitebinary_length_nonzero_componentsle_zero · checked external prerequisitebinary_exponent_split_exists · checked external prerequisitepow_exists · checked external prerequisitebinary_half_scale_boundsbeta_cutoff_prefix_existsbeta_sum_exists · checked external prerequisitebeta_cutoff_count_comparisonprime_bit_prefix_all_bitsprime_cutoff_exponent_boundchebyshev_upper_arithmetic
Original expanded first-order 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))

Complete tactic proof in conservative notation

All 145 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (8)
prime count boundedbinary length nonzero componentsbinary half scale boundsbeta cutoff prefix existschebyshev upper arithmeticbeta cutoff count comparisonprime bit prefix all bitsprime cutoff exponent bound
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 : Le(ell,4) ∨ Lt(4,ell)Definitions: Le(ell,4)Lt(4,ell)Original native command in the exact edition
  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 : Le(k · ell,N · 4)Definitions: Le(k · ell,N · 4)Original native command in the exact edition
  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 : Le(N · 4,N · 8)Definitions: Le(N · 4,N · 8)Original native command in the exact edition
  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: PowTwo(e,v)PowTwo(ell,w)Le(v,N)Lt(N,w)Original native command in the exact edition
  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
  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(x3,U)Original native command in the exact edition
  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 : Lt(1,x3) ∧ (Le(x5 · x5,N) ∧ (Le(ell,2 · x5) ∧ Le(ell,3 · x3)))Definitions: Lt(1,x3)Le(x5 · x5,N)Le(ell,2 · x5)Le(ell,3 · x3)Original native command in the exact edition
  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(x5,x6,x7,d,f,N)Original native command in the exact edition
  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(x8,x9,N,L)Original native command in the exact edition
  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 defined 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 : Le(ell,4) ∨ Lt(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 : Le(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 : Le(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 : ∃ e. ∃ v. ∃ w. ell = S e ∧ (PowTwo(e,v) ∧ (PowTwo(ell,w) ∧ (Le(v,N) ∧ Lt(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 : Lt(1,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 : ∃ U. PowTwo(x3,U)
  66. 0066specialize pow_exists 2
  67. 0067specialize pow_exists x3
  68. 0068apply pow_exists
  69. 0069cases hU
  70. 0070have hscale : Lt(1,x3) ∧ (Le(x5 · x5,N) ∧ (Le(ell,2 · x5) ∧ Le(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 : ∃ d. ∃ f. BetaCutoffPrefix(x5,x6,x7,d,f,N)
  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 : ∃ L. Sum(x8,x9,N,L)
  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