PC002F

prime_count_chebyshev_lower_large

The required lower prime-count bound for all N at least eight, using the actual binary half and central coefficient.

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(7,N) → BitLen(N,ell) → PrimeCount(N,k) → Le(N,8 · k · ell)

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

Definition DAG

BitLen(n,ell) · 1PrimeCount(x,z) · 1Le(a,b) · 4Lt(a,b) · 4

Actual proof prerequisites

binary_exponent_split_exists · checked external prerequisitebinary_split_half_lower_boundle_add_right · checked external prerequisitecentral_binom_prime_count_exponent_boundle_trans · checked external prerequisitebinary_split_eight_boundmul_comm · checked external prerequisitemul_assoc · checked external prerequisite
Original expanded first-order statement 
forall N ell k. (exists pc_le_cheb_large_input. pc_le_cheb_large_input + (8) = (N)) -> ((((N) = 0 /\ (ell) = 1) \/ exists ff_exponent_bl_pc_cheb_large_length ff_lower_bl_pc_cheb_large_length ff_upper_bl_pc_cheb_large_length. (((ell) = S ff_exponent_bl_pc_cheb_large_length) /\ ((exists ff_positive_bl_pc_cheb_large_length. ff_positive_bl_pc_cheb_large_length + 1 = (N)) /\ ((exists pa_b_bl_pc_cheb_large_length_lower pa_c_bl_pc_cheb_large_length_lower. ((forall pa_i_bl_pc_cheb_large_length_lower_repeat. (exists pa_lt_bl_pc_cheb_large_length_lower_repeat_bound. pa_lt_bl_pc_cheb_large_length_lower_repeat_bound + S pa_i_bl_pc_cheb_large_length_lower_repeat = ff_exponent_bl_pc_cheb_large_length) -> (((exists pa_h_bl_pc_cheb_large_length_lower_repeat_decoded. pa_h_bl_pc_cheb_large_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_cheb_large_length_lower_repeat)) * pa_c_bl_pc_cheb_large_length_lower)) /\ exists pa_q_bl_pc_cheb_large_length_lower_repeat_decoded. pa_b_bl_pc_cheb_large_length_lower = pa_q_bl_pc_cheb_large_length_lower_repeat_decoded * S ((S (pa_i_bl_pc_cheb_large_length_lower_repeat)) * pa_c_bl_pc_cheb_large_length_lower) + (2)))) /\ (exists pa_u_bl_pc_cheb_large_length_lower_product pa_v_bl_pc_cheb_large_length_lower_product. ((((exists pa_h_bl_pc_cheb_large_length_lower_product_start. pa_h_bl_pc_cheb_large_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_cheb_large_length_lower_product)) /\ exists pa_q_bl_pc_cheb_large_length_lower_product_start. pa_u_bl_pc_cheb_large_length_lower_product = pa_q_bl_pc_cheb_large_length_lower_product_start * S ((S (0)) * pa_v_bl_pc_cheb_large_length_lower_product) + (1))) /\ ((((exists pa_h_bl_pc_cheb_large_length_lower_product_terminal. pa_h_bl_pc_cheb_large_length_lower_product_terminal + S (ff_lower_bl_pc_cheb_large_length) = S ((S (ff_exponent_bl_pc_cheb_large_length)) * pa_v_bl_pc_cheb_large_length_lower_product)) /\ exists pa_q_bl_pc_cheb_large_length_lower_product_terminal. pa_u_bl_pc_cheb_large_length_lower_product = pa_q_bl_pc_cheb_large_length_lower_product_terminal * S ((S (ff_exponent_bl_pc_cheb_large_length)) * pa_v_bl_pc_cheb_large_length_lower_product) + (ff_lower_bl_pc_cheb_large_length))) /\ forall pa_i_bl_pc_cheb_large_length_lower_product. (exists pa_lt_bl_pc_cheb_large_length_lower_product_bound. pa_lt_bl_pc_cheb_large_length_lower_product_bound + S pa_i_bl_pc_cheb_large_length_lower_product = ff_exponent_bl_pc_cheb_large_length) -> exists pa_p_bl_pc_cheb_large_length_lower_product pa_r_bl_pc_cheb_large_length_lower_product pa_s_bl_pc_cheb_large_length_lower_product. ((((exists pa_h_bl_pc_cheb_large_length_lower_product_factor. pa_h_bl_pc_cheb_large_length_lower_product_factor + S (pa_p_bl_pc_cheb_large_length_lower_product) = S ((S (pa_i_bl_pc_cheb_large_length_lower_product)) * pa_c_bl_pc_cheb_large_length_lower)) /\ exists pa_q_bl_pc_cheb_large_length_lower_product_factor. pa_b_bl_pc_cheb_large_length_lower = pa_q_bl_pc_cheb_large_length_lower_product_factor * S ((S (pa_i_bl_pc_cheb_large_length_lower_product)) * pa_c_bl_pc_cheb_large_length_lower) + (pa_p_bl_pc_cheb_large_length_lower_product))) /\ ((((exists pa_h_bl_pc_cheb_large_length_lower_product_partial. pa_h_bl_pc_cheb_large_length_lower_product_partial + S (pa_r_bl_pc_cheb_large_length_lower_product) = S ((S (pa_i_bl_pc_cheb_large_length_lower_product)) * pa_v_bl_pc_cheb_large_length_lower_product)) /\ exists pa_q_bl_pc_cheb_large_length_lower_product_partial. pa_u_bl_pc_cheb_large_length_lower_product = pa_q_bl_pc_cheb_large_length_lower_product_partial * S ((S (pa_i_bl_pc_cheb_large_length_lower_product)) * pa_v_bl_pc_cheb_large_length_lower_product) + (pa_r_bl_pc_cheb_large_length_lower_product))) /\ ((((exists pa_h_bl_pc_cheb_large_length_lower_product_successor. pa_h_bl_pc_cheb_large_length_lower_product_successor + S (pa_s_bl_pc_cheb_large_length_lower_product) = S ((S (S pa_i_bl_pc_cheb_large_length_lower_product)) * pa_v_bl_pc_cheb_large_length_lower_product)) /\ exists pa_q_bl_pc_cheb_large_length_lower_product_successor. pa_u_bl_pc_cheb_large_length_lower_product = pa_q_bl_pc_cheb_large_length_lower_product_successor * S ((S (S pa_i_bl_pc_cheb_large_length_lower_product)) * pa_v_bl_pc_cheb_large_length_lower_product) + (pa_s_bl_pc_cheb_large_length_lower_product))) /\ pa_s_bl_pc_cheb_large_length_lower_product = pa_r_bl_pc_cheb_large_length_lower_product * pa_p_bl_pc_cheb_large_length_lower_product)))))))) /\ ((exists pa_b_bl_pc_cheb_large_length_upper pa_c_bl_pc_cheb_large_length_upper. ((forall pa_i_bl_pc_cheb_large_length_upper_repeat. (exists pa_lt_bl_pc_cheb_large_length_upper_repeat_bound. pa_lt_bl_pc_cheb_large_length_upper_repeat_bound + S pa_i_bl_pc_cheb_large_length_upper_repeat = ell) -> (((exists pa_h_bl_pc_cheb_large_length_upper_repeat_decoded. pa_h_bl_pc_cheb_large_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_cheb_large_length_upper_repeat)) * pa_c_bl_pc_cheb_large_length_upper)) /\ exists pa_q_bl_pc_cheb_large_length_upper_repeat_decoded. pa_b_bl_pc_cheb_large_length_upper = pa_q_bl_pc_cheb_large_length_upper_repeat_decoded * S ((S (pa_i_bl_pc_cheb_large_length_upper_repeat)) * pa_c_bl_pc_cheb_large_length_upper) + (2)))) /\ (exists pa_u_bl_pc_cheb_large_length_upper_product pa_v_bl_pc_cheb_large_length_upper_product. ((((exists pa_h_bl_pc_cheb_large_length_upper_product_start. pa_h_bl_pc_cheb_large_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_cheb_large_length_upper_product)) /\ exists pa_q_bl_pc_cheb_large_length_upper_product_start. pa_u_bl_pc_cheb_large_length_upper_product = pa_q_bl_pc_cheb_large_length_upper_product_start * S ((S (0)) * pa_v_bl_pc_cheb_large_length_upper_product) + (1))) /\ ((((exists pa_h_bl_pc_cheb_large_length_upper_product_terminal. pa_h_bl_pc_cheb_large_length_upper_product_terminal + S (ff_upper_bl_pc_cheb_large_length) = S ((S (ell)) * pa_v_bl_pc_cheb_large_length_upper_product)) /\ exists pa_q_bl_pc_cheb_large_length_upper_product_terminal. pa_u_bl_pc_cheb_large_length_upper_product = pa_q_bl_pc_cheb_large_length_upper_product_terminal * S ((S (ell)) * pa_v_bl_pc_cheb_large_length_upper_product) + (ff_upper_bl_pc_cheb_large_length))) /\ forall pa_i_bl_pc_cheb_large_length_upper_product. (exists pa_lt_bl_pc_cheb_large_length_upper_product_bound. pa_lt_bl_pc_cheb_large_length_upper_product_bound + S pa_i_bl_pc_cheb_large_length_upper_product = ell) -> exists pa_p_bl_pc_cheb_large_length_upper_product pa_r_bl_pc_cheb_large_length_upper_product pa_s_bl_pc_cheb_large_length_upper_product. ((((exists pa_h_bl_pc_cheb_large_length_upper_product_factor. pa_h_bl_pc_cheb_large_length_upper_product_factor + S (pa_p_bl_pc_cheb_large_length_upper_product) = S ((S (pa_i_bl_pc_cheb_large_length_upper_product)) * pa_c_bl_pc_cheb_large_length_upper)) /\ exists pa_q_bl_pc_cheb_large_length_upper_product_factor. pa_b_bl_pc_cheb_large_length_upper = pa_q_bl_pc_cheb_large_length_upper_product_factor * S ((S (pa_i_bl_pc_cheb_large_length_upper_product)) * pa_c_bl_pc_cheb_large_length_upper) + (pa_p_bl_pc_cheb_large_length_upper_product))) /\ ((((exists pa_h_bl_pc_cheb_large_length_upper_product_partial. pa_h_bl_pc_cheb_large_length_upper_product_partial + S (pa_r_bl_pc_cheb_large_length_upper_product) = S ((S (pa_i_bl_pc_cheb_large_length_upper_product)) * pa_v_bl_pc_cheb_large_length_upper_product)) /\ exists pa_q_bl_pc_cheb_large_length_upper_product_partial. pa_u_bl_pc_cheb_large_length_upper_product = pa_q_bl_pc_cheb_large_length_upper_product_partial * S ((S (pa_i_bl_pc_cheb_large_length_upper_product)) * pa_v_bl_pc_cheb_large_length_upper_product) + (pa_r_bl_pc_cheb_large_length_upper_product))) /\ ((((exists pa_h_bl_pc_cheb_large_length_upper_product_successor. pa_h_bl_pc_cheb_large_length_upper_product_successor + S (pa_s_bl_pc_cheb_large_length_upper_product) = S ((S (S pa_i_bl_pc_cheb_large_length_upper_product)) * pa_v_bl_pc_cheb_large_length_upper_product)) /\ exists pa_q_bl_pc_cheb_large_length_upper_product_successor. pa_u_bl_pc_cheb_large_length_upper_product = pa_q_bl_pc_cheb_large_length_upper_product_successor * S ((S (S pa_i_bl_pc_cheb_large_length_upper_product)) * pa_v_bl_pc_cheb_large_length_upper_product) + (pa_s_bl_pc_cheb_large_length_upper_product))) /\ pa_s_bl_pc_cheb_large_length_upper_product = pa_r_bl_pc_cheb_large_length_upper_product * pa_p_bl_pc_cheb_large_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_pc_cheb_large_length. ff_lower_gap_bl_pc_cheb_large_length + (ff_lower_bl_pc_cheb_large_length) = (N)) /\ (exists ff_upper_gap_bl_pc_cheb_large_length. ff_upper_gap_bl_pc_cheb_large_length + S (N) = (ff_upper_bl_pc_cheb_large_length))))))))) -> (exists pc_code_cheb_large_count pc_scale_cheb_large_count. (forall pc_index_cheb_large_count_mask. (exists pc_lt_cheb_large_count_mask_bound. pc_lt_cheb_large_count_mask_bound + S (pc_index_cheb_large_count_mask) = (N)) -> exists pc_bit_cheb_large_count_mask. (((exists fs_h_pc_cheb_large_count_mask_entry. fs_h_pc_cheb_large_count_mask_entry + S (pc_bit_cheb_large_count_mask) = S ((S (pc_index_cheb_large_count_mask)) * pc_scale_cheb_large_count)) /\ exists fs_q_pc_cheb_large_count_mask_entry. pc_code_cheb_large_count = fs_q_pc_cheb_large_count_mask_entry * S ((S (pc_index_cheb_large_count_mask)) * pc_scale_cheb_large_count) + (pc_bit_cheb_large_count_mask))) /\ (((((~(S (pc_index_cheb_large_count_mask) = 1) /\ forall bpr_left_pc_cheb_large_count_mask_choice_prime bpr_right_pc_cheb_large_count_mask_choice_prime. S (pc_index_cheb_large_count_mask) = bpr_left_pc_cheb_large_count_mask_choice_prime * bpr_right_pc_cheb_large_count_mask_choice_prime -> bpr_left_pc_cheb_large_count_mask_choice_prime = 1 \/ bpr_right_pc_cheb_large_count_mask_choice_prime = 1)) /\ pc_bit_cheb_large_count_mask = 1) \/ (~((~(S (pc_index_cheb_large_count_mask) = 1) /\ forall bpr_left_pc_cheb_large_count_mask_choice_prime bpr_right_pc_cheb_large_count_mask_choice_prime. S (pc_index_cheb_large_count_mask) = bpr_left_pc_cheb_large_count_mask_choice_prime * bpr_right_pc_cheb_large_count_mask_choice_prime -> bpr_left_pc_cheb_large_count_mask_choice_prime = 1 \/ bpr_right_pc_cheb_large_count_mask_choice_prime = 1)) /\ pc_bit_cheb_large_count_mask = 0)))) /\ (exists fs_u_pc_cheb_large_count_sum fs_v_pc_cheb_large_count_sum. ((((exists fs_h_pc_cheb_large_count_sum_body_start. fs_h_pc_cheb_large_count_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_cheb_large_count_sum)) /\ exists fs_q_pc_cheb_large_count_sum_body_start. fs_u_pc_cheb_large_count_sum = fs_q_pc_cheb_large_count_sum_body_start * S ((S (0)) * fs_v_pc_cheb_large_count_sum) + (0))) /\ ((((exists fs_h_pc_cheb_large_count_sum_body_terminal. fs_h_pc_cheb_large_count_sum_body_terminal + S (k) = S ((S (N)) * fs_v_pc_cheb_large_count_sum)) /\ exists fs_q_pc_cheb_large_count_sum_body_terminal. fs_u_pc_cheb_large_count_sum = fs_q_pc_cheb_large_count_sum_body_terminal * S ((S (N)) * fs_v_pc_cheb_large_count_sum) + (k))) /\ forall fs_i_pc_cheb_large_count_sum_body_steps. (exists fs_lt_pc_cheb_large_count_sum_body_steps_bound. fs_lt_pc_cheb_large_count_sum_body_steps_bound + S fs_i_pc_cheb_large_count_sum_body_steps = N) -> exists fs_a_pc_cheb_large_count_sum_body_steps fs_r_pc_cheb_large_count_sum_body_steps fs_s_pc_cheb_large_count_sum_body_steps. ((((exists fs_h_pc_cheb_large_count_sum_body_steps_summand. fs_h_pc_cheb_large_count_sum_body_steps_summand + S (fs_a_pc_cheb_large_count_sum_body_steps) = S ((S (fs_i_pc_cheb_large_count_sum_body_steps)) * pc_scale_cheb_large_count)) /\ exists fs_q_pc_cheb_large_count_sum_body_steps_summand. pc_code_cheb_large_count = fs_q_pc_cheb_large_count_sum_body_steps_summand * S ((S (fs_i_pc_cheb_large_count_sum_body_steps)) * pc_scale_cheb_large_count) + (fs_a_pc_cheb_large_count_sum_body_steps))) /\ ((((exists fs_h_pc_cheb_large_count_sum_body_steps_partial. fs_h_pc_cheb_large_count_sum_body_steps_partial + S (fs_r_pc_cheb_large_count_sum_body_steps) = S ((S (fs_i_pc_cheb_large_count_sum_body_steps)) * fs_v_pc_cheb_large_count_sum)) /\ exists fs_q_pc_cheb_large_count_sum_body_steps_partial. fs_u_pc_cheb_large_count_sum = fs_q_pc_cheb_large_count_sum_body_steps_partial * S ((S (fs_i_pc_cheb_large_count_sum_body_steps)) * fs_v_pc_cheb_large_count_sum) + (fs_r_pc_cheb_large_count_sum_body_steps))) /\ ((((exists fs_h_pc_cheb_large_count_sum_body_steps_successor. fs_h_pc_cheb_large_count_sum_body_steps_successor + S (fs_s_pc_cheb_large_count_sum_body_steps) = S ((S (S fs_i_pc_cheb_large_count_sum_body_steps)) * fs_v_pc_cheb_large_count_sum)) /\ exists fs_q_pc_cheb_large_count_sum_body_steps_successor. fs_u_pc_cheb_large_count_sum = fs_q_pc_cheb_large_count_sum_body_steps_successor * S ((S (S fs_i_pc_cheb_large_count_sum_body_steps)) * fs_v_pc_cheb_large_count_sum) + (fs_s_pc_cheb_large_count_sum_body_steps))) /\ fs_s_pc_cheb_large_count_sum_body_steps = fs_r_pc_cheb_large_count_sum_body_steps + fs_a_pc_cheb_large_count_sum_body_steps))))))) -> (exists pc_le_cheb_large_result. pc_le_cheb_large_result + (N) = (8 * k * ell))

