zeta_apply
plain-language theorem explainer
The arithmetic zeta function evaluates to 1 at every positive integer. Number theorists applying Möbius inversion or Dirichlet series would cite this evaluation as the base case. The proof is a one-line simplification that unfolds the zeta abbreviation and reduces the conditional via the nonzero hypothesis.
Claim. For every positive integer $n$, the arithmetic zeta function satisfies $ζ(n) = 1$.
background
This theorem lives in the module supplying lightweight wrappers around Mathlib arithmetic functions, with the Möbius function as the initial foothold and zeta introduced as a constant-1 function on positive integers. The upstream definition states that zeta is the abbreviation ArithmeticFunction.zeta, the constant function 1 on ℕ>0. The module keeps statements minimal to enable later layering of Dirichlet algebra and inversion once interfaces stabilize.
proof idea
The term proof applies simp to unfold the zeta abbreviation, invoke ArithmeticFunction.zeta_apply, and reduce the conditional using the hypothesis n ≠ 0 together with ↓reduceIte.
why it matters
The result supplies the constant value needed by the sibling theorems zeta_one and zeta_zero in the same module. It establishes the arithmetic zeta function's base evaluation, a prerequisite for multiplicativity statements and further arithmetic-function identities within the primes module. No direct link to Recognition Science forcing-chain steps appears here; the declaration remains pure number-theoretic scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.