primeCounting_sevenhundredfifty
plain-language theorem explainer
The declaration establishes that the prime counting function evaluates to 132 at 750. Number theorists requiring explicit numerical values of π(n) for concrete arguments would cite this result. The proof is a one-line native_decide application that evaluates the definition directly.
Claim. $π(750) = 132$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the prime counting function. The prime counting function is defined as π(n) := #{p ≤ n : p prime} and implemented directly via Nat.primeCounting. This concrete evaluation appears among other arithmetic identities in the file, with the module keeping statements minimal before deeper Dirichlet algebra is added.
proof idea
The proof is a one-line wrapper that applies native_decide to compute primeCounting 750 from its definition as Nat.primeCounting.
why it matters
This supplies a verified concrete instance of the prime counting function inside the arithmetic functions module. It fills the explicit numerical claim π(750) = 132 noted in the declaration comment. No downstream uses are recorded, but the result contributes to the foundational number theory layer supporting Recognition Science constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.