sigma_two_four
plain-language theorem explainer
sigma_two_four asserts that σ₂(4) equals 21. Researchers verifying arithmetic function implementations in this library would reference it for base cases. The proof reduces to a single native_decide tactic that evaluates the divisor sum directly.
Claim. $σ_2(4) = 21$ where $σ_k(n) := ∑_{d|n} d^k$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ. The sigma abbreviation denotes the sum-of-divisors function σ_k. An upstream definition from AbileneParadox introduces a distinct σ-charge for agent reports, but the local sigma handles divisor sums. The setting keeps statements minimal pending deeper Dirichlet algebra.
proof idea
native_decide evaluates the arithmetic expression for σ_2(4) = 1 + 4 + 16 by direct computation.
why it matters
This theorem provides a concrete instance in the arithmetic functions module that supports Möbius footholds. It has no downstream uses yet, serving as a basic check rather than advancing the forcing chain or phi-ladder directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.