PC0029

chebyshev_upper_arithmetic

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

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

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 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))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 9 declared prerequisites and contains 101 exact native proof lines.

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

Proof neighborhood

Direct dependencies

mul_le_mul_left Stable theorem; checked-use authorized mul_le_mul_right Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized mul_add Stable theorem; checked-use authorized add_mul Stable theorem; checked-use authorized add_le_add_right Stable theorem; checked-use authorized add_le_add_left Stable theorem; checked-use authorized

Direct dependents

PC002A prime_count_chebyshev_upper

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

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.

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 : exists g. g + U * ell = U * (2 * U)
  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 : exists g. g + U * ell = 2 * N
  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 : exists g. g + L * ell = L * (3 * h)
  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 : exists g. g + L * ell = 3 * (N + N)
  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 : exists g. g + (U * ell + L * ell) = 2 * N + L * ell
  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 : exists g. g + (U * ell + L * ell) = 2 * N + 6 * N
  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 exact 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 : exists g. g + 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 : exists g. g + 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 : exists g. g + 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 : exists g. g + 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 : exists g. g + (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 : exists g. g + (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