abundant_twentyfour
plain-language theorem explainer
The declaration shows that the sum-of-divisors function at 24 yields a value strictly larger than 48, establishing 24 as an abundant number in the arithmetic functions library. Researchers verifying small cases of abundant numbers in number-theoretic foundations would cite this result. The proof reduces to a direct computational check via native decision procedures.
Claim. $σ_1(24) > 48$
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function and including the sum-of-divisors function σ_k defined as an abbreviation for ArithmeticFunction.sigma k. This theorem operates in the context of providing basic number-theoretic facts for prime-related arithmetic. Upstream, the sigma abbreviation supplies the sum-of-divisors operator used here.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the inequality directly.
why it matters
This result supplies a verified instance of an abundant number within the NumberTheory.Primes.ArithmeticFunctions module, supporting downstream calculations involving divisor sums. It aligns with the framework's emphasis on concrete arithmetic verifications that can feed into larger structures such as the phi-ladder or mass formulas, though no direct link is established here. No open questions are touched as the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.