sigma_three_six
plain-language theorem explainer
The declaration verifies that the sum of cubes of the positive divisors of 6 equals 252. Number theorists checking arithmetic function implementations or building small verification suites would cite this as a concrete numerical anchor. The proof is a one-line wrapper that applies native_decide to evaluate the sum directly from the definition.
Claim. $σ_3(6) = 252$, where $σ_k(n) = ∑_{d|n} d^k$ denotes the sum of the $k$th powers of the positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function and extending to the sum-of-divisors function. The local sigma abbrev is defined as ArithmeticFunction.sigma k, matching the standard σ_k. This sits inside the NumberTheory.Primes.ArithmeticFunctions section whose module doc states the intent to keep statements lightweight before layering Dirichlet algebra and inversion.
proof idea
The proof is a one-line wrapper that invokes native_decide to compute the sum of cubes over the divisors of 6 and confirm equality with 252.
why it matters
This supplies a basic numerical identity for the sum-of-divisors function inside the arithmetic functions module. It supports the module's goal of stabilizing basic interfaces, though no immediate downstream uses are recorded. It aligns with the surrounding focus on primes and squarefree numbers without touching the Möbius inversion machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.