isolated_prime_twentythree
plain-language theorem explainer
23 qualifies as an isolated prime because it is prime while its immediate neighbors 21 and 25 are composite. Number theorists working with small-case verifications in the Recognition Science arithmetic functions layer would cite the result for concrete checks on prime isolation. The proof reduces the entire conjunction to a single native_decide computation that settles the decidable arithmetic facts directly.
Claim. Let Prime$(n)$ denote that the natural number $n$ is prime. Then Prime$(23) ∧ ¬Prime$(21) ∧ ¬Prime$(25).
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent repo-local alias for the standard Nat.Prime predicate. The local theoretical setting keeps statements minimal while deeper Dirichlet algebra remains to be layered on. Upstream results include the Prime definition together with several 'is' structures from foundation and game-theory modules that enforce algebraic or collision-free properties, though the immediate dependence for this theorem is only the primality predicate.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the three primality statements, reducing them to direct decidable computation.
why it matters
The declaration supplies a concrete small-case verification inside the primes arithmetic functions file. It anchors the isolated-prime notion noted in the doc-comment and supports the NumberTheory layer without invoking the Recognition Composition Law or the T5–T8 forcing chain. No downstream theorems are recorded among the used-by edges, so the result functions as a terminal check rather than a lemma for further development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.