PC0028

prime_cutoff_exponent_bound

At a genuine binary-power cutoff U=2^h, h times the actual upper prime count is at most 2N.

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. ∀ h. ∀ U. ∀ b. ∀ c. ∀ d. ∀ f. ∀ L. PowTwo(h,U) → PrimeBitPrefix(b,c,N) → BetaCutoffPrefix(U,b,c,d,f,N) → Sum(d,f,N,L) → Le(h · L,N + N)

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

Definition DAG

PowTwo(e,p) · 3PrimeBitPrefix(b,c,l) · 1BetaCutoffPrefix(u,b,c,d,f,l) · 1Le(a,b) · 2Sum(b,c,l,z) · 1Pow(a,e,z) · 2Primorial(n,z) · 1

Actual proof prerequisites

primorial_exists · checked external prerequisitepow_exists · checked external prerequisitepow_mul_exp · checked external prerequisitepow_four_equals_binary_doubleprimorial_cutoff_count_power_boundprimorial_le_four_pow · checked external prerequisitele_trans · checked external prerequisitebinary_power_two_order_reflects_exponent
Original expanded first-order statement 
forall N h U b c d f L. (exists pa_b_pc_cut_exp_power pa_c_pc_cut_exp_power. ((forall pa_i_pc_cut_exp_power_repeat. (exists pa_lt_pc_cut_exp_power_repeat_bound. pa_lt_pc_cut_exp_power_repeat_bound + S pa_i_pc_cut_exp_power_repeat = h) -> (((exists pa_h_pc_cut_exp_power_repeat_decoded. pa_h_pc_cut_exp_power_repeat_decoded + S (2) = S ((S (pa_i_pc_cut_exp_power_repeat)) * pa_c_pc_cut_exp_power)) /\ exists pa_q_pc_cut_exp_power_repeat_decoded. pa_b_pc_cut_exp_power = pa_q_pc_cut_exp_power_repeat_decoded * S ((S (pa_i_pc_cut_exp_power_repeat)) * pa_c_pc_cut_exp_power) + (2)))) /\ (exists pa_u_pc_cut_exp_power_product pa_v_pc_cut_exp_power_product. ((((exists pa_h_pc_cut_exp_power_product_start. pa_h_pc_cut_exp_power_product_start + S (1) = S ((S (0)) * pa_v_pc_cut_exp_power_product)) /\ exists pa_q_pc_cut_exp_power_product_start. pa_u_pc_cut_exp_power_product = pa_q_pc_cut_exp_power_product_start * S ((S (0)) * pa_v_pc_cut_exp_power_product) + (1))) /\ ((((exists pa_h_pc_cut_exp_power_product_terminal. pa_h_pc_cut_exp_power_product_terminal + S (U) = S ((S (h)) * pa_v_pc_cut_exp_power_product)) /\ exists pa_q_pc_cut_exp_power_product_terminal. pa_u_pc_cut_exp_power_product = pa_q_pc_cut_exp_power_product_terminal * S ((S (h)) * pa_v_pc_cut_exp_power_product) + (U))) /\ forall pa_i_pc_cut_exp_power_product. (exists pa_lt_pc_cut_exp_power_product_bound. pa_lt_pc_cut_exp_power_product_bound + S pa_i_pc_cut_exp_power_product = h) -> exists pa_p_pc_cut_exp_power_product pa_r_pc_cut_exp_power_product pa_s_pc_cut_exp_power_product. ((((exists pa_h_pc_cut_exp_power_product_factor. pa_h_pc_cut_exp_power_product_factor + S (pa_p_pc_cut_exp_power_product) = S ((S (pa_i_pc_cut_exp_power_product)) * pa_c_pc_cut_exp_power)) /\ exists pa_q_pc_cut_exp_power_product_factor. pa_b_pc_cut_exp_power = pa_q_pc_cut_exp_power_product_factor * S ((S (pa_i_pc_cut_exp_power_product)) * pa_c_pc_cut_exp_power) + (pa_p_pc_cut_exp_power_product))) /\ ((((exists pa_h_pc_cut_exp_power_product_partial. pa_h_pc_cut_exp_power_product_partial + S (pa_r_pc_cut_exp_power_product) = S ((S (pa_i_pc_cut_exp_power_product)) * pa_v_pc_cut_exp_power_product)) /\ exists pa_q_pc_cut_exp_power_product_partial. pa_u_pc_cut_exp_power_product = pa_q_pc_cut_exp_power_product_partial * S ((S (pa_i_pc_cut_exp_power_product)) * pa_v_pc_cut_exp_power_product) + (pa_r_pc_cut_exp_power_product))) /\ ((((exists pa_h_pc_cut_exp_power_product_successor. pa_h_pc_cut_exp_power_product_successor + S (pa_s_pc_cut_exp_power_product) = S ((S (S pa_i_pc_cut_exp_power_product)) * pa_v_pc_cut_exp_power_product)) /\ exists pa_q_pc_cut_exp_power_product_successor. pa_u_pc_cut_exp_power_product = pa_q_pc_cut_exp_power_product_successor * S ((S (S pa_i_pc_cut_exp_power_product)) * pa_v_pc_cut_exp_power_product) + (pa_s_pc_cut_exp_power_product))) /\ pa_s_pc_cut_exp_power_product = pa_r_pc_cut_exp_power_product * pa_p_pc_cut_exp_power_product)))))))) -> (forall pc_index_cut_exp_mask. (exists pc_lt_cut_exp_mask_bound. pc_lt_cut_exp_mask_bound + S (pc_index_cut_exp_mask) = (N)) -> exists pc_bit_cut_exp_mask. (((exists fs_h_pc_cut_exp_mask_entry. fs_h_pc_cut_exp_mask_entry + S (pc_bit_cut_exp_mask) = S ((S (pc_index_cut_exp_mask)) * c)) /\ exists fs_q_pc_cut_exp_mask_entry. b = fs_q_pc_cut_exp_mask_entry * S ((S (pc_index_cut_exp_mask)) * c) + (pc_bit_cut_exp_mask))) /\ (((((~(S (pc_index_cut_exp_mask) = 1) /\ forall bpr_left_pc_cut_exp_mask_choice_prime bpr_right_pc_cut_exp_mask_choice_prime. S (pc_index_cut_exp_mask) = bpr_left_pc_cut_exp_mask_choice_prime * bpr_right_pc_cut_exp_mask_choice_prime -> bpr_left_pc_cut_exp_mask_choice_prime = 1 \/ bpr_right_pc_cut_exp_mask_choice_prime = 1)) /\ pc_bit_cut_exp_mask = 1) \/ (~((~(S (pc_index_cut_exp_mask) = 1) /\ forall bpr_left_pc_cut_exp_mask_choice_prime bpr_right_pc_cut_exp_mask_choice_prime. S (pc_index_cut_exp_mask) = bpr_left_pc_cut_exp_mask_choice_prime * bpr_right_pc_cut_exp_mask_choice_prime -> bpr_left_pc_cut_exp_mask_choice_prime = 1 \/ bpr_right_pc_cut_exp_mask_choice_prime = 1)) /\ pc_bit_cut_exp_mask = 0)))) -> (forall pc_index_cut_exp_cutoff. (exists pc_lt_cut_exp_cutoff_bound. pc_lt_cut_exp_cutoff_bound + S (pc_index_cut_exp_cutoff) = (N)) -> exists pc_bit_cut_exp_cutoff. (((exists fs_h_pc_cut_exp_cutoff_entry. fs_h_pc_cut_exp_cutoff_entry + S (pc_bit_cut_exp_cutoff) = S ((S (pc_index_cut_exp_cutoff)) * f)) /\ exists fs_q_pc_cut_exp_cutoff_entry. d = fs_q_pc_cut_exp_cutoff_entry * S ((S (pc_index_cut_exp_cutoff)) * f) + (pc_bit_cut_exp_cutoff))) /\ ((((exists pc_lt_cut_exp_cutoff_choice_below. pc_lt_cut_exp_cutoff_choice_below + S (pc_index_cut_exp_cutoff) = (U)) /\ pc_bit_cut_exp_cutoff = 0) \/ ((exists pc_le_cut_exp_cutoff_choice_above. pc_le_cut_exp_cutoff_choice_above + (U) = (pc_index_cut_exp_cutoff)) /\ (((exists fs_h_pc_cut_exp_cutoff_choice_source. fs_h_pc_cut_exp_cutoff_choice_source + S (pc_bit_cut_exp_cutoff) = S ((S (pc_index_cut_exp_cutoff)) * c)) /\ exists fs_q_pc_cut_exp_cutoff_choice_source. b = fs_q_pc_cut_exp_cutoff_choice_source * S ((S (pc_index_cut_exp_cutoff)) * c) + (pc_bit_cut_exp_cutoff))))))) -> (exists fs_u_pc_cut_exp_count fs_v_pc_cut_exp_count. ((((exists fs_h_pc_cut_exp_count_body_start. fs_h_pc_cut_exp_count_body_start + S (0) = S ((S (0)) * fs_v_pc_cut_exp_count)) /\ exists fs_q_pc_cut_exp_count_body_start. fs_u_pc_cut_exp_count = fs_q_pc_cut_exp_count_body_start * S ((S (0)) * fs_v_pc_cut_exp_count) + (0))) /\ ((((exists fs_h_pc_cut_exp_count_body_terminal. fs_h_pc_cut_exp_count_body_terminal + S (L) = S ((S (N)) * fs_v_pc_cut_exp_count)) /\ exists fs_q_pc_cut_exp_count_body_terminal. fs_u_pc_cut_exp_count = fs_q_pc_cut_exp_count_body_terminal * S ((S (N)) * fs_v_pc_cut_exp_count) + (L))) /\ forall fs_i_pc_cut_exp_count_body_steps. (exists fs_lt_pc_cut_exp_count_body_steps_bound. fs_lt_pc_cut_exp_count_body_steps_bound + S fs_i_pc_cut_exp_count_body_steps = N) -> exists fs_a_pc_cut_exp_count_body_steps fs_r_pc_cut_exp_count_body_steps fs_s_pc_cut_exp_count_body_steps. ((((exists fs_h_pc_cut_exp_count_body_steps_summand. fs_h_pc_cut_exp_count_body_steps_summand + S (fs_a_pc_cut_exp_count_body_steps) = S ((S (fs_i_pc_cut_exp_count_body_steps)) * f)) /\ exists fs_q_pc_cut_exp_count_body_steps_summand. d = fs_q_pc_cut_exp_count_body_steps_summand * S ((S (fs_i_pc_cut_exp_count_body_steps)) * f) + (fs_a_pc_cut_exp_count_body_steps))) /\ ((((exists fs_h_pc_cut_exp_count_body_steps_partial. fs_h_pc_cut_exp_count_body_steps_partial + S (fs_r_pc_cut_exp_count_body_steps) = S ((S (fs_i_pc_cut_exp_count_body_steps)) * fs_v_pc_cut_exp_count)) /\ exists fs_q_pc_cut_exp_count_body_steps_partial. fs_u_pc_cut_exp_count = fs_q_pc_cut_exp_count_body_steps_partial * S ((S (fs_i_pc_cut_exp_count_body_steps)) * fs_v_pc_cut_exp_count) + (fs_r_pc_cut_exp_count_body_steps))) /\ ((((exists fs_h_pc_cut_exp_count_body_steps_successor. fs_h_pc_cut_exp_count_body_steps_successor + S (fs_s_pc_cut_exp_count_body_steps) = S ((S (S fs_i_pc_cut_exp_count_body_steps)) * fs_v_pc_cut_exp_count)) /\ exists fs_q_pc_cut_exp_count_body_steps_successor. fs_u_pc_cut_exp_count = fs_q_pc_cut_exp_count_body_steps_successor * S ((S (S fs_i_pc_cut_exp_count_body_steps)) * fs_v_pc_cut_exp_count) + (fs_s_pc_cut_exp_count_body_steps))) /\ fs_s_pc_cut_exp_count_body_steps = fs_r_pc_cut_exp_count_body_steps + fs_a_pc_cut_exp_count_body_steps)))))) -> (exists pc_le_cut_exp_result. pc_le_cut_exp_result + (h * L) = (N + N))

