sexy_prime_thirtyseven_fortythree
plain-language theorem explainer
37 and 43 form a sexy prime pair: both are prime and differ by exactly 6. Number theorists examining prime constellations or explicit examples of pairs with gap 6 would reference this instance. The proof is a one-line term that applies native_decide to settle the primality checks and equality by direct computation.
Claim. $37$ and $43$ are both prime and satisfy $43 = 37 + 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem supplies a concrete numerical example inside that setting. Upstream structures include nuclear density tiers scaled by powers of phi, ledger factorizations of the positive reals under multiplication, and simplicial edge lengths derived from psi, though the primality statement itself is independent of those constructions.
proof idea
The proof is a one-line term that invokes native_decide to confirm both primality assertions and the arithmetic equality by direct computation.
why it matters
The declaration supplies a verified concrete instance of sexy primes inside the arithmetic-functions module. It anchors number-theoretic examples that can feed later constructions in the Recognition framework, such as those involving the phi-ladder or spectral emergence, even though no downstream uses are recorded. It aligns with the framework's pattern of grounding higher claims in explicit, decidable facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.