twin_prime_fourhundrednineteen_fourhundredtwentyone
plain-language theorem explainer
419 and 421 form a twin prime pair differing by exactly two. Number theorists referencing concrete prime constellations within the Recognition Science arithmetic functions module would cite this instance. The proof is a one-line term application of native_decide that directly resolves the primality conjunction and difference equation.
Claim. $419$ and $421$ are both prime numbers with $421 = 419 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Local conventions treat statements as footholds for later Dirichlet inversion without heavy algebraic machinery. The upstream Prime predicate is the transparent alias for Nat.Prime.
proof idea
The proof is a one-line term wrapper that applies native_decide to discharge the conjunction of the two primality statements and the additive relation.
why it matters
This supplies a verified concrete twin-prime datum inside the arithmetic-functions module. It does not feed any downstream results and sits outside the main forcing chain, RCL, or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.