Complete tactic proof in conservative notation

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

92 script commands · 20 reading checkpoints · 8 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)
pow four equals binary doubleprimorial cutoff count power boundbinary power two order reflects exponent
01Fix variables and assumptionsL1–10

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

  1. L1
    intro N
  2. L2
    intro h
  3. L3
    intro U
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro d
  7. L7
    intro f
  8. L8
    intro L
  9. L9
    intro hU
  10. L10
    intro hm
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hc
  2. L12
    intro hL
03Establish hPL13–15

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

  1. L13
    have hP : ∃ P. Primorial(N,P)Definitions: Primorial(N,P)Original native command in the exact edition
  2. L14
    specialize primorial_exists N
  3. L15
    apply primorial_exists
04Separate the logical casesL16–16

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

  1. L16
    cases hP
05Establish hQL17–20

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

  1. L17
    have hQ : ∃ Q. Pow(U,L,Q)Definitions: Pow(U,L,Q)Original native command in the exact edition
  2. L18
    specialize pow_exists U
  3. L19
    specialize pow_exists L
  4. L20
    apply pow_exists
06Separate the logical casesL21–21

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

  1. L21
    cases hQ
07Establish hTL22–25

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

  1. L22
    have hT : ∃ T. PowTwo(h · L,T)Definitions: PowTwo(h · L,T)Original native command in the exact edition
  2. L23
    specialize pow_exists 2
  3. L24
    specialize pow_exists (h * L)
  4. L25
    apply pow_exists
