twin_prime_onehundredninetyone_onehundredninetythree
plain-language theorem explainer
The theorem asserts that 191 and 193 are both prime with difference exactly 2. Number theorists checking small twin-prime instances or concrete arithmetic facts would reference this verified pair. The proof reduces to a single native_decide tactic that evaluates the primality predicates and equality by direct computation.
Claim. $191$ and $193$ are both prime and satisfy $193 = 191 + 2$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function. This declaration sits in the primes subsection and uses the local alias Prime, defined as an abbreviation for the standard Nat.Prime predicate on natural numbers. Upstream results supply the Prime alias together with structural hypotheses from foundation modules that maintain algebraic consistency across the repository.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to resolve the conjunction of the two primality statements and the arithmetic equality through direct computational evaluation.
why it matters
This concrete twin-prime verification supports the arithmetic functions infrastructure in the NumberTheory layer. It supplies a basic verified fact without feeding into any downstream theorems, consistent with the module's stated goal of keeping statements lightweight until deeper Dirichlet tools stabilize. No direct tie to the forcing chain or phi-ladder is present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.