deficient_nine
plain-language theorem explainer
Verification that 9 is deficient follows from direct computation of the sum-of-divisors function yielding 13, strictly below twice the number. Elementary number theorists examining perfect, abundant, and deficient integers would reference this fact. The proof executes via native decision in the Lean kernel.
Claim. Let $σ_1(n)$ denote the sum of positive divisors of the natural number $n$. Then $σ_1(9) < 18$.
background
The ArithmeticFunctions module supplies small wrappers for Mathlib arithmetic functions, with emphasis on the Möbius function μ as a starting point for Dirichlet inversion. The sigma abbreviation maps each k to the corresponding sum-of-divisors function σ_k, defined via the upstream abbrev that wraps ArithmeticFunction.sigma k.
proof idea
A single application of the native_decide tactic computes the explicit values of the divisors of 9 and verifies the strict inequality.
why it matters
This theorem supplies a concrete instance of a deficient number within the arithmetic functions library. It prepares the ground for potential extensions involving the Möbius function or prime factorizations in the same module, aligning with the lightweight approach described in the module documentation. No immediate parent theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.