sexy_prime_seventeen_twentythree
plain-language theorem explainer
The declaration asserts that 17 and 23 are both prime and differ by exactly 6. Number theorists examining explicit prime constellations would cite this concrete verified pair. The proof reduces to a single native decision procedure that evaluates primality and the arithmetic relation directly.
Claim. Both 17 and 23 are prime numbers and satisfy $23 = 17 + 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The Prime predicate is an alias for the standard natural-number primality predicate. This explicit pair result sits in the same file but does not invoke Möbius or inversion tools. The upstream conjunction lemma from CirclePhaseLift supplies an explicit log-derivative bound M that structures the logical and, while the Prime alias imports the Mathlib definition verbatim.
proof idea
The proof is a one-line term that applies native_decide to confirm the conjunction of the two primality statements and the equality.
why it matters
The result supplies a verified instance of a sexy-prime pair inside the number-theory layer of the Recognition framework. It shares the module with Möbius footholds yet carries no downstream uses. No direct tie to the T0-T8 forcing chain or phi-ladder appears; the declaration may serve as a basic building block for later prime-distribution claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.