prime_triplet_seventeen_nineteen_twentythree
plain-language theorem explainer
17, 19 and 23 form a prime triplet with successive gaps of 2 and 4. Researchers handling arithmetic functions or small-integer constellations in Recognition Science cite this for verified base cases in Möbius or squarefree contexts. The proof is a one-line term that invokes native_decide to settle the three primality checks by direct computation.
Claim. $17$, $19$, and $23$ are all prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting is therefore the interface between primality predicates and arithmetic operations such as squarefree checks. The declaration depends on the Prime predicate imported from the Basic submodule, which supplies the standard definition of primality used throughout the file.
proof idea
The proof is a term-mode one-liner that applies the native_decide tactic. This tactic reduces the conjunction of three primality statements to a decidable computation that confirms each of 17, 19 and 23 is prime.
why it matters
The result supplies a concrete prime-triplet instance inside the arithmetic-functions module. Although the used_by graph is empty, the statement supports the Möbius footholds described in the module documentation and can serve as a base case for later Dirichlet or inversion lemmas. In the Recognition framework it aligns with the use of small primes in gap derivations (T7 eight-tick octave) and empirical programs, leaving open the question of whether the (2,4) gap pattern connects to phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.