vonMangoldt_sum_divisors
plain-language theorem explainer
The identity states that the sum of the von Mangoldt function over the divisors of any natural number n equals the natural logarithm of n. Analytic number theorists working with prime-power factorizations would cite this when converting divisor sums into logarithmic terms. The proof is a one-line wrapper that unfolds the local vonMangoldt abbreviation and invokes Mathlib's standard sum theorem.
Claim. For every natural number $n$, $∑_{d|n} Λ(d) = log n$, where $Λ$ denotes the von Mangoldt function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to von Mangoldt. The von Mangoldt function is introduced as the noncomputable abbreviation vonMangoldt : ArithmeticFunction ℝ := ArithmeticFunction.vonMangoldt, which encodes the standard definition: log p on prime powers and zero elsewhere. The local theoretical setting keeps statements minimal so that Dirichlet algebra and inversion can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper. It applies simp only on the vonMangoldt abbreviation to expose the underlying Mathlib arithmetic function, then directly invokes the theorem ArithmeticFunction.vonMangoldt_sum that records the divisor-sum identity.
why it matters
This supplies the basic link between the von Mangoldt function and the logarithm, providing a foothold for arithmetic manipulations inside the Recognition Science number-theory layer. No downstream theorems currently depend on it, yet it aligns with the module's role of preparing Möbius-style tools that can later support forcing-chain arguments. It touches the standard fact that prime-power contributions sum to logarithmic growth without yet engaging the phi-ladder or J-uniqueness from the core T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.