weak_prime_fortythree
plain-language theorem explainer
The declaration establishes that 43 is a weak prime by verifying its primality together with the primality of its immediate neighbors 41 and 47 and the strict inequality 43 < (41 + 47)/2. Number theorists examining concrete prime-gap instances or arithmetic-function examples would cite this numerical fact. The proof is a one-line wrapper that applies native_decide to confirm the conjunction by direct evaluation.
Claim. $43$ is prime, $41$ is prime, $47$ is prime, and $43 < (41 + 47)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is a transparent alias for the standard Nat.Prime predicate on natural numbers. The local setting is a collection of basic prime facts that can later support Dirichlet inversion or other arithmetic developments.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the conjunction of the three primality statements and the numerical inequality.
why it matters
This supplies a verified numerical instance of the weak-prime property for 43, as stated in the documentation. It resides in the primes arithmetic-functions module and currently has no downstream citations. The result contributes a concrete base fact to the collection of prime statements that may later feed arithmetic-function machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.