sigma_one_threehundredsixty
plain-language theorem explainer
The sum of divisors function satisfies σ_1(360) = 1170. Number theorists and Recognition Science developers working with arithmetic functions cite this for concrete divisor-sum checks during prime factorization work. The proof is a one-line term that invokes native_decide to evaluate the equality by direct computation.
Claim. $σ_1(360) = 1170$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The sigma function here is the standard sum-of-divisors map σ_k(n) = ∑_{d|n} d^k. This theorem records the explicit value at k=1 and n=360. Upstream results supply structures for nuclear densities, σ-charge gaps in decision models, and J-cost factorizations, yet the local setting remains pure computational number theory inside the primes module.
proof idea
The proof is a one-line term wrapper that applies native_decide to the equality sigma 1 360 = 1170.
why it matters
This supplies a verified concrete constant inside the arithmetic-functions layer that supports prime-related calculations in the Recognition framework. It sits among sibling results on the Möbius function and big-Omega and fills a specific instance required by the module's Dirichlet-algebra scaffolding. No downstream uses are recorded yet, and it touches the computational verification step before deeper inversion formulas are layered on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.