practical_twentyfour
plain-language theorem explainer
The sum-of-divisors function satisfies σ₁(24) = 60 which exceeds 24, verifying that 24 is a practical number. Number theorists studying arithmetic functions or practical numbers would reference this verification. The proof is a direct computational evaluation using native_decide on the sigma definition.
Claim. $σ_1(24) ≥ 24$, where $σ_1(n)$ denotes the sum of the positive divisors of the natural number $n$.
background
This module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The sigma abbreviation defines the sum-of-divisors function σ_k as ArithmeticFunction.sigma k. The local setting focuses on basic interfaces for Dirichlet algebra and inversion once stabilized.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the inequality by computing the value of sigma 1 24 directly from its definition as the sum of divisors.
why it matters
This result provides a verified instance for practical numbers within the arithmetic functions module, supporting potential use in number-theoretic aspects of the Recognition Science framework. It depends on the sigma definition in the same file. No immediate downstream theorems reference it, indicating it functions as a standalone check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.