strong_prime_thirtyseven
plain-language theorem explainer
This theorem confirms 37 as a strong prime by verifying its primality together with that of 31 and 41, plus the inequality showing 37 exceeds their average. Number theorists working on prime gaps or arithmetic anchors in Recognition Science would cite it for concrete numerical checks. The proof reduces the full conjunction to a decidable computation via native decision procedures.
Claim. $37$ is prime, $31$ is prime, $41$ is prime, and $37 > (31 + 41)/2$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function for later Dirichlet inversion. Statements remain minimal until basic interfaces stabilize. Primality is the standard predicate on natural numbers. Upstream results supply an alias for that predicate plus foundational structures from option programs, simplicial ledgers, mechanism design, and Ramanujan bridges, though this claim rests mainly on computational primality checking.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the conjunction of three primality statements and the arithmetic inequality.
why it matters
This supplies a verified strong-prime instance marked RS-relevant, supporting numerical footholds in the arithmetic-functions module. It sits alongside Möbius definitions without direct downstream uses in the current graph. The placement aligns with Recognition Science use of specific primes for phi-ladder checks and constant derivations, though linkage to the forcing chain remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.