deficient_seven
plain-language theorem explainer
The theorem verifies that the sum of positive divisors of 7 is strictly less than 14, confirming 7 as deficient. Elementary number theorists would cite this as a direct check on the divisor sum function. The proof reduces to a single native_decide evaluation of the inequality.
Claim. $σ_1(7) < 14$, where $σ_1(n)$ is the sum of the positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and extending to the sum-of-divisors function. The sigma abbreviation is defined as the standard σ_k from ArithmeticFunction.sigma k. This places the result in a setting focused on basic interfaces for Dirichlet algebra before deeper inversion results are layered on.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete inequality directly.
why it matters
The result supplies a concrete arithmetic check within the NumberTheory layer of the Recognition Science monolith. It supports stabilization of basic divisor-sum interfaces that can feed into prime-related constructions or Möbius applications. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.