sigma_prime
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.