ChebyshevPsi
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 in Recognition Science
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.
scope and limits
- Does not establish any asymptotic or limit statement for ψ(x).
- Does not restrict x to positive reals or impose growth conditions.
- Does not embed Recognition Science constants such as phi or the eight-tick octave.
- Does not discharge the weak prime number theorem hypothesis.
- Does not reference the J-cost or defectDist structures directly.
formal statement (Lean)
36def ChebyshevPsi (x : ℝ) : ℝ :=
proof body
Definition body.
37 ∑ n ∈ Finset.Iic ⌊x⌋₊, ArithmeticFunction.vonMangoldt n
38
39/-- Local notation for Chebyshev ψ -/
40local notation "ψ" => ChebyshevPsi
41
42/-! ## Weak Prime Number Theorem -/
43
44/-- **TECHNICAL SCAFFOLD**: Weak Prime Number Theorem.
45
46 The average of the von Mangoldt function tends to 1:
47 ∑_{n≤N} Λ(n) / N → 1 as N → ∞
48
49 **Note**: Exposed as an explicit hypothesis until a full Lean derivation
50 is landed (Wiener-Ikehara Tauberian infrastructure). -/