weak_prime_onehundredthree
plain-language theorem explainer
103 lies below the average of its neighboring primes 101 and 107, satisfying the weak-prime inequality. Number theorists examining prime gaps or Recognition Science applications to arithmetic would reference this explicit instance. The proof reduces to a single native decision procedure that evaluates the primality predicates and the numerical comparison directly.
Claim. $103$ is prime, $101$ is prime, $107$ is prime, and $103 < (101 + 107)/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. The local setting is therefore basic number-theoretic predicates that can later support Dirichlet inversion or square-free checks.
proof idea
The proof is a one-line term wrapper that applies native_decide to the entire conjunction.
why it matters
The declaration supplies a concrete numerical anchor marked RS-relevant in its documentation and placed immediately before the superprimes commentary. It draws on the basic Prime definition and sits inside the arithmetic-functions module whose Möbius material is intended for later inversion lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.