repunit_prime_two
plain-language theorem explainer
The theorem verifies that 11 is prime and equals the repunit R_2 given by (10^2 - 1)/9. Number theorists consulting the Recognition Science primes module would cite this for small repunit checks inside arithmetic functions. The proof applies native_decide as a direct computational verification of the conjunction.
Claim. The number 11 is prime and satisfies $11 = (10^2 - 1)/9$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the repo-local alias for Nat.Prime. This theorem records the primality of the second repunit as a basic fact in the NumberTheory.Primes.ArithmeticFunctions file.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the conjunction of primality and the repunit equality.
why it matters
This supplies a verified instance of a repunit prime inside the arithmetic functions module. It supports prime-related scaffolding in the Recognition Science number theory layer, consistent with the framework's use of standard facts alongside the phi-ladder and eight-tick octave. No immediate downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.