zeta_one
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 in Recognition Science
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.
scope and limits
- Does not prove convergence of any associated Dirichlet series.
- Does not compute values at primes or other positive integers.
- Does not invoke the Möbius function or square-free conditions.
- Does not address analytic continuation or Euler products.
formal statement (Lean)
446theorem zeta_one : zeta 1 = 1 := by
proof body
Term-mode proof.
447 exact zeta_apply (by decide)
448
449/-! ### Values at primes -/
450
451/-- ω(p) = 1 for prime p. -/