liouville_prime_pow
plain-language theorem explainer
Liouville function at a prime power p^k equals (-1)^k. Number theorists simplifying sums or Dirichlet series over prime factorizations cite this reduction when handling completely multiplicative arithmetic functions. The argument splits on the exponent via case analysis, invokes the definition of liouville in terms of total prime factor count, and applies the prime-power formula for that count together with the base case at 1.
Claim. Let $p$ be a prime and $k$ a nonnegative integer. Then the Liouville function satisfies $λ(p^k) = (-1)^k$, where $λ(n) = (-1)^{Ω(n)}$ for $n > 0$ and $Ω$ counts prime factors counted with multiplicity.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the Liouville function. The Liouville function is defined directly as λ(n) = 0 when n = 0 and (-1)^Ω(n) otherwise, with Ω realized by the cardFactors arithmetic function (abbreviated bigOmega). This supplies the explicit evaluation on prime powers as a basic building block for multiplicative properties. The local theoretical setting is arithmetic functions as footholds for Möbius inversion and related number-theoretic tools. Upstream results include the liouville definition, the liouville_one theorem establishing λ(1) = 1, and the prime_iff equivalence used to access Nat.Prime.
proof idea
The proof performs case analysis on k. The zero case reduces immediately to liouville_one. The successor case records that p to a positive power is nonzero, simplifies the liouville definition, rewrites bigOmega via the lemma ArithmeticFunction.cardFactors_apply_prime_pow (which states that Ω(p^m) = m for prime p), and concludes the sign is (-1)^{k+1}.
why it matters
This supplies the concrete evaluation rule for the Liouville function on prime powers inside the arithmetic functions module. It supports calculations that may feed into Dirichlet series or inversion formulas within the Recognition Science number-theoretic scaffolding. No parent theorems appear in the used_by graph, indicating it functions as a foundational lemma rather than a derived step. The result aligns with the framework's use of standard arithmetic functions to interface with forcing-chain constructions and self-similar structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.