practical_twelve
plain-language theorem explainer
The sum-of-divisors function satisfies σ_1(12) ≥ 12, confirming 12 meets the practical-number threshold under the arithmetic-function definition. Number theorists checking concrete cases of practical numbers or divisor sums would cite this verification. The proof is a direct native decision that evaluates the inequality on the fixed natural-number input.
Claim. $σ_1(12) ≥ 12$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors family. The abbrev sigma k stands for ArithmeticFunction.sigma k, so sigma 1 is the ordinary divisor-sum function σ_1. The local setting keeps statements minimal, deferring deeper Dirichlet inversion until the basic interfaces stabilize.
proof idea
One-line wrapper that applies native_decide to the concrete inequality σ_1(12) ≥ 12.
why it matters
The declaration supplies a verified base case for practical numbers inside the NumberTheory.Primes.ArithmeticFunctions development. It draws on the sigma abbrev defined in the same module and sits among sibling results on the Möbius function. No downstream uses are recorded, so its role is to anchor concrete checks that may later support larger arithmetic-function arguments in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.