sigma_two_thirty
plain-language theorem explainer
The sum-of-divisors function σ₂ evaluated at 30 equals 1300. Number theorists checking explicit arithmetic values at small round integers would cite this for verification. The proof is a one-line native computation that evaluates the divisor sum directly.
Claim. $σ_2(30) = 1300$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and including the sum-of-divisors function σ_k. The abbreviation sigma k stands for ArithmeticFunction.sigma k, which returns the function that sums the k-th powers of the divisors of its argument. This theorem records the concrete case k=2, n=30. The local setting is small explicit values supporting prime counting; upstream primeCounting is defined as Nat.primeCounting n. The sigma definition from AbileneParadox addresses an unrelated agent σ-charge and is not used here.
proof idea
The proof is a one-line native_decide that evaluates the sum-of-divisors function directly at the supplied arguments.
why it matters
This supplies an explicit numerical check for σ₂(30) inside the arithmetic functions module that underpins prime counting. It fills a role in the NumberTheory.Primes section by providing round-number values, though it does not connect to the Recognition Science forcing chain, J-uniqueness, phi-ladder, or constants such as phi^5. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.