08Separate the logical casesL26–26

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

  1. L26
    cases hT
09Establish hRL27–30

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

  1. L27
    have hR : ∃ R. Pow(4,N,R)Definitions: Pow(4,N,R)Original native command in the exact edition
  2. L28
    specialize pow_exists 4
  3. L29
    specialize pow_exists N
  4. L30
    apply pow_exists
10Separate the logical casesL31–31

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

  1. L31
    cases hR
11Establish hWL32–35

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

  1. L32
    have hW : ∃ W. PowTwo(N + N,W)Definitions: PowTwo(N + N,W)Original native command in the exact edition
  2. L33
    specialize pow_exists 2
  3. L34
    specialize pow_exists (N + N)
  4. L35
    apply pow_exists
12Separate the logical casesL36–36

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

  1. L36
    cases hW
13Establish hflatL37–46

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

  1. L37
    have hflat : x1 = x2
  2. L38
    specialize pow_mul_exp 2
  3. L39
    specialize pow_mul_exp h
  4. L40
    specialize pow_mul_exp L
  5. L41
    specialize pow_mul_exp (h * L)
  6. L42
    specialize pow_mul_exp U
  7. L43
    specialize pow_mul_exp x1
  8. L44
    specialize pow_mul_exp x2
  9. L45
    apply pow_mul_exp
  10. L46
    refl
