prime_threehundredeleven
plain-language theorem explainer
311 is established as prime. Number theorists using arithmetic functions for Möbius inversion in the Recognition Science module would cite this when verifying small primes in squarefree checks. The proof is a one-line native decision procedure that directly evaluates the primality predicate.
Claim. The natural number $311$ is prime, meaning it has no positive divisors other than $1$ and itself.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime, the standard predicate that n is prime when its only positive divisors are 1 and n. This theorem appears among siblings that define mobius, bigOmega, and squarefree conditions for later Dirichlet inversion work.
proof idea
The proof is a one-line term that applies native_decide to the primality predicate on 311.
why it matters
This supplies a verified small-prime fact inside the arithmetic-functions module that supports Möbius applications. It fills a basic number-theory foothold with no recorded downstream uses and no direct connection to the forcing chain, RCL, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.