abundant_twenty
plain-language theorem explainer
20 is verified as abundant by direct computation showing its divisor sum exceeds twice its value. Number theorists cataloging small abundant numbers would cite this concrete check. The proof is a one-line wrapper applying native_decide to evaluate the inequality.
Claim. The sum-of-divisors function satisfies $σ_1(20) > 40$.
background
The ArithmeticFunctions module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to σ_k. The sigma abbreviation is the standard sum-of-divisors function σ_k(n) drawn from Mathlib. The local setting stabilizes basic interfaces before adding Dirichlet algebra or inversion formulas.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete inequality directly.
why it matters
This supplies a verified instance of an abundant number inside the NumberTheory.Primes component. It supports the arithmetic-function primitives used across the module, though no downstream theorems cite it yet. The result fits the framework's incremental build of number-theoretic tools without touching the forcing chain or RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.