practical_eight
σ₁(8) ≥ 8 holds by direct computation, marking 8 as practical under the divisor-sum criterion used here. Number theorists checking base cases for practical numbers within Recognition Science arithmetic interfaces would cite this result. The proof is a one-line native_decide wrapper that evaluates the sum-of-divisors function exactly and confirms the inequality.
claimThe sum-of-divisors function satisfies $σ_1(8) ≥ 8$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for later Dirichlet work. Sigma is the abbreviation sigma (k : ℕ) := ArithmeticFunction.sigma k, which computes the sum of the k-th powers of the divisors of its argument. The local setting keeps statements minimal while the basic interfaces stabilize.
proof idea
The proof is a term-mode one-liner that invokes native_decide on the concrete inequality sigma 1 8 ≥ 8. The tactic evaluates the arithmetic function at the given arguments and discharges the comparison by computation, with no named lemmas required beyond the sigma definition.
why it matters in Recognition Science
This supplies a verified numerical base fact inside the arithmetic-functions module, supporting number-theory scaffolding before inversion or prime-distribution results are layered on. It has no downstream citations in the current graph and does not touch the forcing chain, phi-ladder, or Recognition constants, but it closes a concrete check aligned with the module's stated goal of stabilizing lightweight interfaces.
scope and limits
- Does not prove the inequality for any n other than 8.
- Does not invoke the Möbius function or Dirichlet inversion.
- Does not connect to the Recognition forcing chain or phi-ladder.
- Does not address asymptotic behavior of sigma or general practical numbers.
formal statement (Lean)
2134theorem practical_eight : sigma 1 8 ≥ 8 := by native_decide
proof body
Term-mode proof.
2135
2136/-- σ_1(12) = 28 ≥ 12, so 12 is practical. -/