safe_prime_onehundredseven
plain-language theorem explainer
107 qualifies as a safe prime because both 107 and 53 are prime. Number theorists checking explicit safe-prime instances or building tables of Sophie Germain primes would cite this verification. The proof is a one-line native_decide term that computes the primality conjunction directly.
Claim. $107$ is prime and $(107-1)/2=53$ is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and keeping statements minimal until Dirichlet algebra stabilizes. Prime is the transparent repo-local alias for Nat.Prime. The theorem records an explicit safe-prime datum inside this arithmetic-functions scaffolding.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the two primality statements.
why it matters
The declaration supplies a concrete number-theoretic fact inside the arithmetic-functions module. It supports later use of prime data in Recognition Science constructions such as the phi-ladder and mass formulas, though no downstream theorems currently reference it. The eight-tick octave and D=3 landmarks presuppose reliable prime facts of this kind.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.