sigma_prime
The theorem states that the sum-of-divisors function σ_k applied to any prime p equals exactly 1 plus p raised to the k power. Number theorists evaluating arithmetic functions at prime inputs during Dirichlet series or Euler product calculations would cite this result. The proof converts the Recognition Science Prime predicate to Nat.Prime, unfolds sigma via its explicit divisor sum, and splits the two-element divisor set using insert and singleton rewrites.
claimFor any natural number $k$ and prime number $p$, the sum-of-divisors function satisfies $σ_k(p) = 1 + p^k$.
background
The sum-of-divisors function σ_k is introduced as an abbreviation for ArithmeticFunction.sigma k, with its explicit action given by sigma_apply: σ_k(n) equals the sum of d^k over all positive divisors d of n. The Prime predicate is the Recognition Science wrapper around standard primality, converted via the prime_iff lemma to Nat.Prime. The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to sigma and the constant zeta function (the arithmetic zeta that equals 1 on all positive integers).
proof idea
The term-mode proof first extracts Nat.Prime p from the input hp via prime_iff. It then simplifies sigma k p directly to the divisor sum using sigma_apply and the fact that p has exactly the divisors 1 and p. A non-equality 1 ≠ p is obtained from one_lt, after which the sum is rewritten by inserting the singleton {p} into the divisor set and reducing the remaining singleton sum to 1^k, followed by an application of add_comm.
why it matters in Recognition Science
This supplies the prime case for the sum-of-divisors function inside the arithmetic-functions layer that supports Möbius inversion and Dirichlet convolution in the Recognition Science number-theory module. It furnishes the necessary base evaluation when sigma appears in zeta-function identities or multiplicative decompositions. No downstream uses are recorded yet, but the result closes the prime evaluation step required for any later Euler-product or convolution arguments.
scope and limits
- Does not claim the equality for composite arguments.
- Does not give a closed form for σ_k on prime powers p^m with m > 1.
- Does not address the Möbius function or Dirichlet inversion.
- Does not supply asymptotic estimates or bounds on σ_k.
formal statement (Lean)
209theorem sigma_prime {k : ℕ} {p : ℕ} (hp : Prime p) : sigma k p = 1 + p ^ k := by
proof body
Term-mode proof.
210 have hp' : Nat.Prime p := (prime_iff p).1 hp
211 simp only [sigma_apply, hp'.divisors]
212 have h_ne : (1 : ℕ) ≠ p := hp'.one_lt.ne'.symm
213 rw [Finset.sum_insert (by simp [h_ne]), Finset.sum_singleton, one_pow, add_comm]
214
215/-! ### Zeta function (constant 1) and Dirichlet convolution -/
216
217/-- The arithmetic zeta function ζ (constant 1 on positive integers). -/