sexy_prime_thirtyone_thirtyseven
plain-language theorem explainer
31 and 37 form a sexy prime pair, both prime with difference exactly 6. Number theorists referencing explicit small-constellation facts inside the Recognition Science arithmetic-functions module would cite this verification. The proof is a one-line native_decide invocation that directly evaluates the primality predicates and the arithmetic equality against the natural-number library.
Claim. The integers 31 and 37 are both prime and satisfy the relation $37 = 31 + 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The local setting keeps statements minimal so that deeper Dirichlet inversion can be added once basic interfaces stabilize. The declaration depends on the transparent alias Prime n := Nat.Prime n together with a logical conjunction lemma from the circle-phase-lift development.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the two primality statements and the difference equation.
why it matters
The result supplies a concrete prime-pair datum inside the arithmetic-functions file. It supports any later use of Möbius or big-Omega functions on small primes but does not advance the forcing chain, the Recognition Composition Law, or the phi-ladder mass formula. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.