sophie_germain_three
plain-language theorem explainer
3 is established as a Sophie Germain prime because both 3 and 7 are prime. Number theorists working with arithmetic functions or small prime cases in the Recognition Science framework would cite the fact when handling explicit instances. The proof reduces to a single native_decide tactic that evaluates the two primality statements directly.
Claim. $3$ is a Sophie Germain prime, i.e., both $3$ and $7$ are prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related inversion tools. Prime is the transparent alias for the standard natural-number primality predicate. This supplies a concrete Sophie Germain instance for use alongside those functions.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction of the two primality statements.
why it matters
The declaration supplies a verified small-case fact inside the primes submodule that supports arithmetic-function statements. It anchors explicit prime pairs used in Möbius calculations and squarefree checks within the Recognition Science number-theory layer. No downstream uses are recorded and no open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.