deficient_eleven
plain-language theorem explainer
The sum-of-divisors function satisfies σ(11) < 2·11, confirming that the prime 11 is deficient, as are all primes. Number theorists working with arithmetic functions or Recognition Science models of discrete number properties would cite this fact. The proof is a direct computational verification via the native_decide tactic.
Claim. Let σ(n) denote the sum of the positive divisors of the positive integer n. Then σ(11) < 2·11.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Here sigma denotes the standard sum-of-divisors function σ_k(n) = ∑_{d|n} d^k. The local theoretical setting keeps statements minimal before adding Dirichlet inversion layers. Upstream results include the structure of nuclear densities in NucleosynthesisTiers.of and the J-cost calibration in PhiForcingDerived.of, though the immediate step uses decidability of the numerical inequality.
proof idea
The proof is a one-line term proof that applies native_decide to evaluate and confirm the inequality directly.
why it matters
This theorem supplies a concrete instance of the general fact that primes are deficient, anchoring the arithmetic functions section of the Recognition Science framework. It supports the phi-ladder constructions and forcing chain steps that rely on basic number-theoretic properties. No downstream theorems are listed, leaving open how this fact integrates into larger claims about mass formulas or the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.