sigma_one_eighthundredforty
plain-language theorem explainer
The sum-of-divisors function σ_1 evaluates to 2880 at the integer 840. Number theorists using explicit arithmetic-function values inside the Recognition Science number-theory layer would cite this evaluation for concrete divisor-sum checks. The proof is a one-line native_decide computation that directly evaluates the equality.
Claim. $σ_1(840) = 2880$
background
The sigma abbreviation in this module is the standard sum-of-divisors function σ_k, defined as an alias for Mathlib's ArithmeticFunction.sigma k. The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ, while keeping statements minimal until deeper Dirichlet inversion is added. The upstream sigma definition supplies the mathematical content of the sum-of-divisors operator used in the theorem.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the concrete value of σ_1(840) and confirm equality with 2880.
why it matters
This supplies a specific numerical instance of the sum-of-divisors function inside the ArithmeticFunctions module. No downstream theorems are listed as users, so the declaration serves as a ready reference value rather than a lemma feeding a larger chain. It fits the module's role of providing basic arithmetic-function footholds without yet engaging the Recognition forcing chain or constants such as phi or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.