primeCounting_eleven
plain-language theorem explainer
The declaration asserts that the prime counting function evaluates to 5 at argument 11. Number theorists checking explicit small values of π(n) for base cases in arithmetic computations would reference this result. The proof reduces immediately to a native decision procedure that evaluates the definition directly.
Claim. $π(11) = 5$
background
The prime counting function is defined as π(n) = #{p ≤ n : p prime} and implemented as a direct wrapper around Mathlib's Nat.primeCounting. This module supplies lightweight wrappers for arithmetic functions, beginning with the Möbius function μ, to support Dirichlet algebra and inversion once interfaces stabilize. The upstream definition primeCounting supplies the core count without additional structure.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the definition of primeCounting at 11 directly.
why it matters
This result supplies an explicit small-value check for the prime counting function inside the arithmetic functions module. It anchors basic number theoretic facts needed for later prime distribution arguments, though no immediate parent theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.