twin_prime_threehundredeleven_threehundredthirteen
plain-language theorem explainer
The statement establishes that 311 and 313 form a twin prime pair. Researchers cataloging explicit small twin primes or verifying concrete instances for arithmetic-progression studies would cite this result. Its verification relies on a single native_decide invocation that checks the primality conditions and difference directly.
Claim. $311$ and $313$ are both prime numbers with $313 = 311 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and squarefreeness predicates. The local setting keeps statements minimal before layering Dirichlet algebra. The Prime predicate is the repository-local transparent alias for the standard natural-number primality predicate.
proof idea
The proof is a one-line wrapper that invokes native_decide to confirm the three conjuncts simultaneously.
why it matters
This instance populates the library of concrete prime-pair examples inside the NumberTheory component. It supports any downstream construction that needs explicit small primes, though no immediate parent theorem consumes it. In the Recognition Science framework it contributes to the arithmetic foundations that interface with the phi-ladder and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.