primeCounting_twohundred
plain-language theorem explainer
The prime counting function evaluates to 46 at 200. Number theorists validating small instances of prime distribution or checking arithmetic function implementations would cite this. The proof is a one-line wrapper that delegates the equality to native_decide on the underlying definition.
Claim. $π(200) = 46$, where $π(n)$ counts the primes $p ≤ n$.
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 by direct delegation to Nat.primeCounting. This sits in the NumberTheory.Primes.ArithmeticFunctions section, providing basic interfaces before deeper Dirichlet algebra.
proof idea
The proof is a one-line wrapper that applies native_decide to the equality primeCounting 200 = 46 after unfolding the definition.
why it matters
This supplies a verified small-case evaluation of the prime counting function inside the arithmetic functions module. It supports foundational number-theoretic computations in the Recognition Science framework but records no downstream uses and does not link to the forcing chain or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.