mod6_eleven_prime
plain-language theorem explainer
11 is prime and 11 ≡ 5 mod 6. Number theorists working with Recognition Science arithmetic functions would cite this when verifying small primes for modular constraints in Möbius or squarefree contexts. The proof is a one-line native_decide term that directly evaluates the conjunction of primality and remainder.
Claim. $11$ is prime and $11 ≡ 5 (mod 6)$.
background
The module provides lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. Prime is the transparent alias for Nat.Prime. This theorem records a basic modular fact about the prime 11 that is flagged as RS-relevant for later use in prime-related arithmetic.
proof idea
The proof is a one-line term wrapper that applies native_decide to compute both the primality predicate and the modulo-6 remainder in a single evaluation step.
why it matters
The declaration supplies a concrete modular fact on a small prime inside the arithmetic-functions module. It supports the Recognition Science emphasis on primes congruent to 5 mod 6, as stated in the declaration comment, and sits ready for use in Möbius or squarefree lemmas even though no downstream citations are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.