fermat_three
plain-language theorem explainer
The theorem confirms that 257, equal to 2 raised to the power 8 plus 1, is a prime number and thus the Fermat prime F_3. Number theorists verifying small Fermat numbers or assembling exact arithmetic facts in the Recognition Science mirror would cite this result. The proof proceeds by a direct term-mode call to native_decide that evaluates the primality predicate on the concrete integer.
Claim. $2^{2^3} + 1 = 257$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local alias Prime stands for the standard predicate Nat.Prime on natural numbers. Upstream results supply this alias together with several foundational structures whose is-instances are imported but not invoked in the primality check itself.
proof idea
The proof is a one-line term-mode wrapper that applies native_decide to discharge the primality goal by direct integer evaluation.
why it matters
The declaration supplies a verified Fermat prime fact inside the primes section of the arithmetic-functions module. It populates exact number-theoretic building blocks that can feed later Dirichlet or inversion arguments, though no downstream uses are recorded yet. The result aligns with the framework's requirement for concrete, machine-checked constants before layering more abstract structures such as the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.