sigma_zero_prime
plain-language theorem explainer
sigma_zero_prime asserts that the zero-order divisor sum equals two on any prime. Number theorists in the Recognition Science arithmetic layer would cite this when establishing base cases for multiplicative functions or divisor counts on the phi-ladder. The argument reduces the claim to the explicit divisors of a prime via sigma_zero_apply and concludes the cardinality is two by applying the singleton and insert lemmas.
Claim. For every prime number $p$, the divisor function satisfies $sigma_0(p)=2$.
background
The module supplies lightweight wrappers for arithmetic functions, beginning with the Möbius function and the sum-of-divisors family. sigma is the abbreviation for Mathlib's ArithmeticFunction.sigma k, while sigma_zero_apply records that sigma 0 n equals the cardinality of the divisors of n. The local Prime abbreviation is the standard Nat.Prime predicate. Upstream, card_singleton states that a singleton Finset has cardinality one.
proof idea
The term proof first applies prime_iff to obtain the Mathlib Nat.Prime instance. It then simplifies via sigma_zero_apply to replace the left side with the divisor cardinality, notes that 1 differs from p, and rewrites the cardinality of the insert of p into the singleton {1} using card_insert_of_notMem together with card_singleton.
why it matters
This identity anchors the arithmetic-function layer in the primes module, which prepares Möbius inversion and divisor sums for use in Recognition Science mass formulas and square-free checks. It directly extends sigma_zero_apply and the Prime definition, closing a basic case that later results on multiplicative functions can build upon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.