weak_prime_seventythree
plain-language theorem explainer
The statement verifies that 73 qualifies as a weak prime by confirming primality of 73 together with its immediate neighbors 71 and 79 and the strict inequality placing 73 below their average. Number theorists building arithmetic-function identities or prime-gap lemmas inside the Recognition Science framework would cite this concrete instance. The proof reduces the entire conjunction to a single native decision procedure that evaluates primality and the arithmetic comparison directly.
Claim. $73$ is prime, $71$ is prime, $79$ is prime, and $73 < (71 + 79)/2$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function. Prime is the transparent alias for the standard natural-number primality predicate. This theorem appears among siblings that introduce Möbius inversion tools and big-Omega functions intended for Dirichlet-series constructions.
proof idea
The proof is a one-line term that invokes native_decide to resolve the three primality checks and the numerical inequality by direct computation.
why it matters
This supplies a verified small-prime fact that can anchor arithmetic-function calculations or gap analyses in the Recognition Science number-theory layer. It connects to the broader framework by providing concrete primes that may enter mass-ladder or phi-ladder constructions, though no downstream use is recorded. It fills a basic verification step without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.