prime_twohundredfortyone
plain-language theorem explainer
241 is established as a prime natural number. Researchers applying Möbius inversion or arithmetic functions in the Recognition Science framework would cite this to confirm small prime factors. The proof is a direct computational check via native_decide.
Claim. $241$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the repo-local alias for Nat.Prime. Upstream results supply collision-free and tautological structures from foundation modules together with the transparent Prime abbreviation.
proof idea
The proof is a one-line term that invokes native_decide to computationally verify the primality of 241.
why it matters
This theorem supplies a verified small prime inside the arithmetic-functions module that supports later Möbius and squarefree machinery. It fills a concrete verification step for the number-theory layer of the Recognition Science monolith without touching the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.