deficient_ten
plain-language theorem explainer
The sum of divisors function satisfies σ_1(10) = 18 which is strictly less than 20, confirming that 10 is deficient. Number theorists classifying perfect, deficient and abundant numbers would cite this as a basic verification instance. The proof is a one-line native decision procedure that evaluates the concrete inequality directly.
Claim. Let $σ_1(n)$ denote the sum of the positive divisors of $n$. Then $σ_1(10) < 2 · 10$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The divisor sum function σ_k(n) is the sum of d^k over all positive divisors d of n; the case k=1 recovers the standard sum-of-divisors function. The local setting is a collection of small interfaces that stabilize basic arithmetic-function notation before deeper Dirichlet inversion is layered on.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the concrete numerical inequality directly.
why it matters
This supplies a basic verified instance of a deficient number inside the arithmetic-functions module. It supports downstream classification work on perfect and abundant numbers, though no parent theorems are recorded in the used-by graph. The result sits among the lightweight footholds that precede Möbius-based inversion statements in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.