vonMangoldt
The von Mangoldt function is supplied as a direct alias to the standard arithmetic function that returns log p on prime powers p^k and zero elsewhere. Number theorists building the prime number theorem port would cite this wrapper when constructing the Chebyshev psi sum or the weak PNT hypothesis. The implementation is a one-line alias to Mathlib's ArithmeticFunction.vonMangoldt.
claimThe von Mangoldt arithmetic function is the map from natural numbers to reals that satisfies Lambda(n) = log p whenever n equals p^k for prime p and integer k at least 1, and Lambda(n) = 0 otherwise.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Moebius function and extending to the von Mangoldt function. Arithmetic functions here are maps from naturals to reals used for encoding multiplicative structure in Dirichlet series and sums over divisors. The local setting keeps statements minimal until deeper inversion formulas stabilize.
proof idea
The declaration is a one-line wrapper that aliases Mathlib's ArithmeticFunction.vonMangoldt.
why it matters in Recognition Science
This definition supplies the von Mangoldt function to the Chebyshev psi construction and the weak prime number theorem scaffold in the PNT port. It fills the arithmetic function interface needed for sums that appear in the prime number theorem derivations. The module positions these as footholds for Dirichlet algebra once the basic interfaces stabilize.
scope and limits
- Does not prove any properties of the function.
- Does not derive the prime number theorem or its weak form.
- Does not connect to the Recognition Science forcing chain or phi-ladder.
formal statement (Lean)
141noncomputable abbrev vonMangoldt : ArithmeticFunction ℝ := ArithmeticFunction.vonMangoldt
proof body
Definition body.
142