safe_prime_fiftynine
plain-language theorem explainer
The theorem asserts that 59 is a safe prime, with both 59 and 29 prime. Number theorists or cryptographers working with small safe primes for examples in arithmetic progressions or protocol tests would cite the fact. The proof is a direct computational verification via native_decide.
Claim. $59$ is a safe prime: $59$ is prime and $(59-1)/2 = 29$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and related prime predicates. The Prime predicate is a transparent alias for Nat.Prime. This declaration appears among specific prime facts in the NumberTheory.Primes section, independent of the Möbius definitions that dominate the file. Upstream imports include foundation-level 'is' structures and the basic Prime alias, though the primality check itself does not invoke them.
proof idea
The proof is a one-line term that applies native_decide to evaluate the conjunction of primality predicates directly.
why it matters
The result supplies a concrete numerical instance of a safe prime inside the arithmetic functions module. It grounds later number-theoretic constructions even though no downstream usage is recorded. The declaration fits the framework's pattern of embedding specific small-integer facts to support abstract arithmetic properties without touching the forcing chain or RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.