deficient_eight
plain-language theorem explainer
The declaration verifies that the sum-of-divisors function applied to 8 is strictly less than 16, confirming 8 as deficient. Number theorists examining concrete cases of abundance and deficiency would cite this instance. The proof is a one-line native decision that evaluates the inequality directly.
Claim. $σ_1(8) < 2 × 8$, where $σ_1$ denotes the sum-of-divisors function.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ. The sigma abbreviation defines the sum-of-divisors function σ_k as ArithmeticFunction.sigma k. The local setting keeps statements minimal so that deeper Dirichlet algebra and inversion can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the concrete inequality σ_1(8) < 16 directly.
why it matters
This supplies a verified deficient-number instance inside the arithmetic-functions library. It supports later work on prime-related divisor sums and Möbius inversion within the NumberTheory.Primes hierarchy. The module doc indicates that such basic facts prepare the ground for Dirichlet inversion once the interfaces are stable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.