sigma_two_ten
plain-language theorem explainer
The declaration establishes that the sum of the squares of the positive divisors of 10 equals 130. Number theorists building arithmetic function libraries would cite it as a verified base case for divisor sums. The proof is a one-line term that applies native_decide to evaluate the sum directly from the definition.
Claim. Let $n$ be a positive integer and let $k$ be a nonnegative integer. Define $d_k(n)$ as the sum of the $k$th powers of all positive divisors of $n$. Then $d_2(10) = 130$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function. The relevant upstream definition is the abbreviation sigma (k : ℕ) that maps to ArithmeticFunction.sigma k, which computes the sum of kth powers of divisors. The unrelated sigma from the AbileneParadox module tracks reporting gaps for agents and plays no role here. The local setting keeps statements minimal to support later Dirichlet inversion once basic interfaces stabilize.
proof idea
The proof is a one-line term that invokes native_decide to compute the divisor sum for 10 and confirm equality with 130.
why it matters
This concrete computation anchors the arithmetic-functions layer inside NumberTheory.Primes, which supplies Möbius footholds for inversion formulas. It supplies a checked base case that downstream prime-arithmetic results can reference without recomputation. No direct tie exists to the Recognition Science forcing chain or RCL, yet the fact contributes to the number-theoretic scaffolding required for consistent arithmetic operations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.