isolated_prime_onehundredthirteen
plain-language theorem explainer
113 is prime while 111 and 115 are composite. Number theorists examining small isolated primes or explicit gap examples would cite the fact for concrete verification. The proof is a one-line native_decide computation that directly evaluates the three primality predicates.
Claim. $113$ is prime while $111=3×37$ and $115=5×23$ are both composite.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the local transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream results include the basic Prime abbreviation together with structural is predicates from foundation and game-theory modules that support direct computational checks.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction Prime 113 ∧ ¬Prime 111 ∧ ¬Prime 115.
why it matters
The declaration supplies an explicit isolated-prime datum inside the arithmetic-functions file. It has no downstream uses and sits beside Möbius lemmas without feeding any parent theorem. It contributes concrete small-prime checks that can anchor arithmetic-function calculations in the Recognition Science number-theory layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.