pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

zeta

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 218abbrev zeta : ArithmeticFunction ℕ := ArithmeticFunction.zeta

proof body

Definition body.

 219

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more