primeCounting_fourhundred
plain-language theorem explainer
The declaration asserts that exactly 78 primes exist at or below 400. Number theorists checking explicit values of the prime counting function in small ranges would cite this verified instance. The proof is a one-line term that invokes native_decide to evaluate the count from the underlying definition.
Claim. $π(400) = 78$, 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 prime counting function is introduced as the standard count of primes up to a given natural number. Its definition delegates directly to Nat.primeCounting, providing the concrete numerical interface used by this theorem.
proof idea
The proof is a one-line term wrapper that applies native_decide to the equality primeCounting 400 = 78.
why it matters
This supplies a concrete numerical check for the prime counting function inside the arithmetic functions module. It anchors explicit evaluations that can support later Möbius-based identities or prime-distribution statements in the Recognition Science number-theory layer, even though no downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.