abundant_thirtysix
plain-language theorem explainer
36 qualifies as abundant since its divisor sum exceeds twice itself. Number theorists studying perfect and abundant numbers cite this explicit case. The proof evaluates the inequality by direct computation.
Claim. $σ_1(36) > 72$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function σ_k. Here sigma 1 n denotes the standard sum of all positive divisors of n. The local setting keeps statements minimal to allow later layering of Dirichlet algebra and inversion once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete numerical inequality directly.
why it matters
This supplies a verified example of an abundant number inside the arithmetic functions module. It fills a small verification step but carries no recorded downstream uses and does not connect to the forcing chain (T0-T8), the Recognition Composition Law, or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.