practical_twenty
plain-language theorem explainer
The sum-of-divisors function satisfies σ₁(20) ≥ 20, confirming 20 as practical under the criterion applied in this arithmetic setting. Number theorists verifying small cases of practical numbers or divisor sums would cite the result. The proof is a one-line wrapper that invokes native_decide to evaluate the inequality directly.
Claim. $σ_1(20) ≥ 20$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to the sum-of-divisors function. The sibling definition sigma (k : ℕ) is the abbreviation sigma (k : ℕ) : ArithmeticFunction ℕ := ArithmeticFunction.sigma k, which implements the standard σ_k. The local theoretical setting keeps statements minimal so that Dirichlet inversion and deeper algebra can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to compute σ_1(20) and confirm the inequality holds.
why it matters
This concrete check populates the arithmetic-functions module that supplies number-theoretic primitives for the Recognition Science framework. It supplies a verified instance of the divisor-sum criterion used to identify practical numbers, consistent with the lightweight-interface approach stated in the module documentation. No downstream theorems depend on it, so it functions as a terminal verification rather than a link in the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.