repunit_index_twentythree
plain-language theorem explainer
The theorem asserts that 23 is prime, supplying the index for repunit R_23 in the Recognition Science arithmetic setup. Number theorists working on repunit constructions or prime indices for Möbius-related functions would cite this result. The proof is a one-line computational verification that applies native decision procedures directly to the natural number 23.
Claim. The natural number 23 is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and its squarefree properties before deeper Dirichlet algebra is added. The local setting treats primality via a transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream results include foundational structures such as collision-free option programs and simplicial ledger identifications, though the direct dependence for this statement is the primality predicate itself.
proof idea
The proof is a term-mode one-line wrapper that applies the native_decide tactic to perform an immediate computational check of primality for 23.
why it matters
This result supplies the R_23 component in the repunit prime index list, as stated in the declaration comment, and supports the arithmetic functions module within the Recognition Science number theory section. It connects to prime usage in Möbius inversions and related constructions, though the usage graph lists no downstream theorems. It touches the verification of specific primes relevant to RS-native ladders and constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.