isolated_prime_onehundredtwentyseven
plain-language theorem explainer
127 is an isolated prime because 125 factors as 5 cubed and 129 as 3 times 43, both composite. Number theorists checking specific prime gaps or constellations would cite this explicit verification. The proof reduces to a single native decision tactic that evaluates the primality predicates for each integer directly.
Claim. $127$ is prime while $125$ and $129$ are not: $Prime(127) ∧ ¬Prime(125) ∧ ¬Prime(129)$, where $Prime(n)$ asserts that $n$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the local alias for the standard natural-number primality predicate. The upstream Prime abbreviation from the Basic sibling module simply reexports Nat.Prime without added structure.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the boolean conjunction of the three primality predicates.
why it matters
This supplies a concrete numerical instance of an isolated prime that can anchor empirical checks. It has no recorded downstream uses. The statement sits in the arithmetic-functions file but does not invoke the Möbius machinery or connect to the forcing chain landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.