weak_prime_nineteen
plain-language theorem explainer
The statement asserts that 19, 17, and 23 are all prime and that 19 lies strictly below the average of 17 and 23. Number theorists working on prime gaps or arithmetic functions inside the Recognition Science setting would cite this concrete instance. The proof reduces the conjunction to a single native_decide call that evaluates the arithmetic directly.
Claim. $19$ is prime, $17$ is prime, $23$ is prime, and $19 < (17 + 23)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent local alias for Nat.Prime. This theorem records a specific numerical fact about neighboring primes that can support later squarefree checks or inversion formulas in the same file.
proof idea
The proof is a one-line wrapper that applies native_decide to the decidable conjunction of three primality predicates and the inequality.
why it matters
The declaration supplies a verified weak-prime instance, as stated in its documentation. It anchors basic prime facts inside the ArithmeticFunctions module, which prepares Möbius footholds for Dirichlet algebra. No downstream theorems are recorded, yet the fact remains available for any later appeal to concrete prime arithmetic in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.