mersenne_two
plain-language theorem explainer
The declaration asserts that 3 is prime because 2 squared minus 1 satisfies the standard primality predicate. Number theorists building arithmetic function layers or prime ladders inside Recognition Science would reference the result for the smallest Mersenne case. The verification reduces directly to a computational decision procedure on the small integer.
Claim. $2^{2}-1=3$ is a prime number under the standard definition of primality for natural numbers.
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 and related algebra can be added later. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream dependencies include structural assertions from OptionAEmpiricalProgram, SimplicialLedger, GameTheory, and RamanujanBridge modules that supply the broader Recognition Science scaffolding in which this number-theoretic fragment sits.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic. This tactic evaluates the primality predicate by direct computation on the concrete value 3, discharging the goal without explicit case analysis or induction.
why it matters
The result supplies a basic verified case inside the primes submodule that supports arithmetic-function definitions such as Möbius. It contributes to the number-theory layer that Recognition Science uses to reach mass ladders and constants. No downstream uses are recorded yet, so the declaration functions as foundational scaffolding rather than a direct link to T5–T8 forcing steps or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.