strong_prime_onehundredone
plain-language theorem explainer
101 exceeds the average of its neighboring primes 97 and 103 while all three numbers are prime. Number theorists examining strong primes or explicit gap examples would cite this verified instance. The proof reduces to a single native_decide call that evaluates the primality predicates and the arithmetic comparison directly.
Claim. Let $p=101$, $q=97$ and $r=103$. Then $p$, $q$ and $r$ are all prime and $p > (q + r)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard natural-number primality predicate. The local setting keeps statements minimal to allow later layering of Dirichlet algebra and inversion once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the conjunction of three primality statements and the inequality.
why it matters
This supplies a concrete verified instance of a strong prime inside the NumberTheory.Primes submodule that supports arithmetic-function calculations. No parent theorem is recorded among the used-by edges. It contributes an explicit number-theoretic fact that may later interface with the phi-ladder or forcing-chain constructions, though the connection remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.