StrongPNT_conditional
plain-language theorem explainer
StrongPNT_conditional supplies the bound ψ(x) − x = O(√x log² x) as x → ∞ under a placeholder for the Riemann hypothesis. Researchers porting analytic number theory into the Recognition monolith cite it when chaining conditional statements to obtain the prime counting asymptotic. The proof is a one-line term that returns the input hypothesis hStrong directly.
Claim. Assuming the Riemann hypothesis, there exists a constant C > 0 such that the Chebyshev function satisfies ψ(x) − x = O(√x (log x)²) as x → ∞.
background
The module NumberTheory.Port.PNT contains conditional ports of classical prime-number results. The Chebyshev function ψ(x) sums log p over prime powers p^k ≤ x, while id is the identity function; the notation =O[atTop] denotes the standard big-O relation at infinity. The upstream Prime abbreviation is simply Nat.Prime, and identity morphisms from CostAlgebra and Octave supply the algebraic scaffolding used throughout the forcing chain.
proof idea
The proof is a term-mode one-liner that returns the hypothesis hStrong. The placeholder hRH is accepted but never used; no lemmas from the depends-on list are applied.
why it matters
This scaffold feeds directly into prime_counting_asymptotic_pnt, which records the prime-counting asymptotic π(x) ∼ x / log x. It occupies the strong-PNT slot in the NumberTheory port and supports later connections to the eight-tick octave and D = 3. The RH placeholder remains an open question for an unconditional version.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.