zeta_apply
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not address the analytic continuation of the Riemann zeta function.
- Does not evaluate zeta at zero or negative arguments.
- Does not prove multiplicativity or other functional equations.
- Does not connect to Dirichlet convolution or inversion formulas.
Lean usage
theorem zeta_one : zeta 1 = 1 := zeta_apply (by decide)formal statement (Lean)
223theorem zeta_apply {n : ℕ} (hn : n ≠ 0) : zeta n = 1 := by
proof body
Term-mode proof.
224 simp only [zeta, ArithmeticFunction.zeta_apply, hn, ↓reduceIte]
225
226/-- ζ(0) = 0. -/