practical_one
plain-language theorem explainer
The theorem verifies that the sum-of-divisors function satisfies σ_1(1) ≥ 1, confirming the base case that 1 is practical. Number theorists examining practical numbers or basic arithmetic functions would cite this as the initial verification step. The proof is a direct one-line computation via native_decide that evaluates the divisor sum from the definition.
Claim. $σ_1(1) ≥ 1$, where $σ_1(n)$ is the sum of the 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 sibling sigma abbreviation defines σ_k(n) as the standard sum-of-divisors arithmetic function from Mathlib. This theorem appears in the NumberTheory.Primes.ArithmeticFunctions module, which keeps statements minimal before layering Dirichlet algebra.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the inequality directly from the sigma definition.
why it matters
This base case anchors the practical-number definition inside the arithmetic-functions layer of the Recognition Science monolith. It supplies the trivial starting point for divisor-sum properties that later connect to prime-related results, though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.