liouville
The Liouville function λ(n) equals (-1) raised to the total number of prime factors of n counted with multiplicity, with the convention λ(0) = 0. Number theorists studying multiplicative functions or Dirichlet series would cite this when relating λ to the Möbius function μ or evaluating special values. The definition is a direct conditional that delegates the exponent to the bigOmega abbreviation for Ω(n).
claimThe Liouville function satisfies λ(0) = 0 and λ(n) = (-1)^{Ω(n)} for n ≠ 0, where Ω(n) counts the prime factors of n with multiplicity.
background
This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to related maps. The upstream bigOmega abbreviation (defined as ArithmeticFunction.cardFactors) supplies Ω(n), the total number of prime factors counted with multiplicity. The local setting keeps statements minimal so deeper Dirichlet algebra can be layered once the basic interfaces stabilize.
proof idea
The definition is a direct case distinction on whether the input equals zero, returning the constant 0 in that case and otherwise applying (-1) raised to the value supplied by bigOmega.
why it matters in Recognition Science
This definition anchors the family of evaluation theorems liouville_eq, liouville_eight, liouville_fortyfive, and liouville_eq_mobius_of_squarefree. It is listed inside the inductive type ComplexTheoremRS among the core results of complex analysis from Recognition Science. Within the framework it supports relations between arithmetic functions and constants appearing in the eight-tick octave constructions.
scope and limits
- Does not define λ for negative integers or non-integers.
- Does not compute explicit prime factorizations of its argument.
- Does not assert multiplicativity or other functional equations.
- Does not reference the J-cost, phi-ladder, or forcing chain directly.
Lean usage
theorem liouville_eq {n : ℕ} (hn : n ≠ 0) : liouville n = (-1) ^ bigOmega n := by simp [liouville, hn]formal statement (Lean)
284def liouville (n : ℕ) : ℤ :=
proof body
Definition body.
285 if n = 0 then 0 else (-1) ^ bigOmega n
286
287/-- λ(0) = 0 (by convention). -/
used by (17)
-
ComplexTheoremRS -
liouville_eight -
liouville_eighthundredforty -
liouville_eq -
liouville_eq_mobius_of_squarefree -
liouville_fortyfive -
liouville_mul -
liouville_one -
liouville_prime -
liouville_prime_pow -
liouville_six -
liouville_ten -
liouville_thirty -
liouville_threehundredsixty -
liouville_twelve -
liouville_twohundredten -
liouville_zero