vonMangoldt_prime
plain-language theorem explainer
The result states that the von Mangoldt function evaluates to the natural logarithm of p whenever p is prime. Number theorists building prime-power identities inside the Recognition Science arithmetic layer would cite it as the base case for extensions to higher powers. The proof is a one-line wrapper that converts the custom Prime predicate via prime_iff and invokes the standard Mathlib evaluation lemma for the von Mangoldt arithmetic function.
Claim. Let $p$ be a prime number. Then the von Mangoldt function satisfies $Λ(p) = log p$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting from the Möbius function and extending to the von Mangoldt function. The von Mangoldt function is introduced as the arithmetic function that returns the natural logarithm of the underlying prime when its argument is a prime power and zero otherwise. The Prime predicate is the Recognition Science wrapper for primality; it is related to Mathlib's Nat.Prime by the prime_iff equivalence stated in the Basic file.
proof idea
The proof first obtains Nat.Prime p from the hypothesis Prime p by applying the left direction of prime_iff. It then reduces the goal by simp using the vonMangoldt abbreviation and the Mathlib lemma ArithmeticFunction.vonMangoldt_apply_prime applied to that Nat.Prime fact.
why it matters
This theorem supplies the base case used by the immediate downstream result vonMangoldt_prime_pow, which extends the identity to all prime powers. It anchors the arithmetic-function interface that supports prime-factorization steps in the Recognition Science number-theory layer, consistent with the phi-ladder constructions appearing elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.