PC0029

chebyshev_upper_arithmetic

The exact small-prime 2N and large-prime 6N budgets combine to the required 8N bound.

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. ∀ h. ∀ U. ∀ L. Le(k,U + L) → Le(U · U,N) → Le(ell,2 · U) → Le(ell,3 · h) → Le(h · L,N + N) → Le(k · ell,8 · N)

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

Definition DAG

Le(a,b) · 12

Actual proof prerequisites

mul_le_mul_left · checked external prerequisitemul_le_mul_right · checked external prerequisitele_trans · checked external prerequisitemul_assoc · checked external prerequisitemul_comm · checked external prerequisitemul_add · checked external prerequisiteadd_mul · checked external prerequisiteadd_le_add_right · checked external prerequisiteadd_le_add_left · checked external prerequisite
Original expanded first-order statement 
forall N ell k h U L. (exists pc_le_upper_arith_count. pc_le_upper_arith_count + (k) = (U + L)) -> (exists pc_le_upper_arith_square. pc_le_upper_arith_square + (U * U) = (N)) -> (exists pc_le_upper_arith_small. pc_le_upper_arith_small + (ell) = (2 * U)) -> (exists pc_le_upper_arith_large. pc_le_upper_arith_large + (ell) = (3 * h)) -> (exists pc_le_upper_arith_exponent. pc_le_upper_arith_exponent + (h * L) = (N + N)) -> (exists pc_le_upper_arith_result. pc_le_upper_arith_result + (k * ell) = (8 * N))

Complete tactic proof in conservative notation

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

101 script commands · 19 reading checkpoints · 13 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro N
  2. L2
    intro ell
  3. L3
    intro k
  4. L4
    intro h
  5. L5
    intro U
  6. L6
    intro L
  7. L7
    intro hk
  8. L8
    intro hsq
  9. L9
    intro hs
  10. L10
    intro hl
02Fix variables and assumptionsL11–11

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

  1. L11
    intro he
03Establish hsmall0L12–17

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

  1. L12
    have hsmall0 : Le(U · ell,U · (2 · U))Definitions: Le(U · ell,U · (2 · U))Original native command in the exact edition
  2. L13
    specialize mul_le_mul_left ell
  3. L14
    specialize mul_le_mul_left (2 * U)
  4. L15
    specialize mul_le_mul_left U
  5. L16
    apply mul_le_mul_left
  6. L17
    exact hs
04Establish hsmall1L18–22

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

  1. L18
    have hsmall1 : U * (2 * U) = 2 * (U * U)
  2. L19
    trans (2 * U) * U
  3. L20
    apply mul_comm
  4. L21
    apply mul_assoc
  5. L22
    rewrite hsmall1 at hsmall0
05Establish hsmallL23–32

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

  1. L23
    have hsmall : Le(U · ell,2 · N)Definitions: Le(U · ell,2 · N)Original native command in the exact edition
  2. L24
    specialize le_trans (U * ell)
  3. L25
    specialize le_trans (2 * (U * U))
  4. L26
    specialize le_trans (2 * N)
  5. L27
    apply le_trans
  6. L28
    exact hsmall0
  7. L29
    specialize mul_le_mul_left (U * U)
  8. L30
    specialize mul_le_mul_left N
  9. L31
    specialize mul_le_mul_left 2
  10. L32
    apply mul_le_mul_left
06Use earlier factsL33–33

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

  1. L33
    exact hsq
07Establish hlarge0L34–39

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

  1. L34
    have hlarge0 : Le(L · ell,L · (3 · h))Definitions: Le(L · ell,L · (3 · h))Original native command in the exact edition
  2. L35
    specialize mul_le_mul_left ell
  3. L36
    specialize mul_le_mul_left (3 * h)
  4. L37
    specialize mul_le_mul_left L
  5. L38
    apply mul_le_mul_left
  6. L39
    exact hl
08Establish hlarge1L40–44

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

  1. L40
    have hlarge1 : L * (3 * h) = 3 * (h * L)
  2. L41
    trans (3 * h) * L
  3. L42
    apply mul_comm
  4. L43
    apply mul_assoc
  5. L44
    rewrite hlarge1 at hlarge0
