isolated_prime_seventynine
plain-language theorem explainer
79 is prime while 77 = 7 × 11 and 81 = 3^4 are composite. Number theorists checking explicit cases inside the Recognition Science arithmetic functions layer would cite this verification. The proof is a one-line native_decide evaluation of the primality predicates.
Claim. $79$ is prime, $77 = 7 × 11$ is composite, and $81 = 3^4$ is 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. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the three primality statements.
why it matters
This supplies a concrete isolated-prime check inside the arithmetic-functions file. It has no listed downstream uses and does not feed any parent theorem in the supplied graph. The result remains a leaf verification with no direct tie to the forcing chain or RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.