mersenne_three
plain-language theorem explainer
The result establishes that 7 is prime as the Mersenne number obtained from exponent 3. Number theorists working with elementary verified facts inside the Recognition Science arithmetic functions module would cite it as a base case. The proof reduces the primality predicate to a direct computational check via native decision.
Claim. The integer $2^3 - 1$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, and keeps statements minimal until Dirichlet algebra layers are added. The local setting treats primality through a transparent alias for the standard natural-number predicate. Upstream results include foundational 'is' predicates from empirical programs and simplicial ledgers that enforce collision-free or tautological properties, together with the basic primality abbreviation.
proof idea
The proof is a one-line term proof that applies native_decide to resolve the decidable primality statement by direct evaluation.
why it matters
It records a concrete small Mersenne prime inside the primes arithmetic functions file. No downstream theorems reference it yet, but the fact accumulates elementary number-theoretic material that may later support prime-ladder constructions. It sits apart from the forcing chain steps T5 through T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.