sexy_prime_thirteen_nineteen
plain-language theorem explainer
The theorem asserts that 13 and 19 are both prime and differ by 6, forming a sexy prime pair. Number theorists cataloging small prime constellations would cite this as a verified base case. The proof is a one-line native_decide computation that directly evaluates the primality predicates and the difference equality.
Claim. $13$ and $19$ are both prime and satisfy $19 = 13 + 6$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function for later Dirichlet inversion work. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers. The upstream and combinator from CirclePhaseLift encodes an explicit log-derivative bound on the circle, while the local Prime definition supplies the predicate used in the conjunction.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the conjunction of the two primality statements and the arithmetic equality.
why it matters
The result supplies a concrete verified instance of a prime pair differing by 6 inside the NumberTheory layer. It supports accumulation of explicit small facts that can feed arithmetic-function identities or prime-distribution statements downstream, consistent with the framework's pattern of pinning constants and small cases before scaling to T5-T8 forcing steps. No parent theorems or open questions are recorded for this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.