liouville_fortyfive
plain-language theorem explainer
The declaration establishes that the Liouville function evaluates to negative one at 45. Number theorists working with multiplicative functions cite this explicit value to confirm the sign rule based on the parity of the total prime factor count. The proof reduces immediately to a native decision procedure that computes the result from the definition.
Claim. $λ(45) = -1$, where $λ(n) = (-1)^{Ω(n)}$ for $n > 0$ and $Ω(n)$ is the total number of prime factors of $n$ counted with multiplicity.
background
The Liouville function is introduced in this module via the definition λ(n) = (-1)^bigOmega n for positive n (with the convention λ(0) = 0). This arithmetic function sits alongside the Möbius function μ, which the module presents as a basic interface for later Dirichlet inversion work. The upstream liouville definition supplies the direct implementation that the present theorem evaluates at the specific argument 45 = 3² × 5.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the definition of liouville directly at 45, confirming that the exponent Ω(45) = 3 is odd and therefore yields -1.
why it matters
This explicit evaluation serves as a verification checkpoint inside the arithmetic functions module, which supplies lightweight wrappers around standard number-theoretic functions before deeper inversion results are layered on. It aligns with the module's role in providing concrete instances that can later support properties of multiplicative functions. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.