mobius_eq_zero_iff_not_squarefree
The Möbius function vanishes on a natural number precisely when that number fails to be squarefree. Number theorists applying inclusion-exclusion or inverting the zeta function would invoke the equivalence to restrict summation domains. The argument is a one-line term proof that negates the companion non-vanishing criterion via congruence of negations and simplification.
claimFor every natural number $n$, the Möbius function satisfies $μ(n)=0$ if and only if $n$ is not squarefree.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function defined as the arithmetic function moebius. The companion theorem states that μ(n) is nonzero exactly when n is squarefree. This equivalence is obtained by logical negation of that statement. The local setting is arithmetic functions providing Möbius footholds for later Dirichlet algebra once basic interfaces stabilize.
proof idea
The term proof applies not_congr to the companion theorem mobius_ne_zero_iff_squarefree and then simplifies the resulting negation with not_ne_iff.
why it matters in Recognition Science
This result completes the basic characterization of the Möbius function within the arithmetic functions module. It supports later squarefree detection inside the Recognition Science number-theoretic scaffolding, although no downstream uses are recorded yet. It supplies the missing half of the squarefree criterion needed for multiplicative-function control.
scope and limits
- Does not supply the explicit sign formula for μ on squarefree arguments.
- Does not extend the criterion to other arithmetic functions such as bigOmega.
- Does not address analytic continuation or Dirichlet series convergence.
formal statement (Lean)
50theorem mobius_eq_zero_iff_not_squarefree {n : ℕ} : mobius n = 0 ↔ ¬Squarefree n := by
proof body
Term-mode proof.
51 -- Negate `μ n ≠ 0 ↔ Squarefree n`.
52 simpa [not_ne_iff] using (not_congr (mobius_ne_zero_iff_squarefree (n := n)))
53
54/-- If `n` is squarefree then `μ n = (-1)^(cardFactors n)`. -/