safe_prime_five
plain-language theorem explainer
The integer 5 qualifies as a safe prime since both 5 and 2 are prime. Number theorists working on small-prime classifications or arithmetic-function examples would reference this fact. The verification proceeds by direct computational decision on the primality conjunction.
Claim. $5$ is a safe prime: both $5$ and $(5-1)/2 = 2$ are prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related square-free predicates. Prime is the transparent alias for the standard natural-number primality predicate. This specific fact sits among sibling results on Möbius inversion and big-Omega functions but stands as an isolated primality check.
proof idea
The proof is a one-line wrapper that applies native decision to confirm the conjunction of the two primality statements.
why it matters
The result supplies a concrete base case for prime-related arithmetic inside the Recognition Science number-theory layer. It feeds no downstream theorems in the current graph and touches no forcing-chain steps or physical constants directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.