deficient_four
plain-language theorem explainer
The theorem verifies that the sum of positive divisors of 4 equals 7 and is strictly less than 8. Elementary number theorists would cite it as a concrete base case when listing small deficient integers. The proof is a one-line computational check that evaluates the inequality directly.
Claim. $σ_1(4) < 8$, where $σ_1(n)$ denotes 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 defining sigma k as the abbreviation for the sum-of-divisors function ArithmeticFunction.sigma k. A number n is deficient when sigma 1 n is less than twice n. The local setting keeps statements minimal ahead of Dirichlet algebra or inversion results.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the concrete numerical inequality sigma 1 4 < 2 * 4.
why it matters
It supplies a verified base case inside the arithmetic functions module that supports later prime-related constructions. No downstream theorems depend on it, and it does not engage the Recognition Science forcing chain, RCL, or phi-ladder. The declaration stabilizes a basic interface without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.