isolated_prime_fortyseven
plain-language theorem explainer
47 is prime while 45 and 49 are both composite, establishing an isolated prime instance. Number theorists working on prime gaps within the Recognition Science arithmetic layer would cite this fact. The proof is a one-line term that invokes native_decide for direct evaluation of the three primality statements.
Claim. $47$ is prime while $45=3^2×5$ and $49=7^2$ are composite, with primality the standard predicate on natural numbers.
background
The module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for the standard primality predicate on natural numbers. The local setting keeps statements minimal before layering Dirichlet algebra or inversion. Upstream the Prime definition is imported directly as the library predicate.
proof idea
One-line term proof that applies native_decide to evaluate the conjunction of primality statements by direct computation.
why it matters
The declaration supplies a verified concrete instance of an isolated prime inside the arithmetic functions file. It populates basic number theory scaffolding that may support later phi-ladder constructions, though no downstream theorems reference it yet. It aligns with the need for explicit prime facts ahead of deeper Recognition Composition Law applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.