StrongPNT_conditional
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.
claimAssuming 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 in Recognition Science
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.
scope and limits
- Does not prove the Riemann hypothesis.
- Does not establish the bound unconditionally.
- Does not supply an explicit value for C.
- Does not apply the bound to finite or small x.
formal statement (Lean)
89theorem StrongPNT_conditional (hRH : True) -- RH placeholder
90 (hStrong : ∃ C > 0, (ψ - id) =O[atTop] fun x ↦ Real.sqrt x * (Real.log x) ^ 2) :
91 ∃ C > 0, (ψ - id) =O[atTop] fun x ↦ Real.sqrt x * (Real.log x) ^ 2
92 := hStrong
proof body
Term-mode proof.
93
94/-! ## Consequences for Prime Counting -/
95
96/-- **TECHNICAL SCAFFOLD**: Prime between consecutive integers for large N. -/