isolated_prime_sixtyseven
plain-language theorem explainer
67 is prime while both 65 and 69 are composite. Number theorists working with isolated primes inside the Recognition Science arithmetic-functions module would cite this explicit verification. The proof is a one-line wrapper that invokes native_decide for direct kernel computation of the primality predicates.
Claim. $67$ is prime while $65$ and $69$ are composite, where primality is the standard predicate on natural numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and keeping statements minimal until Dirichlet algebra stabilizes. The Prime predicate is the transparent alias for Nat.Prime imported from the Basic submodule. This theorem records a concrete isolated-prime instance whose adjacent integers factor as 5×13 and 3×23.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the conjunction of primality and non-primality statements.
why it matters
The declaration supplies a verified concrete fact in the primes section of the arithmetic-functions file. It supports number-theoretic infrastructure for Möbius applications within Recognition Science but has no downstream uses and does not touch the forcing chain, J-uniqueness, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.