weak_prime_sixtyone
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 in Recognition Science
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.
scope and limits
- Does not define weak primes for arbitrary integers.
- Does not invoke or depend on the Möbius function.
- Does not reference the Recognition Composition Law or phi-ladder.
- Does not extend to prime gaps or density statements.
formal statement (Lean)
2771theorem weak_prime_sixtyone : Prime 61 ∧ Prime 59 ∧ Prime 67 ∧ 61 < (59 + 67) / 2 := by native_decide
proof body
Term-mode proof.
2772
2773/-- 73 is a weak prime: 73 < (71 + 79)/2 = 75. -/