sigma_isMultiplicative
The sum-of-divisors function σ_k is multiplicative for every natural number k. Number theorists using Dirichlet convolution or Euler products cite this when reducing divisor sums to prime-power factors. The proof is a one-line wrapper that unfolds the local sigma abbreviation and invokes the corresponding Mathlib fact.
claimFor every natural number $k$, the arithmetic function defined by $σ_k(n) = ∑_{d|n} d^k$ satisfies $σ_k(mn) = σ_k(m)σ_k(n)$ whenever $gcd(m,n)=1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to the sum-of-divisors family. The local definition of sigma is the abbreviation sigma (k : ℕ) := ArithmeticFunction.sigma k, which directly imports the standard sum-of-divisors function. Upstream results include the AbileneParadox sigma (an unrelated agent-report gap) and the UniversalForcingSelfReference structure (a meta-realization certificate), but the relevant dependency for this theorem is the arithmetic sigma abbreviation itself.
proof idea
The term-mode proof first applies simp only [sigma] to replace the local abbreviation with the Mathlib ArithmeticFunction.sigma, then invokes the exact lemma ArithmeticFunction.isMultiplicative_sigma.
why it matters in Recognition Science
This theorem supplies the multiplicativity property required for Euler-product expansions and Dirichlet-series manipulations inside the arithmetic-functions module. The module itself positions these wrappers as Möbius footholds for later inversion formulas. It sits in the NumberTheory.Primes layer that supports the Recognition Science forcing chain by furnishing standard multiplicative tools without introducing new hypotheses.
scope and limits
- Does not establish multiplicativity for functions outside the sigma family.
- Does not compute explicit values of σ_k at prime powers.
- Does not address any physical or Recognition-Science interpretation of the divisor sum.
- Does not extend the result to non-coprime arguments.
formal statement (Lean)
190theorem sigma_isMultiplicative (k : ℕ) : ArithmeticFunction.IsMultiplicative (sigma k) := by
proof body
Term-mode proof.
191 simp only [sigma]
192 exact ArithmeticFunction.isMultiplicative_sigma
193
194/-- σ_0(p) = 2 for prime p. -/