twin_prime_onehundredthirtyseven_onehundredthirtynine
plain-language theorem explainer
137 and 139 form a twin prime pair. Researchers working on Recognition Science constants would cite this fact for the placement of 137 inside the predicted interval for the inverse fine-structure constant. The proof is a direct computational verification that both numbers are prime and differ by two.
Claim. $137$ and $139$ are both prime and satisfy $139 = 137 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for later Dirichlet inversion. This theorem records a concrete twin-prime instance at the integer 137 flagged as RS-relevant. Upstream, Prime is the transparent alias for the standard predicate Nat.Prime on natural numbers; the remaining dependencies are foundational class and structure declarations that do not participate in the primality computation.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to reduce the conjunction to a decidable ground computation of primality for 137 and 139 together with the arithmetic equality.
why it matters
The declaration supplies a verified twin-prime instance at the integer 137 that lies inside the Recognition Science band for alpha inverse. It anchors specific numerical facts inside the arithmetic-functions module that can feed later constructions involving prime values. No parent theorem from the used-by list is recorded, and the fact touches the alpha-band landmark without engaging the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.