MediumPNT
plain-language theorem explainer
The MediumPNT theorem asserts the existence of c > 0 such that the Chebyshev psi function satisfies ψ(x) - x = O(x exp(-c (log x)^{1/10})) as x tends to infinity. Number theorists studying intermediate error terms in prime distribution would cite this bound when bridging weak and strong forms of the prime number theorem. The proof is a one-line term wrapper that returns the input hypothesis verbatim.
Claim. There exists a constant $c > 0$ such that the Chebyshev function satisfies $ψ(x) - x = O(x · exp(-c (log x)^{1/10}))$ as $x → ∞$.
background
In the NumberTheory.Port.PNT module the declaration supplies a medium-strength error bound for the prime number theorem as an explicit technical scaffold. The Chebyshev psi function ψ(x) sums log p over prime powers p^k ≤ x, while the identity supplies the main term x; the big-O notation is the standard asymptotic from Mathlib. Upstream results supply only identity morphisms (from Algebra.CostAlgebra.id and Foundation.ArithmeticOf.id) together with the transparent alias Prime for Nat.Prime, none of which alter the statement. The module imports Mathlib and Primes.Basic, placing the result in the classical setting of prime-counting asymptotics pending a full complex-analytic derivation.
proof idea
The proof is a term-mode one-liner that directly returns the supplied hypothesis hMedium. No lemmas are invoked beyond the input assumption.
why it matters
MediumPNT occupies an intermediate slot in the PNT chain and is used by the downstream prime_counting_asymptotic_pnt theorem that converts the psi bound into the classical π(x) ~ x / log x statement. The doc comment identifies it as a scaffold exposed until the full complex-analytic derivation is imported, consistent with the Recognition Science pattern of carrying arithmetic results forward to physical constants via the phi-ladder. It sits between the weaker WeakPNT and the conditional StrongPNT_conditional siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.