cousin_prime_sixtyseven_seventyone
plain-language theorem explainer
67 and 71 form a verified pair of cousin primes, both prime and differing by 4. Number theorists citing concrete examples of prime constellations in the Recognition Science arithmetic functions module would reference this result. The proof is a one-line native decision that directly confirms the primality predicates and the exact difference.
Claim. $67$ and $71$ are both prime and satisfy $71 = 67 + 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard natural-number primality predicate. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the two primality statements and the arithmetic equality.
why it matters
This supplies an explicit, machine-checked instance of cousin primes inside the arithmetic functions module. It serves as a concrete foothold for later applications of Möbius or other arithmetic functions to prime pairs, consistent with the module's role as a base layer before deeper number-theoretic constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.