deficient_three
plain-language theorem explainer
The declaration shows that 3 is deficient because the sum-of-divisors function yields σ_1(3) = 4, which is strictly less than 6. Number theorists using Recognition Science arithmetic foundations would cite this as a basic verified case. The proof is a one-line wrapper that invokes native_decide to evaluate the inequality directly.
Claim. $σ_1(3) < 2 · 3$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and including the sum-of-divisors function. The sigma abbreviation is defined as ArithmeticFunction.sigma k, which returns the sum of the k-th powers of the divisors of its argument. The local setting centers on Möbius footholds for later Dirichlet extensions, and this theorem supplies a concrete check on deficient numbers using that sigma definition.
proof idea
The proof is a one-line wrapper that applies native_decide to compute sigma 1 3 and confirm the strict inequality.
why it matters
This supplies a verified instance of a deficient number inside the arithmetic functions module that supports Möbius interfaces. It contributes a basic number-theoretic check that may feed prime-related structures in Recognition Science, though it lists no downstream uses. The result aligns with the framework's pattern of concrete arithmetic verifications without invoking the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.