fermat_one
plain-language theorem explainer
Number theorists citing base cases for Fermat primes in arithmetic function contexts would reference the verification that 2^(2^1) + 1 equals 5 and is prime. The result supplies an explicit instance of a Fermat prime. The proof reduces to a single native_decide invocation that computes the value and applies the primality predicate.
Claim. The integer $2^{2^1} + 1$ is prime.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Statements stay minimal to permit later layering of Dirichlet algebra and inversion. The theorem uses the repo-local alias Prime, defined as the standard Nat.Prime predicate.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate 2^(2^1) + 1 and confirm it satisfies the Prime predicate.
why it matters
It furnishes a verified Fermat prime instance inside the primes section of arithmetic functions. No downstream uses appear in the used_by list, yet the result could anchor later prime-distribution or Möbius-related statements. It supplies concrete number-theoretic scaffolding without direct linkage to the forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.