cousin_prime_three_seven
plain-language theorem explainer
The theorem asserts that 3 and 7 form a cousin prime pair differing by 4. Number theorists building arithmetic function libraries or prime constellation examples in the Recognition Science setting would cite this verified instance. Its proof is a direct native_decide computation that checks both primality conditions and the exact difference without intermediate lemmas.
Claim. $3$ and $7$ are both prime and satisfy $7 = 3 + 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and its basic properties such as vanishing on non-squarefree inputs. The local setting keeps statements minimal to allow later layering of Dirichlet inversion once the interfaces stabilize. The declaration depends on the transparent alias for the standard primality predicate and on a general conjunction operation imported from the CirclePhaseLift module.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the full conjunction of the two primality statements and the arithmetic equality.
why it matters
This supplies a concrete small-instance fact for prime pairs inside the arithmetic functions module. It supports downstream work on Möbius-based counting or inversion formulas that may later reference specific prime constellations. No parent theorems are listed among the used-by edges, and the declaration touches no open scaffolding questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.