twin_prime_twentynine_thirtyone
plain-language theorem explainer
29 and 31 form a twin prime pair, both prime with difference exactly 2. Number theorists checking explicit small cases or base instances for arithmetic-function calculations would reference the result. The proof is a one-line native_decide call that evaluates the primality predicates and equality directly.
Claim. $29$ and $31$ are both prime and satisfy $31 = 29 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is a transparent alias for Nat.Prime. This theorem records a concrete twin-prime instance inside the primes submodule rather than stating a general arithmetic identity. The upstream and theorem from CirclePhaseLift supplies an explicit log-derivative bound on a disk, while the Prime abbrev simply re-exports the standard primality predicate.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction of the two primality statements and the difference equation.
why it matters
The declaration supplies a verified small twin-prime pair inside the arithmetic-functions file. It feeds no downstream results in the module, which instead develops Möbius and bigOmega properties. Within the Recognition framework it functions as an explicit numerical check rather than a step in the T0-T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.