arithId_isMultiplicative
The identity arithmetic function id(n) = n is multiplicative. Number theorists working with Dirichlet convolution or inversion formulas cite this as a standard base case. The proof is a one-line term reduction that unfolds the definition and matches Mathlib's built-in multiplicativity result for the identity.
claimLet $id : ℕ → ℕ$ be the function given by $id(n) = n$. Then $id$ is multiplicative: $id(mn) = id(m) ⋅ id(n)$ whenever $m, n$ are coprime natural numbers.
background
Arithmetic functions are maps from natural numbers to numbers that support Dirichlet convolution. The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The identity arithmetic function is defined by id(n) = n. This result confirms its multiplicativity, relying on that definition together with the standard notion of multiplicative functions. The module context prepares for deeper Dirichlet algebra and inversion once basic interfaces stabilize.
proof idea
The proof is a term-mode reduction: it simplifies using the definition of the identity arithmetic function and then directly invokes Mathlib's theorem that the identity arithmetic function is multiplicative.
why it matters in Recognition Science
This establishes the multiplicativity of the identity arithmetic function as a foundational property in the arithmetic functions module. It supports later constructions such as the Möbius function and prime counting. In the Recognition Science framework it supplies a basic number-theoretic tool, though no immediate downstream theorems depend on it.
scope and limits
- Does not prove multiplicativity when arguments are not coprime.
- Does not compute explicit values for specific inputs.
- Does not connect to physical constants or forcing chains.
- Does not generalize beyond natural numbers.
formal statement (Lean)
342theorem arithId_isMultiplicative : ArithmeticFunction.IsMultiplicative arithId := by
proof body
Term-mode proof.
343 simp only [arithId]
344 exact ArithmeticFunction.isMultiplicative_id
345
346/-! ### Prime counting function π -/
347
348/-- The prime counting function π(n) = #{p ≤ n : p prime}. -/