14Use earlier factsL47–49

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

  1. L47
    exact hU
  2. L48
    exact hQ_witness
  3. L49
    exact hT_witness
15Establish hdoubleL50–56

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

  1. L50
    have hdouble : x3 = x4
  2. L51
    specialize pow_four_equals_binary_double N
  3. L52
    specialize pow_four_equals_binary_double x3
  4. L53
    specialize pow_four_equals_binary_double x4
  5. L54
    apply pow_four_equals_binary_double
  6. L55
    exact hR_witness
  7. L56
    exact hW_witness
16Establish hboundL57–66

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

  1. L57
    have hbound : Le(x1,x3)Definitions: Le(x1,x3)Original native command in the exact edition
  2. L58
    specialize le_trans x1
  3. L59
    specialize le_trans x
  4. L60
    specialize le_trans x3
  5. L61
    apply le_trans
  6. L62
    specialize primorial_cutoff_count_power_bound N
  7. L63
    specialize primorial_cutoff_count_power_bound U
  8. L64
    specialize primorial_cutoff_count_power_bound b
  9. L65
    specialize primorial_cutoff_count_power_bound c
  10. L66
    specialize primorial_cutoff_count_power_bound d
17Use earlier factsL67–76

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

  1. L67
    specialize primorial_cutoff_count_power_bound f
  2. L68
    specialize primorial_cutoff_count_power_bound L
  3. L69
    specialize primorial_cutoff_count_power_bound x
  4. L70
    specialize primorial_cutoff_count_power_bound x1
  5. L71
    apply primorial_cutoff_count_power_bound
  6. L72
    exact hm
  7. L73
    exact hc
  8. L74
    exact hL
  9. L75
    exact hP_witness
  10. L76
    exact hQ_witness
18Use earlier factsL77–82

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

  1. L77
    specialize primorial_le_four_pow N
  2. L78
    specialize primorial_le_four_pow x
  3. L79
    specialize primorial_le_four_pow x3
  4. L80
    apply primorial_le_four_pow
  5. L81
    exact hP_witness
  6. L82
    exact hR_witness
19Calculate and transport equalitiesL83–84

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

  1. L83
    rewrite hflat at hbound
  2. L84
    rewrite hdouble at hbound
20Use earlier factsL85–92

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

  1. L85
    specialize binary_power_two_order_reflects_exponent (h * L)
  2. L86
    specialize binary_power_two_order_reflects_exponent (N + N)
  3. L87
    specialize binary_power_two_order_reflects_exponent x2
  4. L88
    specialize binary_power_two_order_reflects_exponent x4
  5. L89
    apply binary_power_two_order_reflects_exponent
  6. L90
    exact hT_witness
  7. L91
    exact hW_witness
  8. L92
    exact hbound

