abundant_eighteen
plain-language theorem explainer
The theorem establishes that the sum-of-divisors function applied to 18 yields a value strictly larger than 36, confirming 18 as abundant. Number theorists examining arithmetic functions or small abundant numbers would reference this explicit computation. The proof is a direct kernel evaluation via native_decide with no additional lemmas required.
Claim. $σ_1(18) > 2 × 18$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function. The sigma abbreviation is defined as ArithmeticFunction.sigma k, which computes the sum of the k-th powers of the divisors of its argument. The local setting keeps statements minimal so that deeper Dirichlet inversion can be added once the basic interfaces are stable.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete inequality σ_1(18) > 36 directly in the Lean kernel.
why it matters
This declaration supplies a concrete instance of an abundant number inside the arithmetic-functions module. It has no downstream uses recorded in the current graph. It illustrates the sigma function in a setting that may later support number-theoretic steps in the Recognition Science framework, though it touches none of the T0-T8 forcing chain or RCL landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.