primeCounting_twenty
plain-language theorem explainer
The declaration establishes that the prime counting function evaluates to 8 at 20. Number theorists checking explicit small values in the arithmetic functions layer would cite this result for direct verification. The proof is a one-line native_decide term that reduces the equality to a decidable computation from the underlying definition.
Claim. $π(20) = 8$, where $π(n)$ counts the primes $p ≤ n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and the prime counting function. The prime counting function is defined by π(n) := Nat.primeCounting n, which returns the cardinality of primes ≤ n. This explicit evaluation sits in the same file as the Möbius definitions and provides a concrete check before deeper Dirichlet inversion is layered on.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the equality primeCounting 20 = 8, which computes both sides directly from the definition and confirms the match.
why it matters
This result supplies a verified small-case instance of the prime counting definition in the NumberTheory.Primes layer. It follows immediately from the primeCounting definition and supports concrete checks that can feed into larger arithmetic function statements, though no downstream uses are recorded yet. It aligns with the framework's practice of fixing explicit values before invoking inversion or Möbius relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.