primeCounting_thirteen
plain-language theorem explainer
The prime counting function evaluates to exactly 6 at the integer 13, confirming the six primes not exceeding that bound. Number theorists checking explicit small values or building arithmetic function libraries would reference this computation. The proof reduces directly to a native decision procedure applied to the definition of the counting function.
Claim. $π(13) = 6$
background
The prime counting function is defined as π(n) = #{p ≤ n : p prime} and implemented by delegating to Mathlib's Nat.primeCounting. This module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function μ, to support Dirichlet algebra and inversion once interfaces stabilize. The result relies on the upstream definition of primeCounting, which delegates to the standard natural number prime counter.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the equality on the concrete natural number 13.
why it matters
This theorem provides an explicit small-case verification within the arithmetic functions module of the NumberTheory.Primes section. It supports the development of prime-related tools that may feed into broader Recognition Science constructions involving number-theoretic functions, though no downstream uses are recorded yet. It aligns with the framework's need for precise counting in foundational number theory steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.