twin_prime_twohundredsixtynine_twohundredseventyone
plain-language theorem explainer
269 and 271 form a twin prime pair, with both satisfying the primality predicate and differing by exactly two. Number theorists working on small prime constellations or arithmetic function examples in the Recognition framework would cite this explicit instance. The proof executes as a term-mode native_decide that directly evaluates the conjunction of primality checks and the difference equation.
Claim. $269$ and $271$ are both prime numbers satisfying $271 = 269 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for the standard Nat.Prime predicate on natural numbers. The declaration sits inside this arithmetic-functions setting and applies the Prime definition to the concrete pair 269 and 271.
proof idea
The proof is a one-line term wrapper that invokes native_decide to resolve the conjunction of the two primality statements and the equality 271 = 269 + 2 by direct computation.
why it matters
The result supplies a verified twin-prime checkpoint inside the NumberTheory.Primes submodule that supports the arithmetic-function layer. It contributes concrete numerical content to the foundational number-theory scaffolding used in Recognition Science constructions such as the phi-ladder and forcing-chain steps, even though the dependency graph records no immediate downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.