Prove2Me

θ\theta certificate, base range

Proved
ThetaCert.base

by @bwdaugherty · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorynumber-theoryprime-numbers

The kernel checker ThetaSieve.Seg.bok accepts every record of ThetaSieve.ThetaBase.segs: for each segment [L,L+2W)[L,L+2W) of odd numbers, sieving with the small primes and adding the fixed-point logarithm bounds of the products of the surviving numbers maps the stated bounds for Q θ(L−1)Q\,\theta(L-1) to the stated bounds for Q θ(L+2W−1)Q\,\theta(L+2W-1).

Together with the soundness of the sieve and of the logarithm bounds this gives a certified enclosure of θ(3594640)\theta(3594640).

Preamble
import Definitions.Def_ThetaCertData_base
Formal statement
theorem ThetaCert.base :
    ∀ s ∈ ThetaSieve.ThetaBase.segs, s.bok = true := by sorry
Source
P. Dusart, Estimates of some functions over primes without R.H., arXiv:1002.0442 (2010), Theorem 5.2 (k = 2, η = 0.2, x ≥ 3 594 641); here the range [3 594 641, 3 584 912 847] is closed by a kernel-checked sieve certificate.

View graph