liouville_ten
plain-language theorem explainer
The Liouville function evaluates to 1 at 10, since 10 = 2 × 5 has exactly two prime factors counting multiplicity. Number theorists verifying arithmetic function tables or checking sign patterns for small composite inputs would cite this evaluation. The proof is a one-line native decision that computes the parity of Ω(10) directly from the definition.
Claim. $λ(10) = 1$, where $λ(n) = (-1)^{Ω(n)}$ 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 n > 0 (with λ(0) = 0 by convention). The surrounding file supplies small wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ, and keeps statements lightweight before adding Dirichlet inversion layers. The upstream liouville definition supplies the direct link to bigOmega, which itself counts prime factors with multiplicity.
proof idea
This is a one-line wrapper that applies native_decide to evaluate the equality by direct computation from the Liouville definition.
why it matters
The declaration supplies a concrete base-case check for the sign of λ on a number with even Ω, confirming the general rule λ(n) = (-1)^Ω(n) for this input. It sits inside the arithmetic-functions module that supports prime-related number theory but has no recorded downstream uses, so it functions as a verification point rather than a core step in any Recognition Science forcing chain or mass-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.