practical_sixteen
plain-language theorem explainer
The declaration verifies that the sum-of-divisors function satisfies σ_1(16) ≥ 16. Number theorists checking concrete instances of practical numbers would cite this verification. The proof is a direct native computation that evaluates the divisor sum and the inequality in one step.
Claim. $σ_1(16) ≥ 16$, where $σ_1(n)$ is the sum of all positive divisors of the natural number $n$.
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 sigma abbreviation defines σ_k as ArithmeticFunction.sigma k, the standard sum-of-divisors map. The local setting keeps statements minimal to allow later layering of Dirichlet algebra once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the divisor sum and the inequality directly.
why it matters
This supplies a verified concrete instance confirming the practical-number condition at 16 via the divisor-sum test. It sits inside the arithmetic-functions module that supports prime-related number theory. No downstream uses are recorded and no direct connection appears to the Recognition Science forcing chain or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.