zeta
plain-language theorem explainer
The arithmetic zeta function is the constant function taking value 1 on every positive integer. Researchers deriving bounds or conjectures for the Euler-Mascheroni constant and completed Riemann zeta functional equations cite this interface. The declaration is a direct one-line abbreviation of Mathlib's built-in constant-1 arithmetic function.
Claim. The arithmetic zeta function is the map from positive integers to reals given by the constant value 1.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, with the Möbius function as the primary example and deeper Dirichlet inversion deferred. The zeta entry re-exports the standard constant-1 function that appears in Dirichlet series and inversion formulas. No upstream lemmas are required; the definition stands as a direct re-export.
proof idea
One-line wrapper that directly references Mathlib's ArithmeticFunction.zeta.
why it matters
The definition feeds the Euler-Mascheroni numerical bounds, optimality claims, irrationality conjecture, and RS structural prediction that gamma equals a closed form in phi and zeta values. It also supports the logic wrappers that transport the completed Riemann zeta functional equation. Within the framework it supplies the number-theoretic zeta needed for ledger-zeta correspondence and constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.