sigma_two_eight
plain-language theorem explainer
The theorem asserts that the sum-of-divisors function σ₂ applied to 8 equals 85. Number theorists checking concrete values of arithmetic functions in the Recognition Science setting would cite this for small-integer verification. The proof is a direct one-line native_decide evaluation that computes the divisor sum at compile time.
Claim. $σ_2(8) = 85$, where $σ_k(n)$ denotes the sum of $d^k$ over all positive divisors $d$ of $n$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function and extending to the sum-of-divisors function. The sibling definition sigma is the abbreviation sigma (k : ℕ) : ArithmeticFunction ℕ := ArithmeticFunction.sigma k, so that sigma k n computes the sum of d^k for d dividing n. The local setting is a collection of basic interfaces for Dirichlet algebra and inversion, kept minimal until the core definitions stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the numerical equality directly.
why it matters
This supplies a verified concrete instance for σ₂(8) inside the arithmetic functions module, supporting later layering of Möbius inversion and prime-related computations. It fills a small base case in the NumberTheory.Primes hierarchy without invoking upstream results from the forcing chain or Recognition Composition Law. No downstream uses are recorded yet, leaving open whether it will anchor larger identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.