primeCounting_fifty
plain-language theorem explainer
The declaration asserts that exactly fifteen primes lie at or below fifty. Researchers checking explicit small values of the prime counting function would cite this verified instance. The proof reduces to a single native decision procedure that evaluates the definition directly.
Claim. $π(50) = 15$
background
The prime counting function is defined by π(n) = #{p ≤ n : p prime} and implemented as Nat.primeCounting n. This module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function, to support Dirichlet algebra and inversion once interfaces stabilize. The upstream definition primeCounting provides the core count used here.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the equality directly.
why it matters
This supplies a verified base case for the prime counting function in the arithmetic functions module. It supports downstream number-theoretic arguments within the Recognition Science framework, though no immediate parent theorems are listed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.