primeCounting_three
plain-language theorem explainer
The declaration verifies that the prime counting function evaluates to 2 at input 3. Number theorists checking small cases of arithmetic functions or preparing base facts for Dirichlet inversion would cite this result. The proof is a direct native decision procedure that evaluates the definition without additional lemmas.
Claim. $π(3) = 2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The prime counting function is defined by π(n) := Nat.primeCounting n, which counts the primes ≤ n. This theorem appears among sibling results on Möbius properties for squarefree integers and provides a concrete small-case verification.
proof idea
The proof is a one-line wrapper that applies native_decide to the equality, which computes the value of primeCounting 3 directly from its definition and confirms equality to 2.
why it matters
This supplies a verified base case for the prime counting function inside the arithmetic functions module. It supports the module's stated aim of stabilizing basic interfaces before adding Dirichlet algebra and inversion. No downstream uses are recorded, so the result remains available for later integration with Recognition Science calculations such as mass ladders or forcing-chain constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.