arithId_def
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute explicit values on composite inputs.
- Does not incorporate the Möbius function or inversion formulas.
- Does not address analytic properties such as Dirichlet series.
formal statement (Lean)
335@[simp] theorem arithId_def : arithId = ArithmeticFunction.id := rfl
proof body
Term-mode proof.
336
337/-- id(n) = n. -/