liouville_twelve
plain-language theorem explainer
The Liouville function evaluates to -1 at 12. Number theorists verifying explicit values on small composites or testing multiplicative function tables would cite this instance. The proof is a direct native_decide evaluation of the definition λ(n) = (-1)^Ω(n) for n > 0.
Claim. $λ(12) = -1$, where $λ(n) = (-1)^{Ω(n)}$ and $Ω(12) = 3$.
background
The Liouville function is introduced in this module as λ(n) = (-1)^Ω(n) for n > 0 (with λ(0) = 0 by convention), where Ω(n) counts prime factors with multiplicity. The module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function and extending to related objects such as Liouville. The upstream definition of liouville supplies the direct computation used here.
proof idea
One-line wrapper that applies native_decide to the definition of liouville at 12.
why it matters
This supplies an explicit evaluation of the Liouville function at 12 inside the arithmetic functions module. It serves as a concrete check during construction of multiplicative function tools in the Recognition Science number theory layer, though no downstream theorems depend on it yet. Such small cases stabilize the interface before deeper inversion or Dirichlet results are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.