09Establish hlarge2L45–54

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

  1. L45
    have hlarge2 : Le(L · ell,3 · (N + N))Definitions: Le(L · ell,3 · (N + N))Original native command in the exact edition
  2. L46
    specialize le_trans (L * ell)
  3. L47
    specialize le_trans (3 * (h * L))
  4. L48
    specialize le_trans (3 * (N + N))
  5. L49
    apply le_trans
  6. L50
    exact hlarge0
  7. L51
    specialize mul_le_mul_left (h * L)
  8. L52
    specialize mul_le_mul_left (N + N)
  9. L53
    specialize mul_le_mul_left 3
  10. L54
    apply mul_le_mul_left
10Use earlier factsL55–55

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

  1. L55
    exact he
11Establish hsixL56–59

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

  1. L56
    have hsix : 3 * (N + N) = 6 * N
  2. L57
    trans 3 * N + 3 * N
  3. L58
    apply mul_add
  4. L59
    symm
12Establish hsixnumL60–64

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

  1. L60
    have hsixnum : 6 = 3 + 3
  2. L61
    norm_num
  3. L62
    rewrite hsixnum
  4. L63
    apply add_mul
  5. L64
    rewrite hsix at hlarge2
13Establish hsum0L65–70

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

  1. L65
    have hsum0 : Le(U · ell + L · ell,2 · N + L · ell)Definitions: Le(U · ell + L · ell,2 · N + L · ell)Original native command in the exact edition
  2. L66
    specialize add_le_add_right (U * ell)
  3. L67
    specialize add_le_add_right (2 * N)
  4. L68
    specialize add_le_add_right (L * ell)
  5. L69
    apply add_le_add_right
  6. L70
    exact hsmall
14Establish hsumL71–80

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

  1. L71
    have hsum : Le(U · ell + L · ell,2 · N + 6 · N)Definitions: Le(U · ell + L · ell,2 · N + 6 · N)Original native command in the exact edition
  2. L72
    specialize le_trans (U * ell + L * ell)
  3. L73
    specialize le_trans (2 * N + L * ell)
  4. L74
    specialize le_trans (2 * N + 6 * N)
  5. L75
    apply le_trans
  6. L76
    exact hsum0
  7. L77
    specialize add_le_add_left (L * ell)
  8. L78
    specialize add_le_add_left (6 * N)
  9. L79
    specialize add_le_add_left (2 * N)
  10. L80
    apply add_le_add_left
15Use earlier factsL81–81

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

  1. L81
    exact hlarge2
16Establish hproductL82–84

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

  1. L82
    have hproduct : (U + L) * ell = U * ell + L * ell
  2. L83
    apply add_mul
  3. L84
    rewrite <- hproduct at hsum
17Establish heightL85–86

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

  1. L85
    have height : 2 * N + 6 * N = 8 * N
  2. L86
    symm
18Establish heightnumL87–96

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

  1. L87
    have heightnum : 8 = 2 + 6
  2. L88
    norm_num
  3. L89
    rewrite heightnum
  4. L90
    apply add_mul
  5. L91
    rewrite height at hsum
  6. L92
    specialize le_trans (k * ell)
  7. L93
    specialize le_trans ((U + L) * ell)
  8. L94
    specialize le_trans (8 * N)
  9. L95
    apply le_trans
  10. L96
    specialize mul_le_mul_right k
19Use earlier factsL97–101

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

  1. L97
    specialize mul_le_mul_right (U + L)
  2. L98
    specialize mul_le_mul_right ell
  3. L99
    apply mul_le_mul_right
  4. L100
    exact hk
  5. L101
    exact hsum

Library-wide reading audit

