arithId
plain-language theorem explainer
arithId defines the identity arithmetic function on natural numbers satisfying id(n) = n. Number theorists working with multiplicative functions and Dirichlet inversion in Recognition Science cite it as a basic building block. The implementation is a direct one-line alias to the standard identity from the arithmetic function library.
Claim. The identity arithmetic function $id : ArithmeticFunction ℕ$ is defined by $id(n) = n$ for every natural number $n$.
background
This module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function as a foothold for later Dirichlet algebra and inversion. Arithmetic functions here are maps from natural numbers equipped for convolution and multiplicativity checks. The identity is the map returning its input unchanged. Upstream, the identity appears as the identity automorphism in CostAlgebra, the identity homomorphism in ArithmeticOf for Peano objects, and the identity morphism in the Octave structure, each preserving the respective algebraic operations.
proof idea
The declaration is a one-line wrapper that directly aliases ArithmeticFunction.id.
why it matters
It supports the downstream theorems arithId_apply (id(n)=n), arithId_def (simplification rule), and arithId_isMultiplicative (identity is multiplicative). These establish basic arithmetic function properties feeding into prime counting and squarefree analysis. The construction aligns with identity morphisms used in the forcing chain (T0-T8) and octave structures of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.