prime_sixhundredthirteen
plain-language theorem explainer
613 is asserted to be a prime natural number. Number theorists applying Möbius inversion or arithmetic functions in the Recognition Science setting would cite this fact when checking small primes for squarefree decompositions. The proof is a one-line computational wrapper that invokes native_decide for direct verification.
Claim. $613$ is a prime number in the natural numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard primality predicate on naturals. Upstream results supply the basic interface for collision-free structures and algebraic tautologies that frame the surrounding number-theoretic scaffolding.
proof idea
The proof is a one-line term wrapper that applies native_decide to confirm primality of 613 by direct evaluation.
why it matters
This supplies a verified small prime for the arithmetic functions module, supporting Möbius calculations and squarefree checks. It rests on the basic Prime alias and feeds no downstream theorems in the current graph. No direct tie to the forcing chain T5-T8 or RS constants appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.