mobius_twohundredten
The declaration establishes that the Möbius function evaluates to 1 at 210. Number theorists computing explicit values of arithmetic functions for squarefree integers with four distinct prime factors would cite this result. The proof proceeds as a one-line native decision procedure on the concrete integer input.
claim$μ(210) = 1$, where $μ$ is the Möbius function.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function $μ$ (implemented as ArithmeticFunction.moebius). The upstream abbrev defines mobius : ArithmeticFunction ℤ := ArithmeticFunction.moebius. The local setting keeps statements minimal so that deeper Dirichlet inversion can be added once the basic interfaces are stable.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the concrete evaluation of the Möbius function at 210.
why it matters in Recognition Science
This explicit value feeds the downstream theorem establishing that the Liouville function at 210 equals 1. It supplies a concrete foothold inside the arithmetic-functions module for the number-theoretic layer of the Recognition Science framework. No open scaffolding questions are addressed.
scope and limits
- Does not prove general properties or identities for the Möbius function.
- Does not compute the function at any integer other than 210.
- Does not address non-squarefree inputs or higher-order arithmetic functions.
formal statement (Lean)
1122theorem mobius_twohundredten : mobius 210 = 1 := by native_decide
proof body
Term-mode proof.
1123
1124/-- μ(18) = 0 (not squarefree, 9 | 18). -/