prime_triplet_eleven_thirteen_seventeen
plain-language theorem explainer
The integers 11, 13, and 17 form a prime triplet with successive gaps of 2 and 4. Number theorists cataloging small prime constellations or gap patterns inside the Recognition Science scaffolding would reference this fact. The proof is a direct one-line invocation of native_decide that computes the primality predicates.
Claim. $11$, $13$, and $17$ are prime numbers that form a triplet with successive gaps of $2$ and $4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting keeps statements minimal until Dirichlet algebra layers are added. Upstream, the Prime abbreviation is the transparent alias for Nat.Prime, while the gap definitions from Gap45.Derivation and the RSBridge.Anchor modules express gap as a product of closure and Fibonacci factors or as the closed-form residue ln(1 + Z/φ)/ln(φ).
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the three primality statements.
why it matters
This supplies a concrete small-gap prime triplet inside the NumberTheory.Primes hierarchy. It draws on the gap machinery from Gap45.Derivation (whose main theorem asserts gap equals 45) and the anchor-scale residue functions, yet currently has no downstream citations. It touches the framework's interest in prime patterns that may later interface with the eight-tick octave or phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.