Library-wide reading audit

Original defined command ledger · 92 lines
  1. 0001intro N
  2. 0002intro h
  3. 0003intro U
  4. 0004intro b
  5. 0005intro c
  6. 0006intro d
  7. 0007intro f
  8. 0008intro L
  9. 0009intro hU
  10. 0010intro hm
  11. 0011intro hc
  12. 0012intro hL
  13. 0013have hP : ∃ P. Primorial(N,P)
  14. 0014specialize primorial_exists N
  15. 0015apply primorial_exists
  16. 0016cases hP
  17. 0017have hQ : ∃ Q. Pow(U,L,Q)
  18. 0018specialize pow_exists U
  19. 0019specialize pow_exists L
  20. 0020apply pow_exists
  21. 0021cases hQ
  22. 0022have hT : ∃ T. PowTwo(h · L,T)
  23. 0023specialize pow_exists 2
  24. 0024specialize pow_exists (h * L)
  25. 0025apply pow_exists
  26. 0026cases hT
  27. 0027have hR : ∃ R. Pow(4,N,R)
  28. 0028specialize pow_exists 4
  29. 0029specialize pow_exists N
  30. 0030apply pow_exists
  31. 0031cases hR
  32. 0032have hW : ∃ W. PowTwo(N + N,W)
  33. 0033specialize pow_exists 2
  34. 0034specialize pow_exists (N + N)
  35. 0035apply pow_exists
  36. 0036cases hW
  37. 0037have hflat : x1 = x2
  38. 0038specialize pow_mul_exp 2
  39. 0039specialize pow_mul_exp h
  40. 0040specialize pow_mul_exp L
  41. 0041specialize pow_mul_exp (h * L)
  42. 0042specialize pow_mul_exp U
  43. 0043specialize pow_mul_exp x1
  44. 0044specialize pow_mul_exp x2
  45. 0045apply pow_mul_exp
  46. 0046refl
  47. 0047exact hU
  48. 0048exact hQ_witness
  49. 0049exact hT_witness
  50. 0050have hdouble : x3 = x4
  51. 0051specialize pow_four_equals_binary_double N
  52. 0052specialize pow_four_equals_binary_double x3
  53. 0053specialize pow_four_equals_binary_double x4
  54. 0054apply pow_four_equals_binary_double
  55. 0055exact hR_witness
  56. 0056exact hW_witness
  57. 0057have hbound : Le(x1,x3)
  58. 0058specialize le_trans x1
  59. 0059specialize le_trans x
  60. 0060specialize le_trans x3
  61. 0061apply le_trans
  62. 0062specialize primorial_cutoff_count_power_bound N
  63. 0063specialize primorial_cutoff_count_power_bound U
  64. 0064specialize primorial_cutoff_count_power_bound b
  65. 0065specialize primorial_cutoff_count_power_bound c
  66. 0066specialize primorial_cutoff_count_power_bound d
  67. 0067specialize primorial_cutoff_count_power_bound f
  68. 0068specialize primorial_cutoff_count_power_bound L
  69. 0069specialize primorial_cutoff_count_power_bound x
  70. 0070specialize primorial_cutoff_count_power_bound x1
  71. 0071apply primorial_cutoff_count_power_bound
  72. 0072exact hm
  73. 0073exact hc
  74. 0074exact hL
  75. 0075exact hP_witness
  76. 0076exact hQ_witness
  77. 0077specialize primorial_le_four_pow N
  78. 0078specialize primorial_le_four_pow x
  79. 0079specialize primorial_le_four_pow x3
  80. 0080apply primorial_le_four_pow
  81. 0081exact hP_witness
  82. 0082exact hR_witness
  83. 0083rewrite hflat at hbound
  84. 0084rewrite hdouble at hbound
  85. 0085specialize binary_power_two_order_reflects_exponent (h * L)
  86. 0086specialize binary_power_two_order_reflects_exponent (N + N)
  87. 0087specialize binary_power_two_order_reflects_exponent x2
  88. 0088specialize binary_power_two_order_reflects_exponent x4
  89. 0089apply binary_power_two_order_reflects_exponent
  90. 0090exact hT_witness
  91. 0091exact hW_witness
  92. 0092exact hbound