prime_triplet_seven_eleven_thirteen
plain-language theorem explainer
The declaration establishes that 7, 11, and 13 are each prime numbers, forming a triplet with successive gaps of 4 and 2. Number theorists cataloging small prime constellations would reference this concrete instance. The proof reduces to a direct computational check via native_decide.
Claim. $7$, $11$, and $13$ are prime numbers.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ. This theorem sits in the primes subsection and records a specific triplet whose gaps are (4, 2). Upstream results define gap as the product of closure and Fibonacci factors, and supply the display function F(Z) = ln(1 + Z/φ)/ln(φ) that closes the integrated RG residue at the anchor scale.
proof idea
The proof is a one-line wrapper that applies native_decide to verify the three primality statements simultaneously.
why it matters
This supplies a concrete numerical fact inside the NumberTheory.Primes section. It aligns with the framework's use of explicit small-gap instances that can feed gap calculations, as seen in the gap definitions from Gap45.Derivation and the anchor display function in RSBridge.Anchor. No downstream theorems are recorded, so its precise role in larger prime-gap or mass-ladder arguments remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.