sigma_three_four
σ₃(4) equals 73 as the sum of cubes over the divisors 1, 2, and 4. Number theorists verifying small instances of the sum-of-divisors function would cite this explicit evaluation. The proof is a one-line native decision that computes the divisor sum directly.
claim$σ_3(4) = 73$, where $σ_k(n) = ∑_{d∣n} d^k$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local sigma abbreviation reexports ArithmeticFunction.sigma k, the standard sum-of-divisors function. An unrelated sigma definition appears upstream in the AbileneParadox module as an agent preference charge, but the present theorem uses the divisor-sum version.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete arithmetic expression for the divisor sum of 4 under exponent 3.
why it matters in Recognition Science
This supplies a verified base case for the sigma function inside the primes arithmetic module. No downstream uses are recorded, so it functions as an isolated check. It supports the module goal of stabilizing basic interfaces before adding Dirichlet algebra or inversion results.
scope and limits
- Does not prove any general identity for σ_k(n).
- Does not invoke or relate to the Möbius function.
- Does not connect to Recognition Science forcing chains or physical constants.
- Does not handle composite numbers beyond this specific case.
formal statement (Lean)
1838theorem sigma_three_four : sigma 3 4 = 73 := by native_decide
proof body
Term-mode proof.
1839
1840/-- σ_3(5) = 1 + 125 = 126. -/