isolated_prime_onehundredthirtyone
plain-language theorem explainer
The declaration verifies that 131 is prime while both 129 and 133 are composite. Number theorists checking small prime gaps or isolation properties would reference this explicit fact. The proof reduces to a single native_decide call that evaluates the three primality assertions by direct computation.
Claim. $131$ is prime while $129$ and $133$ are both composite.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for Nat.Prime. This theorem appears among sibling arithmetic-function definitions but supplies a concrete primality datum rather than a general identity. Upstream, the Prime abbrev is imported from NumberTheory.Primes.Basic; several depends_on edges point to unrelated class and structure definitions whose 'is' fields serve as hypothesis placeholders.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of primality predicates.
why it matters
The result supplies an explicit isolated-prime datum inside the arithmetic-functions module. It has no downstream uses. It contributes a verified number-theoretic atom that can be referenced when the framework later connects arithmetic facts to the Recognition Science forcing chain or the phi-ladder, though no such link is present here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.