sigma_three_three
plain-language theorem explainer
The declaration establishes that the sum-of-divisors function σ_3 applied to 3 equals 28. Number theorists verifying small cases of arithmetic functions before Möbius inversion would cite this explicit evaluation. The proof is a one-line wrapper that applies native_decide to evaluate the finite sum of cubes over the divisors.
Claim. $1^3 + 3^3 = 28$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to the sum-of-divisors function. The local setting keeps statements minimal so that deeper Dirichlet algebra and inversion can be added once basic interfaces stabilize. The sigma abbreviation defines σ_k(n) as the standard sum of d^k over positive divisors d of n.
proof idea
The proof is a one-line wrapper that invokes native_decide to compute the sum directly from the definition of sigma.
why it matters
This supplies a concrete numerical check for the arithmetic-function layer that precedes Möbius-based results in the same module. It has no listed dependents, so its role is foundational verification rather than a step in the forcing chain or phi-ladder. The computation aligns with the module's goal of stabilizing basic interfaces before connecting to Recognition Science structures such as the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.