weak_prime_eightynine
plain-language theorem explainer
The declaration verifies that 89 is a weak prime by confirming primality of 89, 83, and 97 together with the strict inequality 89 below their arithmetic mean. Number theorists cataloging small primes or checking numerical instances inside the Recognition Science arithmetic layer would reference this fact. The proof reduces to one native_decide invocation that evaluates the finite conjunction directly.
Claim. $89$ is prime, $83$ is prime, $97$ is prime, and $89 < (83 + 97)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and keeping statements minimal until Dirichlet inversion stabilizes. Prime is the transparent local alias for the standard natural-number primality predicate. Upstream dependencies include several 'is' structures from foundation and game-theory modules that certify collision-free or tautological properties, plus the primality alias itself.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the conjunction of three primality checks and the numerical inequality.
why it matters
This supplies a concrete weak-prime instance inside the arithmetic-functions module, consistent with the adjacent RS-relevant check for 103. No downstream theorems yet depend on it, so its role remains preparatory for any later prime-gap or distribution arguments that might link to the eight-tick octave or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.