isolated_prime_thirtyseven
plain-language theorem explainer
37 is prime while its neighbors 35 and 39 are composite, supplying a concrete isolated-prime instance marked RS-relevant. Number theorists working with arithmetic functions or prime-gap examples in the Recognition framework would cite it. The proof is a one-line native_decide term that directly evaluates the three primality predicates.
Claim. $37$ is prime while $35 = 5 × 7$ and $39 = 3 × 13$ are composite.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Local notation uses the transparent abbrev Prime for Nat.Prime. The setting prepares Dirichlet inversion and square-free checks once basic interfaces stabilize.
proof idea
One-line wrapper that applies native_decide to the conjunction of primality statements for 37, 35 and 39.
why it matters
The declaration supplies a specific RS-relevant isolated-prime datum inside the arithmetic-functions module. It occupies a slot in the primes section that could later feed Möbius-based counting or phi-ladder mass formulas, though no downstream uses are recorded. It touches the framework's reliance on elementary number-theoretic primitives without invoking the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.