twin_prime_seventeen_nineteen
plain-language theorem explainer
17 and 19 form a twin prime pair. Number theorists verifying small cases or populating arithmetic function libraries cite this fact. The proof is a one-line wrapper that applies native_decide to confirm both primality predicates and the exact difference of 2.
Claim. $17$ and $19$ are both prime numbers satisfying $19 = 17 + 2$.
background
The declaration appears in the ArithmeticFunctions module, whose module documentation describes lightweight wrappers around Mathlib arithmetic functions beginning with the Möbius function μ. The local theoretical setting keeps statements minimal so that deeper Dirichlet inversion can be added once the basic interfaces stabilize. The Prime predicate is the transparent alias for Nat.Prime supplied by the imported Basic submodule.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction of the two primality statements and the equality 19 = 17 + 2.
why it matters
This supplies a concrete verified twin-prime instance inside the number-theory scaffolding that supports Recognition Science arithmetic functions. No downstream theorems are listed as users, so the result functions as a basic building block rather than a direct feeder into the forcing chain or phi-ladder. It aligns with the module's goal of stabilizing small interfaces before layering on inversion formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.