primeCounting_eighthundred
plain-language theorem explainer
π(800) equals 139 by direct evaluation. Number theorists verifying explicit values of the prime counting function at moderate arguments would cite this result. The proof is a one-line native computation that evaluates the definition of primeCounting without invoking further lemmas.
Claim. $π(800) = 139$
background
The prime counting function π(n) is defined as the cardinality of the set of primes p ≤ n. This declaration lives in the ArithmeticFunctions module, which supplies lightweight wrappers around Mathlib arithmetic functions beginning with the Möbius function μ. The upstream definition primeCounting simply delegates to Nat.primeCounting n.
proof idea
The proof is a one-line wrapper that applies native_decide to compute primeCounting 800 directly from its definition.
why it matters
This supplies a concrete numerical instance of the prime counting function inside the arithmetic functions layer. No downstream theorems are listed as users. It contributes an explicit check that can support later Möbius inversion or prime-related calculations within the Recognition Science number-theory scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.