primeCounting_def
plain-language theorem explainer
Recognition Science defines its prime counting function as a direct wrapper around the standard library implementation. Number theorists citing this in Lean proofs gain compatibility with the library version for counting primes up to n. The proof is a reflexivity step that equates the two by construction of the definition.
Claim. For every natural number $n$, the prime counting function satisfies $π(n) = π_{std}(n)$, where $π_{std}$ is the standard implementation that returns the count of primes at most $n$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The prime counting function is defined as the number of primes ≤ n. This theorem sits inside the NumberTheory.Primes.ArithmeticFunctions module, which imports Basic and Squarefree and prepares for later Dirichlet algebra layers.
proof idea
The proof is a term-mode reflexivity that directly matches the wrapper to its defining library call.
why it matters
This declaration secures compatibility for prime counting within the arithmetic functions module. It underpins potential uses in prime-related arguments, though no downstream applications are yet recorded. It fills a basic interface step in the NumberTheory.Primes section without direct connection to the main forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.