Original defined command ledger · 101 lines
  1. 0001intro N
  2. 0002intro ell
  3. 0003intro k
  4. 0004intro h
  5. 0005intro U
  6. 0006intro L
  7. 0007intro hk
  8. 0008intro hsq
  9. 0009intro hs
  10. 0010intro hl
  11. 0011intro he
  12. 0012have hsmall0 : Le(U · ell,U · (2 · U))
  13. 0013specialize mul_le_mul_left ell
  14. 0014specialize mul_le_mul_left (2 * U)
  15. 0015specialize mul_le_mul_left U
  16. 0016apply mul_le_mul_left
  17. 0017exact hs
  18. 0018have hsmall1 : U * (2 * U) = 2 * (U * U)
  19. 0019trans (2 * U) * U
  20. 0020apply mul_comm
  21. 0021apply mul_assoc
  22. 0022rewrite hsmall1 at hsmall0
  23. 0023have hsmall : Le(U · ell,2 · N)
  24. 0024specialize le_trans (U * ell)
  25. 0025specialize le_trans (2 * (U * U))
  26. 0026specialize le_trans (2 * N)
  27. 0027apply le_trans
  28. 0028exact hsmall0
  29. 0029specialize mul_le_mul_left (U * U)
  30. 0030specialize mul_le_mul_left N
  31. 0031specialize mul_le_mul_left 2
  32. 0032apply mul_le_mul_left
  33. 0033exact hsq
  34. 0034have hlarge0 : Le(L · ell,L · (3 · h))
  35. 0035specialize mul_le_mul_left ell
  36. 0036specialize mul_le_mul_left (3 * h)
  37. 0037specialize mul_le_mul_left L
  38. 0038apply mul_le_mul_left
  39. 0039exact hl
  40. 0040have hlarge1 : L * (3 * h) = 3 * (h * L)
  41. 0041trans (3 * h) * L
  42. 0042apply mul_comm
  43. 0043apply mul_assoc
  44. 0044rewrite hlarge1 at hlarge0
  45. 0045have hlarge2 : Le(L · ell,3 · (N + N))
  46. 0046specialize le_trans (L * ell)
  47. 0047specialize le_trans (3 * (h * L))
  48. 0048specialize le_trans (3 * (N + N))
  49. 0049apply le_trans
  50. 0050exact hlarge0
  51. 0051specialize mul_le_mul_left (h * L)
  52. 0052specialize mul_le_mul_left (N + N)
  53. 0053specialize mul_le_mul_left 3
  54. 0054apply mul_le_mul_left
  55. 0055exact he
  56. 0056have hsix : 3 * (N + N) = 6 * N
  57. 0057trans 3 * N + 3 * N
  58. 0058apply mul_add
  59. 0059symm
  60. 0060have hsixnum : 6 = 3 + 3
  61. 0061norm_num
  62. 0062rewrite hsixnum
  63. 0063apply add_mul
  64. 0064rewrite hsix at hlarge2
  65. 0065have hsum0 : Le(U · ell + L · ell,2 · N + L · ell)
  66. 0066specialize add_le_add_right (U * ell)
  67. 0067specialize add_le_add_right (2 * N)
  68. 0068specialize add_le_add_right (L * ell)
  69. 0069apply add_le_add_right
  70. 0070exact hsmall
  71. 0071have hsum : Le(U · ell + L · ell,2 · N + 6 · N)
  72. 0072specialize le_trans (U * ell + L * ell)
  73. 0073specialize le_trans (2 * N + L * ell)
  74. 0074specialize le_trans (2 * N + 6 * N)
  75. 0075apply le_trans
  76. 0076exact hsum0
  77. 0077specialize add_le_add_left (L * ell)
  78. 0078specialize add_le_add_left (6 * N)
  79. 0079specialize add_le_add_left (2 * N)
  80. 0080apply add_le_add_left
  81. 0081exact hlarge2
  82. 0082have hproduct : (U + L) * ell = U * ell + L * ell
  83. 0083apply add_mul
  84. 0084rewrite <- hproduct at hsum
  85. 0085have height : 2 * N + 6 * N = 8 * N
  86. 0086symm
  87. 0087have heightnum : 8 = 2 + 6
  88. 0088norm_num
  89. 0089rewrite heightnum
  90. 0090apply add_mul
  91. 0091rewrite height at hsum
  92. 0092specialize le_trans (k * ell)
  93. 0093specialize le_trans ((U + L) * ell)
  94. 0094specialize le_trans (8 * N)
  95. 0095apply le_trans
  96. 0096specialize mul_le_mul_right k
  97. 0097specialize mul_le_mul_right (U + L)
  98. 0098specialize mul_le_mul_right ell
  99. 0099apply mul_le_mul_right
  100. 0100exact hk
  101. 0101exact hsum