sigma_zero_twelve
plain-language theorem explainer
The declaration verifies that the divisor counting function σ_0(12) equals 6, matching the six positive divisors of 12. Number theorists extending arithmetic function tools in the Recognition Science setting would cite this as a concrete sanity check on the sigma definition. The proof is a direct native_decide term that evaluates the expression in the Lean kernel without further lemmas.
Claim. $σ_0(12) = 6$, where $σ_k(n)$ denotes the sum of the $k$th powers of the positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ and including the sum-of-divisors function σ_k. The local sigma abbreviation is defined as sigma (k : ℕ) := ArithmeticFunction.sigma k, so that σ_0(n) simply counts the divisors of n. This file prepares basic interfaces for later Dirichlet algebra and inversion steps, as noted in the module header.
proof idea
The proof is a one-line term that invokes native_decide to compute sigma 0 12 directly.
why it matters
This equality anchors the arithmetic functions layer before Möbius and squarefree properties are developed. It confirms the sigma definition behaves as expected for small arguments in the NumberTheory.Primes.ArithmeticFunctions file. No downstream uses appear yet, so the result functions as foundational scaffolding for potential prime-related calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.