liouville_mul
The Liouville function satisfies complete multiplicativity: λ(mn) equals λ(m) times λ(n) for nonzero natural numbers m and n. Analytic number theorists would cite this when handling Dirichlet series or sieve expansions involving the Liouville function. The proof is a direct term reduction that applies the additivity of Ω and the power-addition rule after unfolding the definition.
claimFor all nonzero natural numbers $m$ and $n$, the Liouville function satisfies $λ(mn) = λ(m) λ(n)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to related objects such as the Liouville function. The Liouville function is defined via λ(n) = (-1)^Ω(n) with a conditional clause for the zero case, where Ω counts prime factors counted with multiplicity. This sits inside the arithmetic-functions layer that prepares Dirichlet-algebra tools. The key upstream result is bigOmega_mul, which states that Ω(mn) = Ω(m) + Ω(n) for nonzero m and n.
proof idea
The term proof first derives mn ≠ 0 from the two nonzero hypotheses. It then unfolds the liouville definition at m, n, and mn, reducing the conditional branches via simp. The step rewrites the exponent via bigOmega_mul and applies pow_add to obtain the product of the two powers.
why it matters in Recognition Science
The result records the complete multiplicativity of the Liouville function inside the arithmetic-functions module. It supplies a basic algebraic identity that would feed any later development of Dirichlet convolution or inversion formulas, though no downstream uses are recorded. Within Recognition Science the lemma remains a pure number-theory foothold; it does not yet connect to the J-cost or forcing-chain landmarks.
scope and limits
- Does not address the case m = 0 or n = 0.
- Does not establish multiplicativity for the Möbius function.
- Does not treat analytic properties or generating functions.
formal statement (Lean)
324theorem liouville_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
325 liouville (m * n) = liouville m * liouville n := by
proof body
Term-mode proof.
326 have hmn : m * n ≠ 0 := mul_ne_zero hm hn
327 simp only [liouville, hm, hn, hmn, ↓reduceIte]
328 rw [bigOmega_mul hm hn, pow_add]
329
330/-! ### Identity function (for Dirichlet algebra) -/
331
332/-- The identity arithmetic function id(n) = n. -/