prime_threehundredeightythree
plain-language theorem explainer
383 is established as a prime natural number. Researchers applying arithmetic functions such as the Möbius function in prime-related calculations within Recognition Science would cite this result for verification of small primes. The proof is a direct computational check via the native_decide tactic.
Claim. The natural number $383$ is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. The local setting keeps statements minimal to allow later addition of Dirichlet algebra and inversion once basic interfaces stabilize. Prime is a transparent alias for the standard Nat.Prime predicate.
proof idea
The proof is a one-line term that invokes native_decide to computationally verify the primality of 383.
why it matters
This supplies a verified small-prime fact inside the arithmetic-functions module, supporting potential Möbius evaluations. It does not feed any recorded downstream theorems. The declaration remains isolated from the forcing chain, phi-ladder, and Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.