mersenne_seven
plain-language theorem explainer
The declaration asserts that 127, written as 2^7 minus 1, meets the definition of a prime number. Number theorists working on Mersenne primes or specific arithmetic cases in the Recognition Science setting would reference this fact. The verification proceeds as a direct computational check via native decision procedures.
Claim. The integer $2^7 - 1$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, to support Dirichlet algebra once basic interfaces stabilize. This result appears in the primes subsection and relies on the local alias for the standard primality predicate on natural numbers. Upstream results include the primality alias for the Mathlib predicate together with structural hypotheses ensuring algebraic consistency across foundational modules.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to confirm primality of 127 by direct computation.
why it matters
This supplies a concrete Mersenne prime instance that anchors arithmetic facts required for prime distributions in the Recognition Science framework. It sits alongside the eight-tick octave and phi-ladder constructions without feeding any recorded parent theorems. No open questions are discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.