abundant_thirty
plain-language theorem explainer
30 is shown to be abundant since its divisor sum σ_1(30) equals 72, exceeding 60. Researchers in number-theoretic aspects of Recognition Science would reference this concrete verification. The proof relies on a direct native_decide evaluation of the inequality.
Claim. The sum-of-divisors function satisfies $σ_1(30) > 60$, where $σ_1(n)$ is the sum of positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The sigma abbreviation maps k to ArithmeticFunction.sigma k, yielding the sum-of-divisors function σ_k. The local setting keeps statements minimal so that Dirichlet algebra and inversion can be added once basic interfaces stabilize.
proof idea
one-line wrapper that applies native_decide
why it matters
This supplies a verified instance of an abundant integer inside the arithmetic-functions module. It supports the module's role as a foothold for Möbius-based number theory within Recognition Science, though no downstream theorems currently cite it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.