primeCounting_hundred
plain-language theorem explainer
primeCounting_hundred establishes that exactly 25 primes exist up to 100. Number theorists verifying explicit values of the prime counting function inside the Recognition Science arithmetic setup would cite this result. The proof is a one-line native_decide evaluation of the definition.
Claim. $π(100) = 25$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and the prime counting function. primeCounting is defined by primeCounting n := Nat.primeCounting n, so that π(n) counts the primes ≤ n. The surrounding file keeps statements minimal to permit later addition of Dirichlet inversion once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality directly from the definition of primeCounting.
why it matters
This supplies a concrete numerical anchor for the prime counting function inside the NumberTheory.Primes.ArithmeticFunctions component. It supports consistency checks for the framework's arithmetic layer but does not connect to the forcing chain, J-uniqueness, or the phi-ladder. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.