sigma_one_three_pow_one
plain-language theorem explainer
The sum-of-divisors function evaluates to σ_1(3) = 4. Number theorists verifying elementary cases of arithmetic functions or building small test suites would cite this result. The proof applies the native_decide tactic to compute the divisor sum directly.
Claim. $σ_1(3) = 4$, where $σ_k(n)$ denotes the sum of the $k$-th powers of all positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function. The local sigma is defined as the abbreviation sigma (k : ℕ) := ArithmeticFunction.sigma k, which returns the function that maps n to the sum of d^k over d dividing n. This sits in the same file as Möbius definitions to support later Dirichlet algebra and inversion steps.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate sigma 1 (3^1) by direct computation of the divisor sum.
why it matters
This supplies a basic verification for the arithmetic functions library that the module positions as Möbius footholds. No downstream results depend on it, so it functions as an isolated sanity check rather than a link in a larger chain. It does not reference the forcing chain, phi-ladder, or Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.