sexy_prime_five_eleven
plain-language theorem explainer
The declaration asserts that 5 and 11 are both prime numbers differing by 6. Number theorists studying small prime constellations would cite this explicit case. The verification proceeds by a direct native decision procedure that evaluates the primality predicates and the arithmetic equality in one step.
Claim. The integers $5$ and $11$ are both prime and satisfy $11 = 5 + 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is a transparent alias for the standard natural-number primality predicate. This theorem appears as a basic example in the primes section, separate from the log-derivative bounds developed upstream in the circle phase lift module.
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 equality by direct computation.
why it matters
This supplies a concrete instance of a prime pair differing by 6 within the number theory layer. It feeds no downstream results. The broader Recognition framework derives physics from J-uniqueness, the phi fixed point, and the eight-tick octave, but this theorem remains a peripheral arithmetic example without linkage to the T0-T8 chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.