prime_quadruplet_five
plain-language theorem explainer
The statement confirms that the integers 5, 7, 11, and 13 are all prime and form a quadruplet with successive gaps of 2, 4, and 2. Number theorists examining small prime constellations would reference this as an explicit verified instance. The proof reduces to a single native decision procedure that evaluates the primality predicates directly in the computational model.
Claim. The integers 5, 7, 11, and 13 each belong to the set of prime numbers, forming a quadruplet $(5,7,11,13)$ with successive differences 2, 4, 2.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Prime is the local transparent alias for the standard predicate that a natural number is prime. This theorem appears among basic number-theoretic facts that anchor later arithmetic constructions in the file.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the conjunction of the four primality statements.
why it matters
This supplies a concrete prime quadruplet instance inside the arithmetic functions module that prepares Möbius footholds. It fills a basic verification step in the number theory layer of the Recognition framework, though it carries no recorded downstream uses. The module documentation positions such facts as starting points for Dirichlet algebra once interfaces stabilize.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.