dirichletOne_one
The Dirichlet unit function ε satisfies ε(1) = 1 by direct evaluation from its definition. Number theorists working with Dirichlet convolution cite this as the base case for the multiplicative identity in the arithmetic functions ring. The proof is a one-line simplification that unfolds the definition of dirichletOne.
claimLet ε denote the Dirichlet unit function. Then ε(1) = 1.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ and the Dirichlet unit ε. Local setting is the ring of arithmetic functions under Dirichlet convolution, where ε serves as the multiplicative identity. Upstream, dirichletOne is the abbrev wrapping ε = δ_1, the function that equals 1 at argument 1.
proof idea
The proof is a one-line wrapper that applies simp on the definition of dirichletOne.
why it matters in Recognition Science
This closes the base case for the Dirichlet unit inside the arithmetic functions module. It supports later Dirichlet inversion and convolution work in the NumberTheory layer of Recognition Science. No downstream uses are recorded yet, leaving the unit property available for extension.
scope and limits
- Does not prove the convolution identity ε * f = f for arbitrary arithmetic f.
- Does not evaluate ε(n) for any n > 1.
- Does not link to Möbius inversion formulas in the same module.
formal statement (Lean)
254theorem dirichletOne_one : dirichletOne 1 = 1 := by
proof body
Term-mode proof.
255 simp [dirichletOne]
256
257/-- ε(n) = 0 for n > 1. -/