prime_fivehundredtwentyone
plain-language theorem explainer
521 is established as a prime natural number. Number theorists working with arithmetic functions in the Recognition Science framework would cite this when verifying Möbius values or squarefree status at concrete integers. The proof is a one-line wrapper that invokes native_decide for direct computational confirmation.
Claim. $521$ is prime, where primality means the natural number has no positive divisors other than $1$ and itself.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function. Prime is the repo-local alias for the standard predicate that a natural number is prime. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the primality predicate directly via computation.
why it matters
This supplies a concrete prime fact inside the arithmetic-functions module that can feed Möbius and squarefree lemmas. It sits in the NumberTheory.Primes layer that supports later Recognition Science constructions involving integer ladders and constants. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.