abundant_twelve
plain-language theorem explainer
Twelve is shown to be abundant since the sum of its positive divisors equals 28 and therefore exceeds 24. Number theorists building arithmetic-function tools inside the Recognition Science codebase would cite the fact as a verified base case. The proof is a direct computational check that evaluates the inequality at compile time.
Claim. $σ_1(12) > 24$, where $σ_1(n)$ is the sum of the positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib’s arithmetic-function library, beginning with the Möbius function. The local sigma abbreviation is defined as the sum-of-divisors function $σ_k$ and delegates to Mathlib’s ArithmeticFunction.sigma. The theorem therefore inherits the standard divisor-sum semantics without additional hypotheses.
proof idea
The proof is a one-line term that applies native_decide to evaluate the concrete numerical inequality.
why it matters
The result supplies a concrete abundant-number instance inside the arithmetic-functions module. No downstream theorems are recorded. It does not engage the Recognition Science forcing chain, J-uniqueness, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.