liouville_zero
plain-language theorem explainer
The Liouville function satisfies λ(0) = 0 by explicit convention in its definition. Number theorists building arithmetic-function identities or Dirichlet-series expansions in the Recognition Science setting would cite this when initializing sums or products over the naturals. The proof is a one-line simplification that unfolds the case distinction inside the liouville definition.
Claim. $λ(0) = 0$, where $λ(n) = (-1)^{Ω(n)}$ for $n ≠ 0$ and $λ(0) = 0$ by convention.
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 introduced directly as λ(n) = (-1)^Ω(n) for n ≠ 0, with the zero case fixed by convention to ensure well-defined behavior in sums. The upstream definition states: def liouville (n : ℕ) : ℤ := if n = 0 then 0 else (-1) ^ bigOmega n. The local setting keeps statements minimal so that deeper Dirichlet algebra can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the liouville definition, which immediately returns zero on the n = 0 branch.
why it matters
This anchors the zero case for the Liouville function inside the arithmetic-functions module, ensuring consistent initialization for any later multiplicative-function work. It supplies the convention step required before inversion formulas or prime-related identities can be stated cleanly. No downstream uses are recorded yet, so its integration into larger Recognition Science number-theory constructions remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.