prime_triplet_thirteen_seventeen_nineteen
plain-language theorem explainer
The declaration asserts that 13, 17, and 19 are each prime numbers, forming a triplet with successive gaps of 4 and 2. Number theorists studying small-gap prime constellations would reference this concrete case as an explicit example. The proof reduces to a direct computational check via native decision procedures.
Claim. The integers $13$, $17$, and $19$ are prime numbers.
background
The module supplies lightweight wrappers for arithmetic functions, beginning with the Möbius function μ. The Prime predicate is the repo-local alias for the standard Nat.Prime predicate on natural numbers. Upstream results include the gap definition as the product of closure and Fibonacci factors (claimed to equal 45) and the logarithmic anchor residue form F(Z) = ln(1 + Z/φ)/ln(φ).
proof idea
The proof is a one-line term that invokes native_decide to evaluate the conjunction of the three primality statements.
why it matters
This supplies a specific prime triplet instance with gaps (4, 2), placed inside the arithmetic functions module whose doc-comment emphasizes Möbius footholds for later Dirichlet extensions. It feeds no downstream theorems. The result touches the framework's interest in small gaps but remains isolated from the T0-T8 forcing chain and the gap=45 derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.