zeta_one
plain-language theorem explainer
The arithmetic zeta function evaluates to 1 at argument 1. Number theorists constructing Dirichlet series or preparing Möbius inversion steps cite this base case. The proof is a one-line wrapper that invokes the general zeta_apply lemma together with a decidable check that the input is nonzero.
Claim. $ζ(1) = 1$, where $ζ$ is the arithmetic zeta function returning the constant value 1 on every positive integer.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and the zeta function. Zeta is defined as the constant function 1 on positive integers. Upstream, zeta_apply states that ζ(n) = 1 for every n ≠ 0. The local setting keeps statements minimal so that deeper Dirichlet algebra can be added later. The imported for structure records meta-realization axioms but is not invoked in this declaration.
proof idea
The proof is a one-line wrapper that applies zeta_apply to n = 1, using the decide tactic to discharge the hypothesis 1 ≠ 0.
why it matters
This declaration records the base value of the zeta function at 1 inside the arithmetic-functions module. It supports later number-theoretic identities that may feed into Recognition Science forcing chains or self-reference structures. No downstream uses are recorded yet, leaving open its precise role in inversion formulas or prime-counting arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.