prime_quadruplet_onehundredninetyone
plain-language theorem explainer
The integers 191, 193, 197, and 199 form a prime quadruplet with successive gaps of 2, 4, and 2. Number theorists examining explicit prime constellations would reference this verified case. The proof reduces to a single native_decide invocation that performs direct primality testing on each term.
Claim. The numbers $191$, $193$, $197$, and $199$ are all prime.
background
The declaration sits inside the ArithmeticFunctions module, whose primary focus is lightweight wrappers around Mathlib's Möbius function and related arithmetic tools. The module keeps statements minimal to allow later layering of Dirichlet inversion once interfaces stabilize. It depends on the basic definition of primality from the sibling Primes.Basic module together with the Primes instantiation in EulerInstantiation.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the conjunction of four primality statements by direct computation.
why it matters
This supplies a concrete, machine-verified instance of a prime quadruplet inside the arithmetic-functions layer. No downstream theorems currently cite it, so it functions as an explicit data point rather than a lemma in a larger chain. It aligns with the framework's pattern of recording small, decidable facts that can later support constructions involving the phi-ladder or forcing steps, though no direct tie to J-cost or spectral emergence is present here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.