repunit_prime_two
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove primality for larger repunits.
- Does not connect the result to the Recognition Composition Law.
- Does not address general arithmetic function properties.
formal statement (Lean)
2359theorem repunit_prime_two : Prime 11 ∧ 11 = (10^2 - 1) / 9 := by native_decide
proof body
Term-mode proof.
2360
2361/-- R_19 component: 19 is prime (indexes repunit R_19 which is also prime). -/