sigma_three_four
plain-language theorem explainer
σ₃(4) equals 73 as the sum of cubes over the divisors 1, 2, and 4. Number theorists verifying small instances of the sum-of-divisors function would cite this explicit evaluation. The proof is a one-line native decision that computes the divisor sum directly.
Claim. $σ_3(4) = 73$, where $σ_k(n) = ∑_{d∣n} d^k$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local sigma abbreviation reexports ArithmeticFunction.sigma k, the standard sum-of-divisors function. An unrelated sigma definition appears upstream in the AbileneParadox module as an agent preference charge, but the present theorem uses the divisor-sum version.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete arithmetic expression for the divisor sum of 4 under exponent 3.
why it matters
This supplies a verified base case for the sigma function inside the primes arithmetic module. No downstream uses are recorded, so it functions as an isolated check. It supports the module goal of stabilizing basic interfaces before adding Dirichlet algebra or inversion results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.