twin_prime_twohundredeightyone_twohundredeightythree
plain-language theorem explainer
281 and 283 form a twin prime pair, with both satisfying primality and differing by exactly 2. Number theorists cataloging explicit small-scale prime constellations or verifying concrete instances would cite this result. The proof executes as a direct term that invokes native_decide to resolve the conjunction through built-in computational evaluation.
Claim. The integers 281 and 283 are both prime and satisfy $283 = 281 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is a transparent local alias for the standard natural-number primality predicate. Upstream results include foundational structures such as collision-free classes and simplicial ledger constructions that embed number-theoretic facts into the broader Recognition framework.
proof idea
The proof is a one-line term that applies native_decide to the conjunction of the two primality statements and the additive equality, resolving everything through internal decision procedures.
why it matters
This explicit twin prime pair populates the arithmetic functions library and stands available for larger prime-related arguments in the Recognition Science framework. No immediate parent theorems appear in the dependency graph, yet the declaration aligns with the module's role in supplying Möbius footholds for potential Dirichlet algebra extensions. It contributes concrete number-theoretic data that could anchor arithmetic properties relevant to the phi-ladder or forcing chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.