primeCounting_five
plain-language theorem explainer
The declaration establishes that the prime counting function evaluates to 3 at input 5. Number theorists checking small explicit cases of arithmetic functions would cite this result. The proof proceeds by a direct computational decision that evaluates the equality from the underlying definition.
Claim. $π(5) = 3$
background
The prime counting function is defined as π(n) = #{p ≤ n : p prime}, implemented by delegating to Mathlib's Nat.primeCounting. This module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function μ, and keeps statements basic to allow later layering of Dirichlet algebra. The upstream result primeCounting is the direct definition that this theorem evaluates at the concrete point 5.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute primeCounting 5 from its definition and verify equality to 3.
why it matters
This theorem supplies a verified base case inside the arithmetic functions module that supports incremental construction of number-theoretic tools. It fills a concrete small-instance check in the primes layer, consistent with the module's role as a foothold for Möbius-based inversion, though no downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.