weak_prime_eightythree
plain-language theorem explainer
83 is a prime lying strictly below the arithmetic mean of its neighboring primes 79 and 89. Number theorists examining small prime gaps or weak-prime classifications would reference this concrete instance. The proof is a one-line wrapper that invokes native_decide to confirm the three primality claims and the inequality by direct computation.
Claim. $83$ is prime, $79$ is prime, $89$ is prime, and $83 < (79 + 89)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related objects such as big-Omega. Prime is introduced as a transparent alias for Nat.Prime. The present theorem appears among these wrappers but records a specific numerical fact rather than a general identity.
proof idea
The proof is a one-line wrapper that applies native_decide to the entire conjunction, letting the kernel decide primality of 79, 83, 89 and the numerical comparison by exhaustive computation.
why it matters
The declaration supplies a verified small-case fact inside the arithmetic-functions module. It supports later development of Möbius-based tools but carries no recorded downstream uses and does not invoke the forcing chain, phi-ladder, or Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.