strong_prime_seventyone
plain-language theorem explainer
71 qualifies as a strong prime by exceeding the average of its immediate neighbors 67 and 73 in the prime sequence. Number theorists maintaining catalogs of prime gaps or strong primes would cite this explicit verification. The proof is a one-line native decision procedure that evaluates the primality predicates and the arithmetic comparison directly.
Claim. $71$ is prime, $67$ is prime, $73$ is prime, and $71 > (67 + 73)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, while keeping statements minimal until deeper Dirichlet algebra is added. This theorem appears among prime statements in the NumberTheory.Primes section. The predicate Prime is the repo-local alias for the standard natural-number primality predicate Nat.Prime.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the conjunction of three primality checks and the midpoint inequality by direct evaluation.
why it matters
The declaration supplies a concrete numerical instance of the strong-prime property inside the arithmetic-functions module. It feeds no downstream results in the current graph. The statement remains a basic number-theoretic fact that could later support prime-distribution arguments or Möbius-inversion applications, yet carries no direct connection to the Recognition Science forcing chain, phi-ladder, or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.