practical_thirtysix
plain-language theorem explainer
The divisor sum satisfies σ_1(36) = 91 which is at least 36, confirming the basic numerical condition tied to 36 being practical. Number theorists checking concrete cases of practical numbers or divisor bounds would cite this verification. The proof is a direct one-line wrapper that invokes native_decide to evaluate the inequality by computation.
Claim. $σ_1(36) ≥ 36$, where $σ_1(n)$ denotes the sum of all positive divisors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to the divisor sum σ_1. The local setting keeps statements minimal so that deeper Dirichlet inversion can be added later once interfaces stabilize. The declaration depends on the module-local definition of sigma together with the set of primes Primes := {n | Nat.Prime n}.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete inequality by direct computation of the divisor sum.
why it matters
This supplies a concrete numerical check inside the arithmetic-functions scaffolding of the NumberTheory.Primes section. It fills an explicit instance (σ_1(36) ≥ 36) that supports the definition of practical numbers. No downstream users are recorded yet, so the result remains a leaf verification rather than a parent lemma for larger prime or forcing-chain arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.