sigma_zero_onehundredtwenty
plain-language theorem explainer
The declaration establishes that the sum-of-divisors function σ_0 applied to 120 equals 16. Number theorists using the Recognition Science arithmetic functions library would cite this for a verified divisor count at this specific argument. The proof is a one-line native_decide wrapper that evaluates the function directly.
Claim. $σ_0(120) = 16$, where $σ_k$ denotes the sum-of-divisors arithmetic function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting from the Möbius function μ and extending to σ_k. The local sigma is the abbreviation ArithmeticFunction.sigma k, which returns the k-th sum-of-divisors function. This theorem records a concrete evaluation at k=0 and argument 120.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the value of the arithmetic function.
why it matters
This supplies a verified constant for the divisor function inside the arithmetic functions module. It supports the lightweight Dirichlet interface described in the module documentation, though it has no downstream uses yet. The result remains isolated from the J-cost, phi-ladder, and forcing chain steps T5-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.