sigma_three_ten
plain-language theorem explainer
The sum-of-divisors function σ_3 evaluated at 10 equals 1134. Number theorists using arithmetic functions for small-case checks or Möbius inversion setups would cite this equality. The proof is a one-line native decision that evaluates the sum of cubes over the divisors of 10 directly from the definition.
Claim. The sum of the cubes of the positive divisors of 10 equals 1134.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function σ_k. Here sigma is the abbreviation sigma (k : ℕ) := ArithmeticFunction.sigma k, so sigma 3 10 computes ∑_{d|10} d^3. The upstream sigma definition in the same module records this as the standard sum-of-divisors function; the AbileneParadox sigma is unrelated and concerns agent reporting gaps.
proof idea
One-line wrapper that applies native_decide to compute the explicit sum 1^3 + 2^3 + 5^3 + 10^3.
why it matters
This supplies a concrete numerical anchor for the sigma abbreviation inside the arithmetic-functions module, which the module doc positions as a foothold for Möbius inversion. It sits downstream of the sigma definition and supports any later Dirichlet-series or inversion arguments that require verified small values. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.