fermat_zero
plain-language theorem explainer
fermat_zero asserts that the zeroth Fermat number equals 3 and is prime. Number theorists building base cases for Fermat sequences or arithmetic foundations in Recognition Science would cite this explicit verification. The proof is a one-line term that invokes native_decide to evaluate the expression and confirm primality.
Claim. The integer $2^{2^0} + 1$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting keeps statements minimal so that Dirichlet inversion can be added once interfaces stabilize. The predicate Prime is the repository alias for Nat.Prime.
proof idea
The proof is a one-line term that applies native_decide to the concrete value 2^(2^0)+1 and returns the primality judgment.
why it matters
It supplies the base verified Fermat prime inside the arithmetic-functions section of the primes development. No downstream uses are recorded. The fact sits among other explicit prime constructions that support the number-theory layer of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.