cousin_prime_fortythree_fortyseven
plain-language theorem explainer
43 and 47 form a cousin prime pair: both are prime and differ by exactly 4. Number theorists checking explicit small-gap constellations or verifying base cases for prime-pair conjectures would cite this instance. The proof is a one-line wrapper that applies native_decide to settle primality and the arithmetic equality by direct computation.
Claim. $43$ and $47$ are prime numbers satisfying $47 = 43 + 4$.
background
The predicate Prime is a transparent alias for the standard definition of primality on natural numbers. This theorem sits inside a module that supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ, while keeping statements minimal until deeper Dirichlet algebra is added. The upstream Prime abbrev ensures direct compatibility with number-theoretic claims; the logical conjunction handling is supplied by the and result from the CirclePhaseLift module.
proof idea
The proof is a one-line wrapper that invokes native_decide to confirm both primality assertions and the difference equality by direct evaluation.
why it matters
The declaration supplies an explicit, machine-verified cousin-prime instance inside the arithmetic-functions module. It contributes to the NumberTheory.Primes infrastructure that later supports Möbius-based arguments, though it carries no downstream uses and does not invoke the forcing chain, phi-ladder, or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.