primeCounting_two
plain-language theorem explainer
The declaration establishes that the prime counting function evaluates to 1 at input 2. Number theorists checking base cases for prime enumeration or Möbius inversion setups would reference this equality. The proof reduces directly to a native decision procedure that confirms the single prime below or equal to 2.
Claim. $π(2) = 1$
background
The prime counting function is defined as π(n) = #{p ≤ n : p prime} and implemented via Mathlib's Nat.primeCounting. This module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function μ and related tools for Dirichlet inversion. The local setting focuses on small, verifiable statements that can serve as footholds for deeper algebraic number theory.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the equality by direct computation on the definition of primeCounting.
why it matters
This base case anchors the prime counting function within the arithmetic functions module. It supports subsequent developments in prime distribution and Möbius inversion techniques. No downstream uses are recorded yet, leaving room for integration into larger prime theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.