dirichletOne_def
The declaration establishes that the Dirichlet unit function equals the constant arithmetic function 1. Number theorists applying arithmetic functions to Dirichlet convolution identities would cite this to simplify unit-element reductions. The proof is a direct reflexivity step that matches the abbreviation definition without additional lemmas.
claimThe Dirichlet unit function satisfies $ε = 1$, where $1$ denotes the multiplicative identity in the ring of arithmetic functions.
background
This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and the Dirichlet unit. The Dirichlet unit ε (also written δ_1) is the identity element for Dirichlet convolution: it takes the value 1 at n=1 and 0 at all other positive integers. The abbreviation dirichletOne wraps this unit directly as the constant 1 in the ArithmeticFunction ℤ type.
proof idea
The proof is a term-mode reflexivity step. It applies rfl directly to the defining abbreviation dirichletOne := 1, confirming the equality by definition.
why it matters in Recognition Science
This result supplies the identity element required for the Dirichlet ring structure in the arithmetic-functions interface. It supports later Möbius inversion steps referenced in the module documentation, though no downstream uses are recorded yet. The equality closes the basic definitional layer before deeper algebra is layered on.
scope and limits
- Does not prove any multiplicative or inversion properties of the unit.
- Does not connect to the Möbius function definitions in the same file.
- Does not address analytic continuation or convergence questions.
formal statement (Lean)
251@[simp] theorem dirichletOne_def : dirichletOne = 1 := rfl
proof body
Term-mode proof.
252
253/-- ε(1) = 1. -/