practical_eight
plain-language theorem explainer
σ₁(8) ≥ 8 holds by direct computation, marking 8 as practical under the divisor-sum criterion used here. Number theorists checking base cases for practical numbers within Recognition Science arithmetic interfaces would cite this result. The proof is a one-line native_decide wrapper that evaluates the sum-of-divisors function exactly and confirms the inequality.
Claim. The sum-of-divisors function satisfies $σ_1(8) ≥ 8$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for later Dirichlet work. Sigma is the abbreviation sigma (k : ℕ) := ArithmeticFunction.sigma k, which computes the sum of the k-th powers of the divisors of its argument. The local setting keeps statements minimal while the basic interfaces stabilize.
proof idea
The proof is a term-mode one-liner that invokes native_decide on the concrete inequality sigma 1 8 ≥ 8. The tactic evaluates the arithmetic function at the given arguments and discharges the comparison by computation, with no named lemmas required beyond the sigma definition.
why it matters
This supplies a verified numerical base fact inside the arithmetic-functions module, supporting number-theory scaffolding before inversion or prime-distribution results are layered on. It has no downstream citations in the current graph and does not touch the forcing chain, phi-ladder, or Recognition constants, but it closes a concrete check aligned with the module's stated goal of stabilizing lightweight interfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.