twin_prime_five_seven
plain-language theorem explainer
The declaration asserts that 5 and 7 form a twin prime pair with difference exactly 2. Number theorists checking elementary cases or building small-scale verifications in Recognition Science would reference it. The proof reduces to a single native decision procedure that directly confirms the primality predicates and arithmetic relation.
Claim. $5$ and $7$ are both prime with $7 = 5 + 2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for Nat.Prime. This theorem appears among basic prime checks in the NumberTheory.Primes section of the file.
proof idea
The proof is a one-line term that invokes native_decide to resolve the conjunction of the two primality statements and the equality.
why it matters
This elementary verification anchors the arithmetic primitives required for later Möbius-based constructions in the module. It fills a basic fact in the NumberTheory layer without recorded downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.