practical_thirty
plain-language theorem explainer
The sum-of-divisors function satisfies σ₁(30) = 72 ≥ 30. Number theorists checking concrete cases of practical numbers would cite this verification. The proof is a direct computation via native_decide that evaluates the inequality without intermediate lemmas.
Claim. $σ_1(30) ≥ 30$, where $σ_1(n)$ is the sum of the positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and including the sum-of-divisors function. The sibling definition sigma (k : ℕ) is the standard ArithmeticFunction.sigma k, so sigma 1 30 denotes σ₁(30). The local setting is basic number-theoretic scaffolding for later Dirichlet algebra; the present theorem checks the divisor-sum inequality that appears in the definition of practical numbers.
proof idea
One-line wrapper that applies native_decide to evaluate σ₁(30) = 72 and confirm the comparison 72 ≥ 30.
why it matters
The declaration supplies a concrete verified instance inside the arithmetic-functions module. It rests on the sigma abbreviation defined in the same file and supports incremental checks toward practical-number statements. No downstream results are recorded, indicating it functions as a basic sanity check rather than a lemma feeding larger theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.