arithId_apply
plain-language theorem explainer
The arithmetic identity function on natural numbers satisfies id(n) = n for every n. Number theorists working with multiplicative functions inside the Recognition Science framework cite this when reducing expressions that contain the identity map. The proof is a one-line simplification that unfolds the definition of the arithmetic identity function.
Claim. For every natural number $n$, the arithmetic identity function evaluated at $n$ equals $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for later Dirichlet algebra. The arithmetic identity function is the canonical map sending each natural number to itself. Upstream results include the multiplicativity theorem for J-automorphisms, which states that such an automorphism preserves multiplication on positive reals.
proof idea
The proof is a one-line wrapper that applies simp to the definition of the arithmetic identity function.
why it matters
This result supplies the basic equality for the arithmetic identity function and prepares its use in multiplicative contexts within the NumberTheory.Primes module. It aligns with the Recognition Science treatment of multiplicative maps under the J-cost algebra and the forcing chain. No open questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.