twin_prime_onehundredseventynine_onehundredeightyone
plain-language theorem explainer
The declaration asserts that 179 and 181 form a twin prime pair, both prime and differing by exactly 2. Number theorists building explicit small-case verifications or checking arithmetic facts would cite this result. The proof is a direct computational evaluation via the native_decide tactic on the primality predicates and equality.
Claim. $179$ and $181$ are both prime numbers and satisfy $181 = 179 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and related maps such as bigOmega. Prime is the transparent repo-local alias for Nat.Prime on natural numbers. The local setting keeps statements minimal so that deeper Dirichlet inversion can be added once interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the conjunction of the two primality statements and the difference equality.
why it matters
This supplies an explicit, machine-verified twin prime pair inside the number-theory layer of the Recognition Science framework. It supports the basic prime infrastructure (Prime alias) used by sibling arithmetic-function definitions, though no downstream uses are recorded. It aligns with the framework's pattern of concrete computational checks before layering on J-cost or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.