sigma
plain-language theorem explainer
sigma defines the sum-of-divisors arithmetic function σ_k on the naturals. Number theorists and Recognition Science developers cite it when divisor sums appear in cost algebras or arithmetic encodings. The implementation is a one-line wrapper that directly aliases Mathlib's ArithmeticFunction.sigma.
Claim. For each natural number $k$, the arithmetic function $σ(k)$ sends $n$ to the sum of the $k$-th powers of the positive divisors of $n$, that is $σ(k)(n) = ∑_{d∣n} d^k$.
background
The module supplies small wrappers around Mathlib's arithmetic function library, starting with the Möbius function μ (spelled ArithmeticFunction.moebius in code). We keep the statements lightweight here; deeper Dirichlet algebra and inversion can be layered on once the basic interfaces stabilize.
proof idea
This is a one-line wrapper that applies ArithmeticFunction.sigma from Mathlib.
why it matters
This supplies the sigma component for canonicalRecognitionCostSystem in Algebra.CostAlgebra, which constructs the canonical recognition cost system (ℝ₊, J, σ, W). It also supports the RecognitionCostSystem structure that packages a ratio cost, a conservation functional, and a finite window length. Within the Recognition framework it furnishes arithmetic primitives for prime-related computations, though no explicit tie to the forcing chain or RCL appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.