mobius_ne_zero_iff_squarefree
The equivalence states that the Möbius function μ(n) is nonzero precisely when n is squarefree. Number theorists applying Möbius inversion or studying prime factorizations would cite this characterization. The proof is a one-line term wrapper that unfolds the local mobius abbreviation and invokes the matching Mathlib lemma.
claimFor any natural number $n$, the Möbius function satisfies $μ(n) ≠ 0$ if and only if $n$ is squarefree.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The abbreviation mobius is defined as ArithmeticFunction.moebius, mapping natural numbers to integers. Squarefree n is the standard predicate that n is not divisible by p² for any prime p. This sits among sibling results on the Möbius function such as its definition and its values on primes.
proof idea
The proof is a one-line term wrapper. It applies simpa with the mobius abbreviation to reduce the local statement to ArithmeticFunction.moebius_ne_zero_iff_squarefree from Mathlib.
why it matters in Recognition Science
This theorem supplies the positive direction for the vanishing criterion of the Möbius function and feeds directly into the sibling result mobius_eq_zero_iff_not_squarefree. It also supports the later bridge mobius_ne_zero_iff_vp_le_one that rewrites the condition in terms of prime exponents. The result provides a basic arithmetic foothold inside the NumberTheory.Primes layer without touching Recognition Science landmarks such as the J-function or the phi-ladder.
scope and limits
- Does not compute the explicit value of μ(n) when n is squarefree.
- Does not address the case n = 0.
- Does not extend the equivalence to other arithmetic functions.
- Does not connect to the Recognition forcing chain or constants such as phi.
formal statement (Lean)
46theorem mobius_ne_zero_iff_squarefree {n : ℕ} : mobius n ≠ 0 ↔ Squarefree n := by
proof body
Term-mode proof.
47 simpa [mobius] using (ArithmeticFunction.moebius_ne_zero_iff_squarefree (n := n))
48
49/-- `μ n = 0` iff `n` is not squarefree. -/