sigma_three_two
plain-language theorem explainer
The sum-of-divisors function satisfies σ_3(2) = 9 by adding the cubes of the divisors of 2. Number theorists building arithmetic-function interfaces inside Recognition Science would cite this as a verified base case. The proof is a one-line native_decide tactic that evaluates the definition directly.
Claim. Let $σ_k(n)$ denote the sum of the $k$th powers of the positive divisors of $n$. Then $σ_3(2) = 9$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and including the sum-of-divisors function. The sigma abbreviation defines σ_k as ArithmeticFunction.sigma k, which computes the sum of d^k over d dividing n. This theorem verifies a specific small case in that setting, consistent with the module's focus on basic interfaces before deeper Dirichlet algebra.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to reduce the equality to a decidable computation of the divisor sum.
why it matters
This equality supplies a concrete verification step inside the arithmetic-functions layer of NumberTheory.Primes, which the module positions as Möbius footholds for later inversion work. It does not engage the forcing chain, RCL, or physical constants, but stabilizes the basic interface the module requires before layering further results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.