deficient_two
plain-language theorem explainer
Sigma_1 applied to 2 yields 3, which is strictly less than 4, confirming that 2 is deficient. Number theorists building arithmetic-function properties inside the Recognition Science framework cite this as a base case for small primes. The verification is a direct computational check via native_decide.
Claim. $σ_1(2) < 4$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and the sum-of-divisors function. The abbreviation sigma k denotes σ_k, the arithmetic function that sums d^k over all positive divisors d of its argument. The local setting is therefore the elementary layer of Dirichlet arithmetic before inversion formulas or deeper Recognition Science structures are introduced.
proof idea
One-line wrapper that applies native_decide to evaluate the concrete inequality σ_1(2) < 4 by direct computation of the divisor sum.
why it matters
The result supplies a verified base case for deficiency inside the arithmetic-functions module that supports later prime and Möbius constructions. No downstream theorems are recorded, so the declaration functions as an isolated computational anchor rather than a link in a longer chain. It remains outside the T0–T8 forcing sequence and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.