ChebyshevPsi
plain-language theorem explainer
ChebyshevPsi defines the classical Chebyshev psi function as the partial sum of the von Mangoldt function over positive integers up to floor(x). Number theorists porting analytic estimates into the Recognition Science framework cite this as the base object for Chebyshev-type bounds and prime counting. The implementation is a direct one-line definition that applies the standard summation over Finset.Iic of ArithmeticFunction.vonMangoldt.
Claim. $ψ(x) := ∑_{n ≤ x} Λ(n)$, where Λ denotes the von Mangoldt arithmetic function.
background
The NumberTheory.Port.PNT module ports classical prime distribution tools into the Recognition Science setting. ChebyshevPsi supplies the standard ψ function used for the weak prime number theorem scaffold, which treats the average of Λ(n) tending to 1 as an explicit hypothesis pending full Wiener-Ikehara infrastructure. The von Mangoldt function Λ(n) equals log p when n is a prime power p^k and zero otherwise. Upstream structures from PhiForcingDerived calibrate J-cost while SimplicialLedger.ContinuumBridge and EdgeLengthFromPsi link ledger factors to continuum limits, providing the broader calibration context even though this definition itself remains a direct port.
proof idea
The definition is a direct transcription of the classical sum. It applies the Finset.Iic operator to ⌊x⌋₊ and sums ArithmeticFunction.vonMangoldt over that initial segment. No additional lemmas or tactics are invoked beyond the built-in summation notation.
why it matters
This definition anchors the weak prime number theorem scaffold and the subsequent conditional PNT statements in the module. It supplies the counting object needed to connect prime distribution to the Recognition Science forcing chain, including T5 J-uniqueness and the phi-ladder mass formula. Sibling declarations such as WeakPNT and StrongPNT_conditional depend on it as the base object; the module comment flags the weak form as a technical scaffold until a full derivation lands.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.