mobius_twohundredten
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.