Complete tactic proof in conservative notation

All 72 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

72 script commands · 15 reading checkpoints · 10 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 (3)
binary split half lower boundcentral binom prime count exponent boundbinary split eight 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 hsplitL7–9

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

  1. L7
    have hsplit : exists h d. (d = 0 \/ d = 1) /\ N = (h + h) + d
  2. L8
    specialize binary_exponent_split_exists N
  3. L9
    apply binary_exponent_split_exists
03Separate the logical casesL10–12

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

  1. L10
    cases hsplit
  2. L11
    cases hsplit_witness
  3. L12
    cases hsplit_witness_witness
04Establish hhL13–20

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

  1. L13
  2. L14
    specialize binary_split_half_lower_bound N
  3. L15
    specialize binary_split_half_lower_bound x
  4. L16
    specialize binary_split_half_lower_bound x1
  5. L17
    specialize binary_split_half_lower_bound 4
  6. L18
    apply binary_split_half_lower_bound
  7. L19
    exact hsplit_witness_witness_left
  8. L20
    exact hsplit_witness_witness_right
05Establish heightL21–24

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

  1. L21
    have height : 4 + 4 = 8
  2. L22
    norm_num
  3. L23
    rewrite height
  4. L24
    exact hN
06Establish hhalfL25–29

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

  1. L25
    have hhalf : Le(x + x,N)Definitions: Le(x + x,N)Original native command in the exact edition
  2. L26
    rewrite hsplit_witness_witness_right
  3. L27
    specialize le_add_right (x + x)
  4. L28
    specialize le_add_right x1
  5. L29
    apply le_add_right
