primeCounting_one
plain-language theorem explainer
The prime counting function evaluates to zero at one. Number theorists using the Recognition Science arithmetic layer would cite this base case when starting inductive arguments over the primes. The proof is a one-line simplification that unfolds the wrapper definition directly to Mathlib's Nat.primeCounting.
Claim. $π(1) = 0$, where $π(n)$ counts the primes less than or equal to $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The upstream definition states that the prime counting function π(n) equals the cardinality of primes p ≤ n, implemented as a direct alias to Nat.primeCounting. This places the declaration in the initial interface layer before deeper Dirichlet inversion is added.
proof idea
The proof is a one-line term-mode simplification that unfolds primeCounting and reduces via Nat.primeCounting.
why it matters
This base case anchors the prime counting function at the start of the naturals inside the Recognition Science number theory module. It supports future inductive constructions over primes without yet feeding any listed downstream theorems. The result closes the trivial instance consistent with the module's focus on small arithmetic interfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.