sexy_prime_seven_thirteen
plain-language theorem explainer
The theorem asserts that 7 and 13 are both prime and differ by 6. Number theorists checking explicit prime constellations or seeding arithmetic-function examples would reference this instance. Its proof is a one-line native_decide term that reduces the entire conjunction to a decidable computation over natural numbers.
Claim. $7$ and $13$ are prime numbers satisfying $13 = 7 + 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related maps such as bigOmega. This theorem supplies a verified prime-pair fact inside that setting. It rests on the transparent alias Prime n := Nat.Prime n from the Basic submodule and on a general conjunction result imported from CirclePhaseLift.
proof idea
The proof is a one-line term that applies native_decide to the conjunction of the two primality statements and the equality 13 = 7 + 6.
why it matters
The declaration supplies a concrete sexy-prime example inside the arithmetic-functions scaffolding. It feeds no immediate downstream theorems in the current graph, indicating it functions as a basic verified atom rather than a derived step. The surrounding module keeps statements lightweight pending deeper Dirichlet-algebra layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.