weak_prime_sixtyone
plain-language theorem explainer
The theorem verifies that 61 qualifies as a weak prime by confirming primality of 61, 59, and 67 together with the inequality 61 < (59 + 67)/2. Number theorists checking small prime configurations for arithmetic function computations in Recognition Science would cite it for explicit boundary verification. The proof is a one-line term wrapper that invokes native_decide to discharge the decidable finite statement.
Claim. $61$, $59$, and $67$ are prime and $61 < (59 + 67)/2$.
background
The declaration resides in the ArithmeticFunctions module, which supplies lightweight wrappers around Mathlib arithmetic functions beginning with the Möbius function μ. The local setting keeps statements minimal to allow later layering of Dirichlet algebra and inversion once basic interfaces stabilize. Prime is the repository-local alias for Nat.Prime. Upstream results supply collision-free checks and algebraic tautologies from Foundation and GameTheory modules, but this theorem depends only on decidability of primality for small naturals.
proof idea
The proof is a one-line term wrapper that applies native_decide to the conjunction of three primality predicates and the arithmetic comparison, resolving the entire decidable proposition in a single step.
why it matters
This supplies a concrete small-case anchor for prime verification inside the number theory layer supporting arithmetic functions such as Möbius. It fills an explicit check in the primes module without feeding any downstream theorems. No direct link appears to the forcing chain, RCL, or phi-ladder, leaving open whether weak-prime facts integrate into mass formulas or eight-tick structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.