zeta_isMultiplicative
plain-language theorem explainer
The declaration shows that the zeta arithmetic function is multiplicative. Number theorists working with Dirichlet convolution and Möbius inversion cite this as the basic property of the constant-1 function. The proof is a one-line term wrapper that unfolds the local definition of zeta and invokes the corresponding Mathlib lemma.
Claim. The arithmetic function $ζ$ defined by $ζ(n)=1$ for every positive integer $n$ is multiplicative: $ζ(mn)=ζ(m)ζ(n)$ whenever $gcd(m,n)=1$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function μ. Zeta is the constant function with value 1 at every positive integer; it serves as the neutral element for Dirichlet convolution. The local theoretical setting keeps statements minimal so that basic interfaces stabilize before deeper inversion results are added.
proof idea
The proof is a term-mode one-liner. It applies simp only [zeta] to unfold the definition, then uses exact ArithmeticFunction.isMultiplicative_zeta from Mathlib.
why it matters
The result supplies the multiplicative property needed for the subsequent identity μ * ζ = ε that opens the Möbius-inversion section. It anchors the number-theoretic layer of the Recognition framework, supporting prime factorization work that feeds into the phi-ladder and the eight-tick octave. No downstream uses appear yet, so its direct connection to forcing-chain steps remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.