sophie_germain_eleven
plain-language theorem explainer
Eleven qualifies as a Sophie Germain prime because both it and twenty-three are prime. Number theorists working with arithmetic functions or prime pairs in the Recognition Science setting would cite this concrete instance. The proof reduces to a single native_decide call that evaluates the primality predicates by direct computation.
Claim. Both $11$ and $23$ are prime numbers.
background
The module wraps Mathlib arithmetic functions and begins with the Möbius function, keeping statements lightweight before deeper Dirichlet algebra. The Prime abbreviation is the transparent alias for the standard Nat.Prime predicate on natural numbers. Upstream results supply basic primality definitions from the Primes.Basic module along with structural lemmas from foundation and number-theory imports, though this declaration depends only on decidability of the predicates.
proof idea
The proof is a one-line wrapper that applies native_decide to resolve the conjunction of the two primality statements by direct evaluation.
why it matters
The declaration supplies a concrete Sophie Germain prime pair for use in prime-related constructions within the arithmetic-functions scaffolding. It fills a small number-theoretic foothold in the module but does not invoke the forcing chain, RCL, or phi-ladder. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.