safe_prime_fortyseven
plain-language theorem explainer
The statement verifies that 47 is a safe prime by confirming both 47 and 23 are prime. Number theorists compiling explicit lists of safe primes for applications in cryptography or arithmetic progressions would reference this check. The proof applies native_decide to evaluate the primality predicates directly in the kernel.
Claim. $47$ is prime and $(47-1)/2 = 23$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream results supply structural definitions from foundation modules that maintain collision-free and algebraic consistency across the Recognition Science codebase.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the two primality statements.
why it matters
This explicit verification of a small safe prime supports number-theoretic scaffolding used in Recognition Science mass formulas and phi-ladder calculations. It feeds no immediate parent theorems in the current dependency graph. The declaration aligns with the framework's T0-T8 forcing chain emphasis on concrete small-integer checks before scaling to constants such as alpha inverse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.