primeCounting_seventeen
plain-language theorem explainer
The declaration establishes that exactly seven primes exist at or below 17. Number theorists checking explicit small values of the prime counting function or assembling arithmetic identities would reference this checkpoint. The proof reduces to a single native decision procedure that evaluates the count directly from the underlying definition.
Claim. $π(17) = 7$
background
The prime counting function π(n) returns the cardinality of the set of primes ≤ n. In this module it is introduced as a thin wrapper around the standard library implementation. The surrounding file supplies lightweight arithmetic-function interfaces, beginning with the Möbius function μ, to prepare for Dirichlet inversion once the basic signatures stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to the equality, delegating the verification to Lean’s built-in decision procedure on the concrete natural-number value.
why it matters
This supplies an explicit numerical anchor for the prime counting function inside the arithmetic-functions module. It can serve as a reference point for later identities that combine π with the Möbius function or other arithmetic operations, although no downstream uses are recorded yet. Within the Recognition Science setting such concrete evaluations provide verifiable base cases for any number-theoretic steps that appear in the forcing chain or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.