primeCounting_one
The prime counting function evaluates to zero at one. Number theorists using the Recognition Science arithmetic layer would cite this base case when starting inductive arguments over the primes. The proof is a one-line simplification that unfolds the wrapper definition directly to Mathlib's Nat.primeCounting.
claim$π(1) = 0$, where $π(n)$ counts the primes less than or equal to $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The upstream definition states that the prime counting function π(n) equals the cardinality of primes p ≤ n, implemented as a direct alias to Nat.primeCounting. This places the declaration in the initial interface layer before deeper Dirichlet inversion is added.
proof idea
The proof is a one-line term-mode simplification that unfolds primeCounting and reduces via Nat.primeCounting.
why it matters in Recognition Science
This base case anchors the prime counting function at the start of the naturals inside the Recognition Science number theory module. It supports future inductive constructions over primes without yet feeding any listed downstream theorems. The result closes the trivial instance consistent with the module's focus on small arithmetic interfaces.
scope and limits
- Does not compute π(n) for any n > 1.
- Does not connect π to the J-cost, phi-ladder, or Recognition Composition Law.
- Does not invoke forcing chain steps T0-T8 or dimension D=3.
formal statement (Lean)
358theorem primeCounting_one : primeCounting 1 = 0 := by
proof body
Term-mode proof.
359 simp [primeCounting, Nat.primeCounting]
360
361/-- π(2) = 1. -/