prime_triplet_five_seven_eleven
plain-language theorem explainer
The statement asserts that 5, 7, and 11 are prime numbers. Number theorists examining small prime triplets with gaps of 2 and 4 might reference this verified instance. The proof reduces to a single native decision procedure that checks the primality predicates directly.
Claim. The integers 5, 7, and 11 are all prime.
background
This module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function. The local theoretical setting keeps statements basic before layering Dirichlet algebra. Upstream results include the definition of the gap as the product of closure and Fibonacci factors, the display function F(Z) = ln(1 + Z/φ)/ln(φ) for anchor residues, and the alias for Nat.Prime.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the conjunction of primality predicates.
why it matters
This declaration verifies a specific prime triplet with consecutive gaps of 2 and 4. It appears in the arithmetic functions module focused on Möbius footholds but records no parent theorems or downstream citations. The result stands as an isolated fact check within the primes section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.