07Establish hexponentL30–39

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

  1. L30
    have hexponent : Le(x,ell · k)Definitions: Le(x,ell · k)Original native command in the exact edition
  2. L31
    specialize central_binom_prime_count_exponent_bound N
  3. L32
    specialize central_binom_prime_count_exponent_bound ell
  4. L33
    specialize central_binom_prime_count_exponent_bound k
  5. L34
    specialize central_binom_prime_count_exponent_bound x
  6. L35
    apply central_binom_prime_count_exponent_bound
  7. L36
    exact hh
  8. L37
    exact hhalf
  9. L38
    exact hl
  10. L39
    exact hk
08Establish hpositivehalfL40–44

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

  1. L40
    have hpositivehalf : Lt(0,x)Definitions: Lt(0,x)Original native command in the exact edition
  2. L41
    specialize le_trans 1
  3. L42
    specialize le_trans 4
  4. L43
    specialize le_trans x
  5. L44
    apply le_trans
09Construct an explicit witnessL45–45

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

  1. L45
    exists 3
10Calculate and transport equalitiesL46–46

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

  1. L46
    norm_num
11Use earlier factsL47–47

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

  1. L47
    exact hh
12Establish hpositiveL48–54

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

  1. L48
    have hpositive : Lt(0,ell · k)Definitions: Lt(0,ell · k)Original native command in the exact edition
  2. L49
    specialize le_trans 1
  3. L50
    specialize le_trans x
  4. L51
    specialize le_trans (ell * k)
  5. L52
    apply le_trans
  6. L53
    exact hpositivehalf
  7. L54
    exact hexponent
