chen_prime_eleven
plain-language theorem explainer
The declaration asserts that both 11 and 13 are prime numbers, supplying a concrete Chen prime instance for 11 where the twin 13 is also prime. Number theorists working on arithmetic functions or prime distributions in the Recognition Science framework would cite it as a verified base case. The proof is a direct one-line native_decide computation that evaluates the primality predicates without further lemmas.
Claim. Both $11$ and $13$ are prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and its basic properties on squarefree integers. The local theoretical setting keeps statements minimal so that Dirichlet inversion and deeper algebra can be added once the interfaces stabilize. The predicate Prime is a transparent alias for Nat.Prime, imported from the sibling Basic module.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the conjunction of primality statements for 11 and 13.
why it matters
The result supplies a verified small-prime fact inside the arithmetic-functions module, supporting later Möbius applications on primes. It fills a concrete RS-relevant Chen prime instance noted in the declaration comment, though it does not yet feed any downstream theorem. No direct tie to the forcing chain or phi-ladder appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.