superprime_twohundredeleven
plain-language theorem explainer
211 and 47 are both prime. This primality fact is recorded in the arithmetic functions module to anchor isolated-prime examples within Recognition Science number theory. The proof is a one-line term that applies native_decide to evaluate the conjunction directly.
Claim. $211$ and $47$ are both prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is a transparent alias for Nat.Prime. The theorem appears in a section on isolated primes (p-2 and p+2 both composite). Upstream dependencies include the Prime definition from Basic and several structure or theorem markers labeled is from foundation, simplicial ledger, game theory, Ramanujan bridge, and circle phase lift modules.
proof idea
The proof is a term-mode one-liner that invokes native_decide on the conjunction Prime 211 ∧ Prime 47.
why it matters
The declaration supplies a concrete primality fact inside the NumberTheory.Primes.ArithmeticFunctions layer. It supports classification of isolated primes but has no recorded downstream uses. It does not invoke the Recognition Composition Law, the phi-ladder, or the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.