mobius_eighteen
plain-language theorem explainer
The Möbius function evaluates to zero at 18 because 18 is divisible by the square 9 and therefore not square-free. Number theorists applying Möbius inversion or checking arithmetic-function values at small composites would cite this evaluation. The proof is a one-line native decision that computes the function value directly from its definition.
Claim. $μ(18) = 0$, where $μ$ is the Möbius function.
background
The Möbius function is supplied as an arithmetic function ℕ → ℤ via a direct wrapper around Mathlib's ArithmeticFunction.moebius. The module supplies lightweight interfaces for such functions, with the explicit goal of enabling later Dirichlet inversion once the basic definitions stabilize. The sole upstream dependency is the abbrev that names this standard Möbius function without extra hypotheses.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the arithmetic function at 18 and confirm the result equals zero.
why it matters
This supplies a concrete evaluation case inside the arithmetic-functions module that supports later number-theoretic constructions. It fills a specific instance of the Möbius function as part of the NumberTheory.Primes scaffolding, though no downstream theorems currently depend on it. The declaration remains isolated from the Recognition Science forcing chain and constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.