sigma_three_eight
plain-language theorem explainer
The sum-of-divisors function σ_3 evaluated at 8 equals 585. Number theorists building explicit arithmetic tables in the Recognition Science number-theory layer would cite this for verification of small cases. The proof is a direct computational check via native decision procedure.
Claim. $σ_3(8) = 585$, where $σ_k(n)$ denotes the sum of the $k$th powers of the positive divisors of $n$.
background
The sigma function is defined locally as an abbreviation for Mathlib's ArithmeticFunction.sigma k, giving the standard sum-of-divisors function $σ_k(n) = ∑_{d|n} d^k$. The module supplies lightweight wrappers around arithmetic functions, beginning with the Möbius function μ, to support later Dirichlet inversion once interfaces stabilize. The upstream sigma declaration in Decision.AbileneParadox defines an unrelated σ-charge for agent reporting, while the local abbrev supplies the number-theoretic version used here.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the finite sum of cubes over the divisors of 8.
why it matters
This supplies an explicit base case for the arithmetic-functions module that opens the NumberTheory.Primes layer and its Möbius footholds. No downstream theorems currently depend on it, so it functions as a verified computational anchor rather than a link in a larger chain. Within Recognition Science it remains isolated from the forcing chain T0-T8, the Recognition Composition Law, and the phi-ladder, serving only as a sanity check on the imported sigma definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.