feat(IK): prove isCompletelyMultiplicative_liouville

[Chessing234]

Closes #1685.

Motivation

isCompletelyMultiplicative_liouville was the last sorry standing between the
liouville definition and LSeries_liouville_eq (IK's $\zeta(2s)/\zeta(s)$
identity), which needs complete multiplicativity to run the Euler product.

Scope

• Proves isCompletelyMultiplicative_liouville in IwaniecKowalskiCh1.lean.
• No other declaration touched; no new sorry introduced.

The proof is the paper's own reason: $\Omega$ is completely additive, so
$\lambda = (-1)^{\Omega}$ is completely multiplicative over ℤ, and the
ℝ-valued statement is that identity pushed through Int.cast. Concretely it
threads through Mathlib's cardFactors_mul rather than inventing machinery —
IsCompletelyMultiplicative quantifies over all a b : ℕ including 0, so
the two zero cases are discharged first (arithmetic functions vanish at 0),
and cardFactors_mul then covers the rest.

Note for reviewers: this duplicates Mathlib

While proving this I found that Mathlib already carries the same function and
the same fact, in Mathlib/NumberTheory/ArithmeticFunction/Liouville.lean:

def liouville : ArithmeticFunction ℤ where
  toFun n := if n = 0 then 0 else (-1) ^ cardFactors n

theorem liouville_apply_mul (m n : ℕ) : liouville (m * n) = liouville m * liouville n
theorem isMultiplicative_liouville : IsMultiplicative liouville

liouville_apply_mul is exactly the multiplicative half of this PR's goal, for
all m n including zero. The local liouville here is
toArithmeticFunction (fun n => (-1 : ℤ) ^ Ω n), which unfolds to the same
function.

I did not switch to it in this PR, because Mathlib.NumberTheory.LSeries.Dirichlet
does not appear to pull that file in, so using it means adding an import — a
scope change I'd rather not smuggle into a sorry-closing PR (§1). If you'd
prefer the local liouville be replaced by (or proved equal to) Mathlib's, I'm
happy to do that as a follow-up; it would also give LSeries_liouville_eq a
shorter route. Flagging per §14.

Test plan

• lake build PrimeNumberTheoremAnd.IwaniecKowalskiCh1 — clean.
• No new warnings other than declaration uses 'sorry'. The file's sorry
  count goes 7 → 6; the warning at line 1789 is gone and no new one appears.
• lake build :blueprint — not run. I started it and had to kill it:
  this machine has ~1.3 GB free after the Mathlib cache, and the full-project
  build was consuming it fast enough to run out. This diff changes only a
  proof body — no @[blueprint] title/statement/proof field and no
  references.bib entry — so the generated per-module .tex should be
  byte-identical, but I have not verified that and am not claiming I did.
  Please let CI cover it, or tell me and I'll free space and re-run.