liouville_eight
plain-language theorem explainer
The theorem records that the Liouville function evaluates to -1 at the integer 8. Analytic number theorists reference this concrete case when verifying the sign of λ(n) for prime powers with odd total exponent. The proof is a direct native computation that applies the definition λ(n) = (-1)^Ω(n) and evaluates the exponent for n = 2^3.
Claim. The Liouville function satisfies $λ(8) = -1$.
background
The Liouville function is defined by λ(n) = (-1)^Ω(n) for positive n, where Ω(n) is the total number of prime factors counted with multiplicity; the definition sets λ(0) = 0 by convention. This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the Liouville function to support prime calculations. The upstream definition supplies the general formula via the bigOmega helper and the special case at zero.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the expression directly from the definition of the Liouville function.
why it matters
This evaluation supplies a concrete anchor for the Liouville function at the prime power 8 = 2^3, where the odd exponent produces the negative sign. It forms part of the arithmetic-function toolkit in the module that underpins later prime and square-free manipulations, even though no immediate downstream theorems are listed. Within the Recognition Science setting it contributes to the number-theoretic layer supporting the Recognition Composition Law and the forcing-chain calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.