strong_prime_seventynine
plain-language theorem explainer
The statement verifies that 79 is a strong prime by confirming primality of 79, 73 and 83 together with the strict inequality 79 greater than their average. Number theorists building arithmetic-function tables or prime-gap facts inside the Recognition Science framework would cite the concrete instance. The proof is a direct computational decision that evaluates the conjunction without manual lemmas.
Claim. $79$ is prime, $73$ is prime, $83$ is prime, and $79 > (73 + 83)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The predicate Prime is the repository-local alias for the standard natural-number primality predicate. This theorem records a specific numerical fact about neighboring primes that can later support Möbius or Dirichlet calculations once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the primality assertions and the numerical comparison directly.
why it matters
The result supplies a concrete strong-prime datum for arithmetic-function scaffolding. It fills a small numerical checkpoint in the module whose larger aim is to stabilize Möbius footholds before adding inversion theorems. No parent theorem or downstream use is recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.