fermat_four
65537 is asserted to be prime as the fourth Fermat number F_4. Number theorists checking small cases in Fermat prime lists or arithmetic progressions would cite the fact for verification. The proof proceeds by a single native_decide tactic that evaluates the expression and confirms primality directly.
claim$2^{2^4} + 1 = 65537$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and keeping statements minimal to support later Dirichlet inversion layers. The local setting is basic interface stabilization rather than full algebraic development. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the value of 2^(2^4)+1 and verify its primality at the meta level.
why it matters in Recognition Science
The declaration supplies a concrete verified instance of F_4 within the primes arithmetic functions section. No downstream uses appear in the used_by edges. It fills a specific computational case in the number-theoretic scaffolding but does not connect to the Möbius or inversion machinery developed in the same module.
scope and limits
- Does not prove any general property of Fermat numbers beyond this single case.
- Does not invoke or depend on the Möbius function defined in the module.
- Does not supply a primality test usable for other integers.
- Does not address infinitude or distribution of primes.
formal statement (Lean)
1268theorem fermat_four : Prime (2 ^ (2 ^ 4) + 1) := by native_decide
proof body
Term-mode proof.
1269
1270/-! ### Cousin primes (differ by 4) -/
1271
1272/-- 3 and 7 are cousin primes. -/