sigma_two_six
plain-language theorem explainer
The sum-of-divisors function σ_2 applied to 6 equals 50. Number theorists checking small arithmetic-function values would cite this for direct verification. The proof is a one-line native decision procedure that evaluates the sum from the definition without manual expansion.
Claim. $σ_2(6) = 50$, where $σ_2(n)$ is the sum of $d^2$ over all positive divisors $d$ of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including the sum-of-divisors function. Here sigma is the abbrev that maps k to ArithmeticFunction.sigma k, so sigma 2 6 computes the sum of squares of divisors of 6. The local setting keeps statements minimal before layering Dirichlet algebra. The upstream sigma definition in AbileneParadox concerns agent reporting gaps and is unrelated to this arithmetic sum.
proof idea
The proof is a one-line wrapper that applies native_decide to compute sigma 2 6 directly from the Mathlib definition.
why it matters
This supplies a concrete numerical check for the sigma function inside the NumberTheory.Primes.ArithmeticFunctions module. It supports basic infrastructure for prime-related arithmetic but does not feed any downstream theorems and sits outside the main Recognition Science forcing chain or RCL. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.