sigma_two_four
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 in Recognition Science
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.
scope and limits
- Does not derive general properties of σ_k.
- Does not link to physical constants or dimensions.
- Does not involve the J-function or RCL.
formal statement (Lean)
1651theorem sigma_two_four : sigma 2 4 = 21 := by native_decide
proof body
Term-mode proof.
1652
1653/-- σ_2(5) = 1 + 25 = 26. -/