sigma_zero_threehundredsixty
plain-language theorem explainer
The sum-of-divisors function at exponent zero applied to 360 equals 24. Number theorists working with divisor counts or arithmetic functions would cite this identity when handling highly composite integers. The proof is a direct computational check via native decision that evaluates the divisor sum exactly.
Claim. $σ_0(360) = 24$, where $σ_0(n)$ denotes the number of positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and extending to the sum-of-divisors function. The relevant sigma is the abbrev sigma (k : ℕ) : ArithmeticFunction ℕ := ArithmeticFunction.sigma k, so that sigma 0 n computes the divisor count of n. The upstream sigma definition in AbileneParadox concerns a separate σ-charge for decision agents and plays no role in this arithmetic statement.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the value of the arithmetic function directly.
why it matters
This supplies a verified numerical identity for the divisor count of 360 inside the arithmetic-functions module. It supports potential downstream use of exact divisor sums or Möbius inversion steps, though no parent theorems currently depend on it. The result sits among the basic footholds that keep the number-theory layer ready for any Recognition Science calculations that require precise arithmetic identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.