sophie_germain_five
plain-language theorem explainer
The declaration verifies that 5 is a Sophie Germain prime by confirming primality of both 5 and 11. Number theorists building enumerations of small prime pairs or safeprime sequences would cite this base case. The proof reduces to a single native_decide invocation that evaluates the primality predicates directly from the arithmetic library.
Claim. $5$ is a Sophie Germain prime, i.e., both $5$ and $2·5+1=11$ are prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent local alias for the standard Nat.Prime predicate. Upstream results supply the primality definition together with structural hypotheses from foundation modules that enforce collision-free or tautological properties in related contexts.
proof idea
The proof is a one-line term that invokes native_decide to resolve the conjunction of the two primality statements.
why it matters
This populates a base case for prime-pair constructions inside the number-theory layer that supports Möbius inversion. It sits downstream of the Prime alias and fills a small enumeration step without reference to the forcing chain, phi-ladder, or eight-tick octave. No downstream usage is recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.