strong_prime_twentynine
plain-language theorem explainer
29 satisfies the strong-prime condition: it is prime, 23 and 31 are prime, and 29 exceeds the average of those neighbors. Number theorists tabulating strong primes or prime-gap examples would cite the explicit check. The argument is a single native_decide term that resolves the full conjunction of primality predicates and the arithmetic comparison.
Claim. $29$ is prime, $23$ is prime, $31$ is prime, and $29 > (23 + 31)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem appears among sibling definitions for mobius, bigOmega, and squarefree predicates. The local setting uses the transparent alias Prime n := Nat.Prime n for the standard primality predicate on natural numbers. Upstream results include structural 'is' predicates from foundation modules that certify collision-free or tautological properties, together with the primality alias itself.
proof idea
The proof is a one-line term that invokes native_decide on the conjunction. The decision procedure simultaneously checks the three primality statements and evaluates the integer inequality.
why it matters
The declaration records an explicit strong-prime instance inside the arithmetic-functions module. No downstream theorems depend on it. It supplies a concrete number-theoretic fact that can anchor later calculations involving primes, without engaging the core Recognition Science forcing chain, RCL, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.