arithId_def
plain-language theorem explainer
The declaration equates the custom arithmetic identity function to Mathlib's standard identity on natural numbers. Researchers handling Möbius inversion or Dirichlet convolution in the Recognition framework cite this to ensure consistency with library primitives. The proof reduces to a reflexivity application after unfolding the abbreviation.
Claim. The identity arithmetic function on natural numbers satisfies $id(n) = n$ for all $n$, where the custom definition coincides exactly with the standard identity arithmetic function.
background
This module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function to stabilize basic interfaces before deeper Dirichlet algebra. The identity serves as the base case for convolution. Upstream, the identity appears in CostAlgebra as the identity automorphism (the map sending each element to itself) and in ArithmeticOf as the identity homomorphism on Peano objects, with the local arithmetic identity defined to match $id(n) = n$.
proof idea
The proof is a one-line wrapper that applies reflexivity to the abbreviation definition of the custom identity arithmetic function.
why it matters
This equality anchors the arithmetic functions module and supports the Möbius function constructions that follow. It aligns custom definitions with standard number theory tools in the Recognition Science framework, though it invokes no direct step from the T0-T8 forcing chain. No open questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.