cousin_prime_seven_eleven
plain-language theorem explainer
7 and 11 form a cousin prime pair differing by 4, recorded as a verified fact inside the arithmetic functions module. Researchers enumerating small prime constellations differing by 4 would cite this instance as a base case. The proof succeeds by a single native_decide tactic that evaluates the primality predicates and equality directly.
Claim. The integers 7 and 11 are both prime and satisfy $11 = 7 + 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The Prime predicate is the transparent alias for the standard Nat.Prime notion of primality in the naturals. This statement appears among basic prime facts and does not invoke the Möbius machinery or the log-derivative bound supplied by the upstream and theorem.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the two primality checks and the arithmetic equality.
why it matters
It supplies a concrete small-case instance of cousin primes inside the primes infrastructure, though it currently feeds no downstream results. The surrounding module context centers on arithmetic functions such as Möbius, so the declaration provides basic prime data that could support later constellation or inversion arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.