sexy_prime_twentythree_twentynine
plain-language theorem explainer
23 and 29 form a sexy prime pair: both satisfy the primality predicate and differ by six. Number theorists enumerating small prime constellations or testing arithmetic functions on explicit primes would cite this instance. The proof reduces the entire conjunction to a single native_decide call that evaluates it by direct computation.
Claim. $23$ and $29$ are both prime and satisfy $29 = 23 + 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate Prime is a transparent alias for the standard Nat.Prime test on natural numbers. The conjunction connective is supplied by the circle-phase-lift module, which elsewhere records explicit log-derivative bounds.
proof idea
The proof is a one-line term-mode wrapper that applies native_decide to the decidable proposition Prime 23 ∧ Prime 29 ∧ 29 = 23 + 6.
why it matters
The declaration supplies an explicit sexy-prime datum inside the arithmetic-functions module. It can serve as a test case for Möbius-function evaluations on square-free integers whose prime factors lie in small constellations. It does not connect directly to the T0–T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.