safe_prime_eleven
plain-language theorem explainer
The declaration confirms that 11 is a safe prime by verifying that both 11 and 5 are prime. Number theorists handling small primes inside Recognition Science arithmetic setups would reference this fact when building phi-ladder examples or mass formulas. The proof is a direct computational check via native decision that evaluates the primality conjunction without intermediate lemmas.
Claim. 11 is a safe prime, i.e., both $11$ and $(11-1)/2 = 5$ are prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added later once interfaces stabilize.
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
This supplies a concrete safe-prime instance inside the arithmetic-functions module. It feeds basic number-theoretic facts used in Recognition Science constructions such as the phi-ladder and T5 J-uniqueness, even though no downstream uses are recorded yet. It aligns with the framework's reliance on small primes for mass formulas and eight-tick octave steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.