liouville_one
plain-language theorem explainer
The Liouville function evaluates to 1 at the unit. Number theorists cite this base case when reducing λ on empty factorizations or prime-power cases. The proof is a one-line simplification that invokes the definition of λ together with the length of the prime-factors list for 1.
Claim. Let λ be the Liouville function defined by λ(n) = (-1)^{Ω(n)} for positive integers n, where Ω(n) counts the prime factors of n with multiplicity. Then λ(1) = 1.
background
The module supplies lightweight wrappers for arithmetic functions, beginning with the Möbius function and extending to the Liouville function. The latter is defined directly as λ(n) = (-1)^{bigOmega n} for n > 0, where bigOmega n equals the length of the list of prime factors of n. The upstream theorem bigOmega_apply states that bigOmega n = n.primeFactorsList.length, so the empty list for n = 1 yields the exponent 0.
proof idea
This is a one-line wrapper that applies the definition of liouville and the theorem bigOmega_apply, reducing the claim to (-1)^0 = 1 by simplification.
why it matters
The result supplies the zero-exponent case for the downstream theorem liouville_prime_pow, which establishes λ(p^k) = (-1)^k. It forms a foundational step inside the arithmetic-functions module whose prime-factorization tools support later Recognition Science constructions that rely on multiplicative structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.