cousin_prime_nineteen_twentythree
plain-language theorem explainer
19 and 23 form a cousin prime pair, both prime and separated by exactly 4. Number theorists referencing concrete prime-pair instances inside the Recognition Science arithmetic-functions module would cite this verification. The proof is a one-line wrapper that invokes native_decide to evaluate the primality predicates and the arithmetic equality.
Claim. $19$ and $23$ are prime numbers satisfying $23 = 19 + 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. This theorem records a basic fact about specific primes in the same file that hosts Möbius-related definitions and squarefree checks.
proof idea
The proof is a one-line wrapper that applies native_decide, which directly evaluates the conjunction of the two Prime statements (via the Nat.Prime alias) and the equality 23 = 19 + 4.
why it matters
The declaration supplies a verified cousin-prime instance inside NumberTheory.Primes.ArithmeticFunctions. It sits among Möbius footholds and squarefree lemmas, providing a concrete base case even though no downstream uses are recorded. It aligns with the framework's pattern of grounding number-theoretic claims before layering Dirichlet algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.