sigma_three_one
plain-language theorem explainer
σ_3(1) evaluates to 1 under the sum-of-divisors function. Number theorists cite this as the trivial base case when inducting on positive integers or applying identities for divisor sums. The proof is a one-line wrapper that invokes native_decide to evaluate the definition directly.
Claim. $σ_3(1) = 1$, where $σ_k(n)$ denotes the sum of the $k$th powers of the positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The sigma abbreviation defines the sum-of-divisors function σ_k via ArithmeticFunction.sigma k. The upstream sigma definition in the same module confirms this computes the divisor sum, while the unrelated sigma from Decision.AbileneParadox represents a decision-theory charge and plays no role here.
proof idea
The proof is a one-line wrapper that applies native_decide to compute sigma 3 1 directly from the arithmetic-function definition.
why it matters
This supplies the base case for σ_3 in the arithmetic-functions module supporting prime and squarefree results. It fills a concrete verification step in the number-theory footholds without linking to the forcing chain, RCL, or phi-ladder. No downstream theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.