twin_prime_fourhundredsixtyone_fourhundredsixtythree
plain-language theorem explainer
The declaration establishes that 461 and 463 form a twin prime pair differing by 2. Researchers cataloging explicit small primes for arithmetic function calculations or numerical checks in number theory would cite this result. The proof reduces to a single native_decide tactic that resolves the primality predicates and additive relation by direct computation.
Claim. $461$ and $463$ are both prime numbers satisfying $463 = 461 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. This theorem appears among explicit prime verifications that support those wrappers. It rests on the upstream definition of the set of primes as the subset of natural numbers satisfying the primality predicate, together with the transparent local alias for that predicate.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the conjunction of the two primality statements and the equality.
why it matters
This supplies a concrete twin prime pair for use in arithmetic function work within the Recognition framework. It populates the NumberTheory.Primes section that underpins Möbius applications and related Dirichlet constructions. No downstream theorems are listed, so the result functions as a numerical anchor rather than a lemma in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.