twin_prime_fiftynine_sixtyone
plain-language theorem explainer
59 and 61 form a twin prime pair because both satisfy the primality predicate and differ by exactly 2. Number theorists checking small explicit cases or building verified lists of prime constellations would reference this result. The proof is a one-line term that applies native_decide to evaluate the conjunction of the two primality statements and the arithmetic equality at the concrete integers.
Claim. $59$ and $61$ are both prime numbers and satisfy $61 = 59 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, while keeping statements minimal until Dirichlet algebra layers are added. Prime is the transparent alias for Nat.Prime, so the declaration simply asserts the standard primality predicate on 59 and 61 together with the difference condition. The upstream CirclePhaseLift.and result supplies an explicit log-derivative bound on a disk, while the Basic.Prime abbrev ensures direct compatibility with Mathlib's Nat.Prime predicate.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the conjunction of the two primality checks and the equality 61 = 59 + 2 at the concrete values.
why it matters
The declaration supplies a concrete verified twin-prime instance inside the arithmetic-functions module. No downstream theorems currently cite it, so it functions as a basic building block for later prime-pair developments. It sits among the explicit small-case verifications that support the broader number-theory scaffolding in the Recognition Science repository.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.