mobius_sq_eq_one_iff_squarefree
plain-language theorem explainer
The equivalence asserts that the square of the Möbius function at a natural number n equals one precisely when n has no repeated prime factors. Analytic number theorists would cite the result when isolating the squarefree indicator in sums or when verifying vanishing conditions for μ. The proof splits into directions: the forward leg reaches a contradiction by substituting the zero value on non-squarefree inputs, while the converse substitutes the explicit sign formula and reduces the exponent parity via the total prime factor count.
Claim. For any natural number $n$, the equality $μ(n)^2 = 1$ holds if and only if $n$ is square-free.
background
The Möbius function μ maps natural numbers to integers and is realized here as an arithmetic function. It vanishes exactly when n fails to be square-free, and on square-free inputs it equals (-1) raised to the total number of prime factors counted with multiplicity (denoted bigOmega or Ω(n)). The square-free predicate requires every exponent in the prime factorization to be at most one.
proof idea
The term proof opens a biconditional with constructor. The left-to-right direction assumes the squared equality, supposes n is not square-free, invokes mobius_eq_zero_of_not_squarefree to obtain μ(n) = 0, and derives an immediate contradiction by simplification. The right-to-left direction assumes square-freeness, replaces μ(n) by (-1)^bigOmega(n) via mobius_apply_of_squarefree, rewrites the square using that twice bigOmega is even, and applies the fact that (-1) to an even power equals one.
why it matters
The theorem supplies the standard characterization of square-free integers through the Möbius function and therefore serves as a prerequisite for any later arithmetic-function identities in the NumberTheory.Primes hierarchy. No downstream declarations cite it yet, so it functions as foundational scaffolding rather than a direct link into the forcing chain or J-cost results. It remains independent of the Recognition Science constants and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.