sigma_one_onehundredtwenty
plain-language theorem explainer
Verification that the sum-of-divisors function evaluates to 360 at 120 appears here as a basic arithmetic check. Number theorists referencing the Recognition Science library for explicit divisor sums would invoke this equality. Native decision procedures in Lean confirm the result by direct evaluation.
Claim. The sum-of-divisors function satisfies $σ_1(120) = 360$.
background
The ArithmeticFunctions module supplies wrappers around Mathlib's arithmetic functions, with emphasis on the Möbius function μ as a starting point for Dirichlet series and inversion. The sigma abbreviation denotes the sum-of-divisors function σ_k, defined via ArithmeticFunction.sigma k.
proof idea
The proof applies native_decide directly to the equality, allowing the Lean kernel to evaluate the sum of divisors computationally without manual expansion.
why it matters
Placed in the primes arithmetic functions section, this supplies a verified constant for use in larger number-theoretic arguments within Recognition Science. It fills a basic computational slot before more advanced structures like Möbius inversion are developed. No immediate downstream theorems depend on it according to the dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.