13Establish hboundL55–64

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

  1. L55
    have hbound : Le(N,8 · (ell · k))Definitions: Le(N,8 · (ell · k))Original native command in the exact edition
  2. L56
    specialize binary_split_eight_bound N
  3. L57
    specialize binary_split_eight_bound x
  4. L58
    specialize binary_split_eight_bound x1
  5. L59
    specialize binary_split_eight_bound (ell * k)
  6. L60
    apply binary_split_eight_bound
  7. L61
    exact hsplit_witness_witness_left
  8. L62
    exact hsplit_witness_witness_right
  9. L63
    exact hexponent
  10. L64
    exact hpositive
14Establish horderL65–65

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

  1. L65
    have horder : 8 * (ell * k) = (8 * k) * ell
15Establish hswapL66–72

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

  1. L66
    have hswap : ell * k = k * ell
  2. L67
    apply mul_comm
  3. L68
    rewrite hswap
  4. L69
    symm
  5. L70
    apply mul_assoc
  6. L71
    rewrite horder at hbound
  7. L72
    exact hbound

Library-wide reading audit

Original defined command ledger · 72 lines
  1. 0001intro N
  2. 0002intro ell
  3. 0003intro k
  4. 0004intro hN
  5. 0005intro hl
  6. 0006intro hk
  7. 0007have hsplit : exists h d. (d = 0 \/ d = 1) /\ N = (h + h) + d
  8. 0008specialize binary_exponent_split_exists N
  9. 0009apply binary_exponent_split_exists
  10. 0010cases hsplit
  11. 0011cases hsplit_witness
  12. 0012cases hsplit_witness_witness
  13. 0013have hh : Lt(3,x)
  14. 0014specialize binary_split_half_lower_bound N
  15. 0015specialize binary_split_half_lower_bound x
  16. 0016specialize binary_split_half_lower_bound x1
  17. 0017specialize binary_split_half_lower_bound 4
  18. 0018apply binary_split_half_lower_bound
  19. 0019exact hsplit_witness_witness_left
  20. 0020exact hsplit_witness_witness_right
  21. 0021have height : 4 + 4 = 8
  22. 0022norm_num
  23. 0023rewrite height
  24. 0024exact hN
  25. 0025have hhalf : Le(x + x,N)
  26. 0026rewrite hsplit_witness_witness_right
  27. 0027specialize le_add_right (x + x)
  28. 0028specialize le_add_right x1
  29. 0029apply le_add_right
  30. 0030have hexponent : Le(x,ell · k)
  31. 0031specialize central_binom_prime_count_exponent_bound N
  32. 0032specialize central_binom_prime_count_exponent_bound ell
  33. 0033specialize central_binom_prime_count_exponent_bound k
  34. 0034specialize central_binom_prime_count_exponent_bound x
  35. 0035apply central_binom_prime_count_exponent_bound
  36. 0036exact hh
  37. 0037exact hhalf
  38. 0038exact hl
  39. 0039exact hk
  40. 0040have hpositivehalf : Lt(0,x)
  41. 0041specialize le_trans 1
  42. 0042specialize le_trans 4
  43. 0043specialize le_trans x
  44. 0044apply le_trans
  45. 0045exists 3
  46. 0046norm_num
  47. 0047exact hh
  48. 0048have hpositive : Lt(0,ell · k)
  49. 0049specialize le_trans 1
  50. 0050specialize le_trans x
  51. 0051specialize le_trans (ell * k)
  52. 0052apply le_trans
  53. 0053exact hpositivehalf
  54. 0054exact hexponent
  55. 0055have hbound : Le(N,8 · (ell · k))
  56. 0056specialize binary_split_eight_bound N
  57. 0057specialize binary_split_eight_bound x
  58. 0058specialize binary_split_eight_bound x1
  59. 0059specialize binary_split_eight_bound (ell * k)
  60. 0060apply binary_split_eight_bound
  61. 0061exact hsplit_witness_witness_left
  62. 0062exact hsplit_witness_witness_right
  63. 0063exact hexponent
  64. 0064exact hpositive
  65. 0065have horder : 8 * (ell * k) = (8 * k) * ell
  66. 0066have hswap : ell * k = k * ell
  67. 0067apply mul_comm
  68. 0068rewrite hswap
  69. 0069symm
  70. 0070apply mul_assoc
  71. 0071rewrite horder at hbound
  72. 0072exact hbound