prime_twohundredfiftyseven
plain-language theorem explainer
257 equals 2^8 + 1 and is the third Fermat prime. Number theorists using arithmetic functions or prime distributions in the Recognition Science setup would reference this fact for Möbius calculations on primes. The proof is a one-line native_decide wrapper that computationally confirms the property.
Claim. $257$ is prime, where $257 = 2^8 + 1$ is the Fermat prime $F_3$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. Prime is defined locally as the transparent alias for Nat.Prime. Upstream results include the Prime abbrev and various 'is' structures from foundation modules that certify algebraic or collision-free properties without new axioms.
proof idea
The proof is a one-line wrapper that applies native_decide to verify primality of 257.
why it matters
This supplies a concrete primality fact inside the arithmetic functions layer that supports Möbius applications on primes. It fills the specific claim noted in the doc-comment for F_3. No downstream uses appear, so it serves as a basic building block rather than a parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.