sigma_one_prime
plain-language theorem explainer
The result shows that the sum-of-divisors function at exponent 1 returns p plus one whenever p is prime. Number theorists using arithmetic functions inside the Recognition Science stack would cite the identity when evaluating divisor sums over prime arguments. The argument converts the local primality hypothesis, substitutes the explicit divisor sum via sigma_one_apply, and splits the two-element sum with a single rewrite and commutativity.
Claim. Let $p$ be a prime number. Then the sum-of-divisors function satisfies $σ_1(p) = p + 1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and the sum-of-divisors function σ_k. Here sigma is the abbreviation for ArithmeticFunction.sigma, while sigma_one_apply states that σ_1(n) equals the sum of the divisors of n. Prime is the transparent local alias for Nat.Prime. The proof also draws on the add_comm theorem from the arithmetic-from-logic foundation and the prime_iff conversion between the local and Mathlib primality predicates.
proof idea
The proof first converts the local Prime hypothesis to Nat.Prime via prime_iff. It then applies sigma_one_apply to replace sigma 1 p with the sum over the divisors of p. Because p is prime the divisors are exactly {1, p}, so the sum is split by inserting the singleton for 1 and the singleton for p, followed by an application of add_comm.
why it matters
The identity supplies the base case for evaluating σ over primes and therefore supports later arithmetic-function identities in the same module, including those that will involve the Möbius function. It closes a necessary computational step before Dirichlet inversion or multiplicativity arguments are layered on top. No downstream uses are recorded yet and no open questions are attached to the declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.