sexy_prime_eleven_seventeen
plain-language theorem explainer
11 and 17 are verified as sexy primes, with both satisfying the primality condition and differing by 6. Number theorists examining fixed-gap prime pairs would cite this as an explicit example. The verification uses direct computation through native decision procedures.
Claim. The numbers 11 and 17 are both prime and satisfy the equation $17 = 11 + 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for the standard Nat.Prime predicate. The upstream and theorem from CirclePhaseLift supplies an explicit log-derivative bound M that yields an angular Lipschitz constant on the circle, while the Prime abbrev ensures direct compatibility with Mathlib primality checks.
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 arithmetic equality.
why it matters
This supplies a concrete verified instance of a sexy-prime pair inside the arithmetic-functions module. No downstream theorems are listed among the used_by edges. It fills a basic number-theoretic foothold without invoking Recognition Science landmarks such as the J-uniqueness forcing step, the phi fixed point, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.