practical_eighteen
plain-language theorem explainer
The sum of divisors function satisfies σ_1(18) ≥ 18, confirming that 18 meets the basic divisor-sum test associated with practical numbers. Number theorists checking small cases of arithmetic inequalities or building libraries of verified divisor properties would reference this result. The proof executes a direct computational check via the native decision procedure.
Claim. $σ_1(18) ≥ 18$, where $σ_1(n)$ is the sum of the 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 local sigma abbreviation is defined as the standard σ_k from Mathlib's ArithmeticFunction.sigma. Upstream results supply the definition of sigma as an ArithmeticFunction ℕ together with the module's emphasis on keeping statements lightweight pending deeper Dirichlet algebra.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the inequality by direct evaluation.
why it matters
This verification supplies a concrete base case inside the arithmetic-functions layer. It has no recorded downstream uses and does not cite any paper proposition or chain step from the Recognition Science forcing sequence. The result remains isolated from T0-T8 landmarks, the Recognition Composition Law, and the phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.