zeta_mul_moebius
The arithmetic identity ζ ⋅ μ = ε holds in the ring of integer-valued arithmetic functions, where ζ is the constant-1 function and μ the Möbius function. Researchers applying Möbius inversion to sums over divisors would invoke this relation as the starting point. The proof proceeds by direct unfolding of the local abbreviations for zeta and mobius followed by an exact match to the corresponding Mathlib coefficient identity.
claim$ζ ⋅ μ = ε$ in the ring of arithmetic functions over $ℤ$, where $ζ(n) = 1$ for all positive integers $n$, $μ$ denotes the Möbius function, and $ε$ is the Dirichlet unit with $ε(1) = 1$ and $ε(n) = 0$ for $n > 1$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ defined as an abbreviation for ArithmeticFunction.moebius. The zeta function is introduced as the constant function 1 on positive integers. Upstream, the identity event is characterized as the canonical point of zero J-cost at state 1, providing the algebraic unit ε = δ_1 in this context. The local setting keeps statements minimal to allow layering of Dirichlet algebra once interfaces stabilize.
proof idea
The term proof first simplifies using the definitions of mobius and zeta, then applies the exact Mathlib result ArithmeticFunction.coe_zeta_mul_moebius that verifies the product equals the unit function coefficient-wise.
why it matters in Recognition Science
This identity is the algebraic foundation for Möbius inversion in number theory and supplies the unit element needed for the ring structure of arithmetic functions. It connects to the Recognition framework's emphasis on the identity event as the J-cost minimum. No immediate downstream uses are recorded, but it supports potential extensions to Dirichlet series and inversion formulas within the NumberTheory.Primes hierarchy. It touches the open question of integrating full arithmetic function theory with the forcing chain (T0-T8).
scope and limits
- Does not establish convergence properties of associated Dirichlet series.
- Does not derive the explicit formula for the Möbius function on prime powers.
- Does not address generalizations to other rings or semigroups.
- Does not prove the Möbius inversion theorem itself.
formal statement (Lean)
244theorem zeta_mul_moebius : (↑zeta : ArithmeticFunction ℤ) * mobius = 1 := by
proof body
Term-mode proof.
245 simp only [mobius, zeta]
246 exact ArithmeticFunction.coe_zeta_mul_moebius
247
248/-- For the identity (Dirichlet unit), we wrap ε = δ_1. -/