practical_four
plain-language theorem explainer
The sum-of-divisors function satisfies σ₁(4) ≥ 4, confirming that 4 meets the divisor condition used to identify practical numbers. Number theorists working on arithmetic functions or practical-number lists would reference this concrete case. The proof evaluates the inequality through a native decision procedure that computes the divisor sum directly.
Claim. $σ_1(4) ≥ 4$, where $σ_1(n)$ denotes the sum of the positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function. The abbreviation sigma (k : ℕ) stands for ArithmeticFunction.sigma k, which returns the k-th divisor-sum function. This theorem supplies a specific numerical check inside that library for the case n = 4.
proof idea
The proof is a one-line wrapper that applies native_decide to the concrete inequality sigma 1 4 ≥ 4.
why it matters
The declaration supplies a verified base case inside the arithmetic-functions module that supports divisor-based arguments in the Recognition Science number-theory layer. It sits alongside Möbius-function definitions and feeds any later practical-number or prime-related constructions, though no downstream uses are recorded yet. The result aligns with the module's focus on stable interfaces for Dirichlet algebra and inversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.