weak_prime_thirtyone
plain-language theorem explainer
Verification that 31 qualifies as a weak prime asserts primality of 31 together with its neighbors 29 and 37 plus the inequality 31 below their average. Number theorists checking small prime gaps or concrete arithmetic instances inside Recognition Science would cite this fact. The proof reduces the entire conjunction to a single native_decide evaluation on these small integers.
Claim. The integers $29$, $31$, and $37$ are prime and $31 < (29 + 37)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent local alias for the standard primality predicate on natural numbers. Upstream results include structural 'is' predicates from foundational modules that certify collision-free or algebraic properties, together with the basic Prime abbreviation from the primes basic file.
proof idea
The proof is a one-line wrapper that invokes native_decide to resolve the conjunction of three primality checks and the numerical inequality.
why it matters
This supplies a verified weak-prime instance in the arithmetic functions layer. No downstream uses are recorded. It contributes a basic arithmetic fact without engaging the Möbius or big-Omega siblings defined in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.