isolated_prime_onehundredfiftyseven
plain-language theorem explainer
157 is an isolated prime: it is prime while 155 and 159 are both composite. Number theorists checking explicit small cases inside the Recognition Science primes scaffolding would cite this result for verification. The proof is a one-line native_decide computation that directly tests primality of the three integers.
Claim. $157$ is prime while neither $155$ nor $159$ is prime, 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. Statements remain minimal until deeper Dirichlet inversion is added. The local Prime predicate is a transparent alias for the standard Nat.Prime definition on natural numbers.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the conjunction of primality and non-primality assertions by direct computation.
why it matters
This supplies a concrete verified instance of an isolated prime inside the NumberTheory.Primes section. It supports the arithmetic scaffolding but feeds no downstream theorems yet. It aligns with the framework's pattern of explicit small-case checks before general results on the phi-ladder or J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.