Exact prime masks · binary length · explicit constants · Constructive arithmetic

Effective Chebyshev prime-count bounds

N≥2 ∧ BitLen(N,ℓ) ∧ PrimeCount(N,k) ⇒ N≤8kℓ ∧ kℓ≤8N

Count every prime through N with a complete decidable finite mask and prove both integer Chebyshev bounds using actual central binomial and primorial estimates.

Open the definition-aware map Read the final theorem See campaign milestone G027

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 certificate

Fully expanded arithmetic

Inspect all 2621 native tactic lines and 239 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem PC0031 and follow only the lemmas and conservative definitions supporting prime_count_chebyshev_bounds.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G027 milestone → theorem and definition dependencies.
Major independently established statements: PC0031 prime_count_chebyshev_bounds.
Independently verified Alpha v34 checked-use theorem family: 55 dependency-curried kernel-checked theorem bodies · 239 proof prerequisites · 16 linked definitions · 27 definition-dependency arrows · 2621 exact tactic lines · first admitted v27 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 1224 bundle nodes; SHA-256 c4711433c92b67d2ebeb30131669c60563c70e0464dafa851d417fb88fb21a6d.
Exact mathematical boundary: 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.