strong_prime_onehundredseven
plain-language theorem explainer
107 is established as a strong prime by verifying that it, along with neighbors 103 and 109, are all prime and that it exceeds their average. Number theorists or cryptographers selecting primes for security applications would cite this concrete fact. The verification is a single native_decide call that resolves the conjunction by direct computation.
Claim. $107$, $103$, and $109$ are prime numbers and $107 > (103 + 109)/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 Nat.Prime predicate on natural numbers. This theorem records a specific numerical instance of a strong prime, defined by the middle value exceeding the arithmetic mean of its immediate prime neighbors.
proof idea
The proof is a one-line term that applies native_decide to the conjunction of three primality checks and the stated inequality.
why it matters
The declaration supplies a verified strong-prime datum inside the arithmetic-functions file. No downstream theorems reference it, so it functions as an isolated numerical checkpoint rather than a lemma in a larger chain. Within Recognition Science it could support discrete selections on the phi-ladder or specific rung calculations, but the current placement leaves that connection open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.