deficient_one
plain-language theorem explainer
The theorem records that the sum-of-divisors function satisfies σ_1(1) < 2. Number theorists classifying deficient numbers cite it as the trivial base case. The proof reduces the concrete inequality to a decidable statement via native decision procedures.
Claim. The sum-of-divisors function satisfies $σ_1(1) < 2·1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The sigma abbreviation is defined directly as sigma (k : ℕ) := ArithmeticFunction.sigma k, recovering the standard sum-of-divisors function σ_k. The local setting is therefore ordinary number-theoretic bookkeeping rather than any Recognition Science construct.
proof idea
The proof is a one-line term that applies native_decide to the numerical inequality σ_1(1) < 2.
why it matters
This supplies the base case for the definition of deficient numbers inside the arithmetic-functions module. No downstream theorems reference it in the current graph, and the declaration does not touch the forcing chain, the phi-ladder, or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.