sigma_zero_fortyfive
plain-language theorem explainer
The declaration establishes that the divisor counting function σ_0 at 45 returns exactly 6. Researchers using the Recognition Science number theory library for arithmetic function calculations would cite this verified constant. The proof relies on native_decide to evaluate the sum-of-divisors definition directly.
Claim. $σ_0(45) = 6$, where $σ_k(n)$ denotes the sum of the $k$-th powers of the divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function σ_k. The local setting focuses on basic interfaces for Dirichlet algebra and inversion once stabilized.
proof idea
The proof is a one-line term that invokes native_decide to compute the value of sigma 0 45 directly from the definition.
why it matters
This theorem provides a concrete verification of the divisor function at a small integer, supporting the arithmetic functions module in the NumberTheory.Primes section. It fills a basic computational checkpoint without feeding into downstream results in the current graph. No direct tie to the core Recognition Science chain steps such as the J-uniqueness or phi-ladder appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.