cousin_prime_thirteen_seventeen
plain-language theorem explainer
The integers 13 and 17 form a cousin prime pair, satisfying primality for each and a difference of exactly 4. Number theorists working with explicit small cases of prime constellations or arithmetic functions would cite this instance. The verification applies a direct computational decision procedure that evaluates the finite predicates in a single step.
Claim. $13$ and $17$ are both prime numbers satisfying $17 = 13 + 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is defined locally as the transparent alias for the standard predicate on natural numbers. The upstream result from CirclePhaseLift supplies an explicit log-derivative bound used in related analytic estimates, while the Basic.Prime abbreviation ensures direct access to Nat.Prime without additional hypotheses.
proof idea
One-line wrapper that applies native_decide to the conjunction of the two primality statements and the arithmetic equality.
why it matters
The declaration supplies an explicit small-case fact inside the arithmetic functions module. It populates concrete prime data that can feed later constructions involving arithmetic functions on primes, even though no downstream uses are recorded yet. It aligns with the number-theoretic scaffolding required before deeper Dirichlet inversion or Recognition Science applications of discrete structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.