WeakPNT
plain-language theorem explainer
The weak prime number theorem asserts that the Cesaro mean of the von Mangoldt function tends to one as the upper limit tends to infinity. Analytic number theorists cite this Chebyshev form when building toward the full prime number theorem. The Lean proof is a term that returns the supplied hypothesis without further reduction.
Claim. Assume the limit as $N$ tends to infinity of the sum of the von Mangoldt function up to $N$, divided by $N$, equals one. Then the same limit holds.
background
The von Mangoldt function maps each natural number to the logarithm of its prime factor when the number is a prime power and to zero otherwise. This declaration resides in the PNT port module as an explicit placeholder. It draws on the arithmetic function definition from the Primes.ArithmeticFunctions sibling and on interface structures from Foundation modules that encode collision-free empirical programs and simplicial ledger edge lengths.
proof idea
The proof is a term-mode one-liner that returns the hypothesis hWeak directly.
why it matters
It supplies the hypothesis for the prime_counting_asymptotic_pnt theorem that states the prime counting function is asymptotic to x over log x. The declaration occupies the weak slot in the progression from ChebyshevPsi to MediumPNT and StrongPNT_conditional. In the Recognition Science setting it supports the number-theoretic layer but remains open to a derivation from J-uniqueness or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.