twin_prime_eleven_thirteen
plain-language theorem explainer
Eleven and thirteen form a twin prime pair with difference exactly two. Number theorists checking small explicit cases or seeding arithmetic function examples would reference this instance. The proof reduces to a single native decision procedure that evaluates the primality predicates and the equality directly.
Claim. $11$ and $13$ are both prime with $13 = 11 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is a transparent alias for the standard predicate Nat.Prime on natural numbers. The local setting keeps statements minimal so that Dirichlet algebra and inversion can be added once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the conjunction of the two primality statements and the difference equality at compile time.
why it matters
This explicit twin-prime fact anchors the primes section of the arithmetic-functions module. It supplies a concrete base case that can feed constructions involving Möbius inversion over small prime sets. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.