isolated_prime_eightynine
plain-language theorem explainer
89 is prime while its immediate odd neighbors 87 and 91 are composite. Number theorists working with isolated primes or arithmetic functions in the Recognition Science setting would cite this concrete instance. The proof is a direct computational verification performed by the native_decide tactic.
Claim. $89$ is prime, $87$ is composite, and $91$ is 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. Prime is the transparent alias for the standard primality predicate on natural numbers. This theorem records a specific isolated-prime fact inside the primes component of the Recognition Science number-theory layer.
proof idea
The proof is a one-line wrapper that applies native_decide to decide the conjunction by direct computation of the primality status of 89, 87, and 91.
why it matters
The result supplies an explicit isolated-prime datum for arithmetic-function calculations in the primes module. It supports later development of Möbius inversion and squarefree properties without introducing new hypotheses. No downstream theorems currently reference it, leaving its role as a base fact for potential use in prime-gap or isolation arguments within the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.