strong_prime_fortyone
plain-language theorem explainer
Verification that 41 is a strong prime rests on confirming primality of 41, 37, and 43 together with the midpoint inequality 41 > (37 + 43)/2. Number theorists examining explicit prime constellations or gap properties would cite the check. The argument succeeds via a single native_decide invocation that evaluates the entire conjunction by direct computation on natural numbers.
Claim. The integers 41, 37 and 43 are all prime and satisfy $41 > (37 + 43)/2$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function and its basic properties before deeper Dirichlet algebra is added. The local setting keeps statements minimal so that inversion formulas and related identities can be layered once the interfaces stabilize. The Prime predicate used here is the repository alias for the standard natural-number primality predicate.
proof idea
The proof is a one-line term wrapper that applies native_decide to evaluate the primality assertions and the arithmetic comparison directly.
why it matters
The declaration supplies a concrete numerical instance inside the arithmetic-functions module but feeds no downstream theorems. It illustrates the kind of explicit prime fact that could later support Möbius-based calculations, though no such connection is drawn. It touches basic number-theory scaffolding without reference to the Recognition Science forcing chain, J-uniqueness, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.