twin_prime_onehundredseven_onehundrednine
plain-language theorem explainer
107 and 109 form a twin prime pair differing by exactly two. Number theorists referencing concrete examples of small twin primes in formal arithmetic settings would cite this instance. The proof is a term-mode native_decide invocation that directly evaluates the primality predicates and the difference equality.
Claim. $107$ and $109$ are both prime numbers and satisfy $109 = 107 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for later Dirichlet work. Prime is a transparent local alias for the standard Nat.Prime predicate on natural numbers. This declaration records a specific twin prime pair as a basic fact inside the primes section of the arithmetic functions file.
proof idea
The proof is a one-line term wrapper that applies native_decide to confirm both primality statements and the exact difference of two.
why it matters
This supplies a machine-verified twin prime pair inside the NumberTheory.Primes.ArithmeticFunctions module. With zero listed downstream uses it functions as a concrete reference example rather than a lemma feeding larger results. It touches on specific numerical checks that may support empirical aspects of the Recognition Science program, though no direct tie to the forcing chain or phi-ladder appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.