primeCounting_seventeen
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 in Recognition Science
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.
scope and limits
- Does not prove the prime number theorem or any asymptotic statement.
- Does not compute π(n) for any n other than 17.
- Does not invoke or relate to the Möbius function.
- Does not supply a non-computational or analytic proof.
formal statement (Lean)
390theorem primeCounting_seventeen : primeCounting 17 = 7 := by
proof body
Term-mode proof.
391 native_decide
392
393/-- π(20) = 8. -/