isolated_prime_ninetyseven
plain-language theorem explainer
97 is established as an isolated prime because it is prime while both immediate distance-2 neighbors are composite. Number theorists cataloging prime gaps or preparing arithmetic-function inputs in the Recognition Science setting would reference the fact. The proof is a single native_decide term that evaluates the primality predicates directly.
Claim. $97$ is prime while $95 = 5×19$ and $99 = 3^2×11$ are both composite.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The predicate Prime is the transparent alias for Nat.Prime. Upstream 'is' declarations from OptionAEmpiricalProgram, SimplicialLedger, MechanismDesignFromSigma and MockThetaPhantom supply collision-free or tautological interfaces that the broader framework treats as discharged hypotheses.
proof idea
The proof is a one-line term that applies the native_decide tactic to the conjunction Prime 97 ∧ ¬Prime 95 ∧ ¬Prime 99.
why it matters
The declaration supplies an explicit isolated-prime datum inside the NumberTheory.Primes.ArithmeticFunctions module. It can serve as a concrete input for later Möbius or big-Omega calculations once Dirichlet inversion is layered on, consistent with the module's stated plan to stabilize basic interfaces before deeper algebra. No downstream use is recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.