deficient_five
plain-language theorem explainer
The declaration verifies that the sum-of-divisors function applied to 5 returns a value strictly below twice 5, establishing 5 as deficient. Elementary number theorists building libraries of arithmetic functions would reference this computational check. The proof proceeds as a direct native decision that evaluates the inequality without expansion or lemmas.
Claim. $σ_1(5) < 2 × 5$
background
The ArithmeticFunctions module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function and keeping statements minimal for later Dirichlet layering. The sigma abbreviation defines the sum-of-divisors function σ_k as ArithmeticFunction.sigma k. This theorem uses that definition to check a concrete case of deficiency.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the inequality directly.
why it matters
This theorem supplies a basic verified instance inside the arithmetic functions scaffolding. It supports stabilization of the basic interfaces described in the module documentation before deeper algebraic work is added. No downstream uses are recorded, and the result does not touch Recognition Science landmarks such as the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.