primeCounting
plain-language theorem explainer
The prime counting function π(n) counts the number of primes ≤ n and is supplied here as a direct alias to the standard library implementation. Analysts working on the Prime Number Theorem in the Recognition Science port cite this definition when stating asymptotics for π(x). The implementation is a one-line alias with no additional computation or hypotheses.
Claim. The prime counting function is defined by π(n) := |{p ∈ ℕ : p ≤ n and p is prime}|.
background
This module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The prime counting function is introduced as a basic interface to support later Dirichlet series and inversion formulas once the core definitions stabilize. It follows Mathlib conventions for ℕ and primes with no extra structure imposed.
proof idea
This is a one-line definition that aliases directly to Nat.primeCounting.
why it matters
The definition supplies the input to the asymptotic statements prime_counting_asymptotic and prime_counting_asymptotic_pnt, which encode the classical Prime Number Theorem π(x) ~ x / log x. It anchors the number-theoretic scaffolding used in the Recognition Science framework for the forcing chain, though it does not invoke J-cost or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.