sigma_zero_eight
plain-language theorem explainer
Sigma_0(8) evaluates to 4 under the sum-of-divisors definition. Number theorists checking small divisor counts reference this as a verified instance. Native decision computes the result directly from the function definition.
Claim. $sigma_0(8) = 4$
background
The module supplies lightweight wrappers for arithmetic functions from Mathlib, beginning with the Möbius function and extending to the sum-of-divisors function. Sigma is defined as the sum-of-divisors function sigma_k, the sum of d^k over divisors d of n. The local theoretical setting focuses on Möbius footholds for building Dirichlet algebra later.
proof idea
The proof is a one-line wrapper that invokes native_decide to compute the value of the arithmetic function directly.
why it matters
This supplies a concrete base case for the divisor function sigma_0(8)=4 within the arithmetic functions module. It supports potential downstream uses in prime-related calculations though no direct dependents are listed. It aligns with the framework's use of number-theoretic tools to underpin Recognition Science derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.