prime_quadruplet_onehundredone
plain-language theorem explainer
The declaration asserts that 101, 103, 107 and 109 are all prime, forming a quadruplet with successive gaps of 2, 4 and 2. Number theorists examining small prime constellations or explicit arithmetic examples would reference this instance. The proof reduces the four primality checks to a single native_decide computation.
Claim. The integers $101$, $103$, $107$ and $109$ are all prime numbers.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The local setting keeps statements minimal so that deeper Dirichlet algebra and inversion can be added once basic interfaces stabilize. Primality is supplied by the transparent alias Prime n := Nat.Prime n from the Basic sibling module.
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 finite computation.
why it matters
This explicit quadruplet supplies a concrete arithmetic fact inside the NumberTheory.Primes component. It does not feed any downstream theorems in the current dependency graph. The statement remains a basic example that may later support prime-distribution arguments or constant derivations within the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.