primeCounting_sixhundred
plain-language theorem explainer
The prime counting function satisfies π(600) = 109. Number theorists testing explicit small-n values or validating arithmetic-function wrappers would cite this result. The proof is a one-line native decision that evaluates the count directly.
Claim. $π(600) = 109$
background
The prime counting function π(n) is defined as the cardinality of primes p ≤ n. This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ, to prepare for Dirichlet inversion once the interfaces stabilize. The upstream declaration primeCounting simply delegates to the standard Nat.primeCounting implementation.
proof idea
The proof is a one-line wrapper that applies native_decide to reduce the equality to a decidable computation of the prime count at 600.
why it matters
This supplies a concrete numerical anchor for the prime counting definition inside the arithmetic-functions module. No downstream results currently depend on it, so it functions as a verification checkpoint rather than a lemma in a larger chain. It supports consistency checks for Möbius-based identities that presuppose accurate prime enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.