WeakPNT
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.
claimAssume 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 in Recognition Science
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.
scope and limits
- Does not derive the limit from the J-function or Recognition Composition Law.
- Does not supply error terms or stronger forms of the prime number theorem.
- Does not invoke Tauberian theorems or complex analysis.
formal statement (Lean)
51theorem WeakPNT
52 (hWeak :
53 Tendsto (fun N ↦ (∑ n ∈ Finset.Iic N, ArithmeticFunction.vonMangoldt n) / N)
54 atTop (nhds 1)) :
55 Tendsto (fun N ↦ (∑ n ∈ Finset.Iic N, ArithmeticFunction.vonMangoldt n) / N)
56 atTop (nhds 1) := hWeak
proof body
Term-mode proof.
57
58/-- **TECHNICAL SCAFFOLD**: Chebyshev ψ is asymptotic to x. -/