liouville_prime
plain-language theorem explainer
The declaration shows that the Liouville function evaluates to minus one at every prime. Analytic number theorists cite this evaluation when handling multiplicative functions or preparing Dirichlet series expansions. The term-mode proof reduces the definition of liouville via simplification, invokes the prime-factor count for primes, and normalizes the resulting exponent.
Claim. If $p$ is prime then the Liouville function satisfies $λ(p) = -1$, where $λ(n) = (-1)^{Ω(n)}$ for $n > 0$ and $Ω(n)$ denotes the total number of prime factors of $n$ 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 by λ(n) = 0 when n = 0 and λ(n) = (-1)^bigOmega n otherwise, with bigOmega serving as the abbreviation for ArithmeticFunction.cardFactors. The Prime predicate is a transparent alias for Nat.Prime, and the prime_iff theorem supplies the equivalence between the two.
proof idea
The proof first obtains Nat.Prime p from the hypothesis via the prime_iff theorem and records that p is nonzero. Simplification then unfolds the liouville definition to (-1) raised to bigOmega p. The cardFactors_apply_prime lemma supplies the fact that this exponent equals 1 for any prime, after which rewriting and norm_num finish the reduction to -1.
why it matters
This supplies the base case evaluation of the Liouville function on primes inside the arithmetic-functions layer. It supports sibling results on the Möbius function and prepares multiplicative-function identities before any deeper Dirichlet inversion is added. No direct link to the forcing chain, Recognition Composition Law, or physical constants appears; the result remains a supporting number-theoretic tool.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.