deficient_three
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 in Recognition Science
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.
scope and limits
- Does not prove deficiency for any integer besides 3.
- Does not relate the result to J-uniqueness, the phi ladder, or spatial dimensions.
- Does not invoke physical constants or the Recognition Composition Law.
formal statement (Lean)
1462theorem deficient_three : sigma 1 3 < 2 * 3 := by native_decide
proof body
Term-mode proof.
1463
1464/-- 4 is deficient: σ_1(4) = 7 < 8. -/