sigma_two_three
plain-language theorem explainer
The equality σ₂(3) = 10 holds by direct evaluation of the sum-of-divisors function at n=3. Number theorists using arithmetic functions would cite this as a basic numerical checkpoint. The proof is a one-line wrapper that invokes a decision procedure to compute the value from the definition.
Claim. $σ_2(3) = 10$, where $σ_k(n) = ∑_{d|n} d^k$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ as a foothold for later Dirichlet inversion. The sigma abbreviation defines the sum-of-divisors function σ_k via the standard Mathlib interface. The upstream sigma definition states that σ_k(n) sums d^k over all positive divisors d of n.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic function definition directly.
why it matters
This theorem supplies a concrete numerical value for σ₂(3) inside the arithmetic functions module. It supports elementary calculations in the number-theoretic layer of the Recognition framework, though it does not connect to the forcing chain T0-T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.