Certified Chebyshev psi(N) Upper Bounds

This module provides computable upper bounds on the Chebyshev function psi(N) = sum_{n in Ioc 0 N} vonMangoldt(n).

The core checker is generalized by a rational slope slope:

• checkPsiLeMulWith N slope depth checks psiUB(N) <= slope * N
• checkAllPsiLeMulWith bound slope depth checks all N = 1..bound

The original 1.11-specific API is kept as thin wrappers:

• checkPsiBound, allPsiBoundsHold, and their bridge theorems.

Computable upper bound on vonMangoldt(n)

def LeanCert.Engine.ChebyshevPsi.vonMangoldtUB (n : ℕ) (depth : ℕ := 20) : ℚ

Computable upper bound on the von Mangoldt function vonMangoldt(n). Returns (logPointComputable (minFac n) depth).hi when IsPrimePow n, and 0 otherwise.

Equations

• LeanCert.Engine.ChebyshevPsi.vonMangoldtUB n depth = if IsPrimePow n then (LeanCert.Core.IntervalRat.logPointComputable (↑n.minFac) depth).hi else 0

def LeanCert.Engine.ChebyshevPsi.psiUB (N : ℕ) (depth : ℕ := 20) : ℚ

Computable upper bound on psi(N): psiUB N depth = sum n in Ioc 0 N, vonMangoldtUB n depth.

Equations

• LeanCert.Engine.ChebyshevPsi.psiUB N depth = ∑ n ∈ Finset.Ioc 0 N, LeanCert.Engine.ChebyshevPsi.vonMangoldtUB n depth

Correctness theorems

theorem LeanCert.Engine.ChebyshevPsi.vonMangoldt_le_vonMangoldtUB (n depth : ℕ) : ArithmeticFunction.vonMangoldt n ≤ ↑(vonMangoldtUB n depth)

The von Mangoldt function is bounded above by our computable bound.

theorem LeanCert.Engine.ChebyshevPsi.psi_le_psiUB (N depth : ℕ) : Chebyshev.psi ↑N ≤ ↑(psiUB N depth)

The Chebyshev function psi(N) is bounded above by psiUB(N).

Decidable comparison infrastructure

theorem LeanCert.Engine.ChebyshevPsi.psi_le_of_psiUB_le (N depth : ℕ) (slope : ℚ) (h : decide (psiUB N depth ≤ slope) = true) : Chebyshev.psi ↑N ≤ ↑slope

Master theorem: if psiUB(N, depth) <= slope is verified computationally, then psi(N) <= slope.

Generic slope checker: psi(N) <= slope * N

def LeanCert.Engine.ChebyshevPsi.checkPsiLeMulWith (N : ℕ) (slope : ℚ) (depth : ℕ := 20) : Bool

Computable check: does psiUB(N) <= slope * N hold?

Equations

• LeanCert.Engine.ChebyshevPsi.checkPsiLeMulWith N slope depth = decide (LeanCert.Engine.ChebyshevPsi.psiUB N depth ≤ slope * ↑N)

theorem LeanCert.Engine.ChebyshevPsi.psi_le_of_checkPsiLeMulWith (N depth : ℕ) (slope : ℚ) (h : checkPsiLeMulWith N slope depth = true) : Chebyshev.psi ↑N ≤ ↑slope * ↑N

If checkPsiLeMulWith N slope depth holds, then psi(N) <= slope * N.

theorem LeanCert.Engine.ChebyshevPsi.psi_le_mul_real_of_checkPsiLeMulWith (x : ℝ) (slope : ℚ) (depth : ℕ) (hslope : 0 ≤ slope) (hx : 0 < x) (h : checkPsiLeMulWith ⌊x⌋₊ slope depth = true) : Chebyshev.psi x ≤ ↑slope * x

Real-variable form: if checkPsiLeMulWith floor(x) slope depth holds and slope >= 0, then psi(x) <= slope*x.

Backwards-compatible wrappers for slope = 111/100

def LeanCert.Engine.ChebyshevPsi.checkPsiBound (N : ℕ) (depth : ℕ := 20) : Bool

Legacy check used by downstream code: psiUB(N) <= 1.11 * N.

Equations

• LeanCert.Engine.ChebyshevPsi.checkPsiBound N depth = LeanCert.Engine.ChebyshevPsi.checkPsiLeMulWith N (111 / 100) depth

theorem LeanCert.Engine.ChebyshevPsi.psi_le_of_checkPsiBound (N depth : ℕ) (h : checkPsiBound N depth = true) : Chebyshev.psi ↑N ≤ 111 / 100 * ↑N

Legacy theorem used by downstream code: psi(N) <= 1.11 * N.

theorem LeanCert.Engine.ChebyshevPsi.psi_le_mul_real (x : ℝ) (depth : ℕ) (hx : 0 < x) (h : checkPsiBound ⌊x⌋₊ depth = true) : Chebyshev.psi x ≤ 111 / 100 * x

Real-variable legacy theorem: psi(x) <= 1.11 * x, given checkPsiBound floor(x) depth.

Efficient incremental checker (for #eval / native_decide testing)

def LeanCert.Engine.ChebyshevPsi.psiUBPrefix (n depth : ℕ) : ℚ

Helper: accumulate vonMangoldtUB from 1 to n-1.

Equations

• LeanCert.Engine.ChebyshevPsi.psiUBPrefix n depth = ∑ i ∈ Finset.Ioc 0 (n - 1), LeanCert.Engine.ChebyshevPsi.vonMangoldtUB i depth

def LeanCert.Engine.ChebyshevPsi.checkAllPsiLeMulWith (bound : ℕ) (slope : ℚ) (depth : ℕ := 20) : Bool

Efficient O(N) check that psiUB(N) <= slope * N for all N = 1..bound. Uses incremental accumulation instead of recomputing psiUB from scratch.

Equations

• LeanCert.Engine.ChebyshevPsi.checkAllPsiLeMulWith bound slope depth = LeanCert.Engine.ChebyshevPsi.checkAllPsiLeMulWith.go bound slope depth 1 0

@[irreducible]

def LeanCert.Engine.ChebyshevPsi.checkAllPsiLeMulWith.go (bound : ℕ) (slope : ℚ) (depth n : ℕ) (acc : ℚ) : Bool

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.ChebyshevPsi.allPsiBoundsHold (bound : ℕ) (depth : ℕ := 20) : Bool

Legacy O(N) checker for slope = 111/100.

Equations

• LeanCert.Engine.ChebyshevPsi.allPsiBoundsHold bound depth = LeanCert.Engine.ChebyshevPsi.checkAllPsiLeMulWith bound (111 / 100) depth

Bridge: checkAllPsiLeMulWith.go -> checkPsiLeMulWith

theorem LeanCert.Engine.ChebyshevPsi.checkAllPsiLeMulWith_implies_checkPsiLeMulWith (bound : ℕ) (slope : ℚ) (depth : ℕ) (h : checkAllPsiLeMulWith bound slope depth = true) (N : ℕ) (hN : 0 < N) (hNb : N ≤ bound) : checkPsiLeMulWith N slope depth = true

If checkAllPsiLeMulWith bound slope depth returns true, then checkPsiLeMulWith N slope depth is true for all N in {1, ..., bound}.

theorem LeanCert.Engine.ChebyshevPsi.allPsiBoundsHold_implies_checkPsiBound (bound depth : ℕ) (h : allPsiBoundsHold bound depth = true) (N : ℕ) (hN : 0 < N) (hNb : N ≤ bound) : checkPsiBound N depth = true

Legacy bridge theorem for slope = 111/100.