strong_prime_ninetyseven
plain-language theorem explainer
97, 89 and 101 are all primes and 97 exceeds the average of 89 and 101. Number theorists anchoring concrete prime-gap checks inside the Recognition Science arithmetic layer would cite this instance. The proof is a one-line native_decide term that resolves the entire conjunction of primality predicates and the numerical inequality at once.
Claim. $97$, $89$ and $101$ are prime numbers and $97 > (89 + 101)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent repo-local alias for Nat.Prime. This declaration appears among siblings that define and apply μ on square-free inputs, yet asserts only a specific numerical fact rather than a general inversion law.
proof idea
One-line wrapper that applies native_decide to the conjunction of three primality statements and the arithmetic comparison.
why it matters
Supplies a verified numerical anchor for strong-prime examples inside the arithmetic-functions module. It sits downstream of the Prime alias and upstream of any future prime-gap or distribution results, but records zero uses. The fact does not touch the core Recognition Science forcing chain, RCL or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.