isPerfect_six
plain-language theorem explainer
6 satisfies the perfect number condition that its divisor sum equals twice the number. Researchers verifying small cases in arithmetic function libraries cite this verification. The proof is a one-line native_decide application on the decidable predicate for the sigma equality.
Claim. The sum of the positive divisors of 6 equals twice 6, that is, $σ_1(6) = 12$.
background
A number n is perfect when the sum-of-divisors function σ_1(n) equals 2n. The definition carries a DecidablePred instance that reduces the equality to direct computation for concrete inputs. The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ, yet this theorem is simply an instance check for the smallest perfect number.
proof idea
The proof is a one-line wrapper that invokes native_decide on the decidable instance of the sigma equality at 6.
why it matters
This declaration records the classical fact that 6 is perfect inside the arithmetic functions module. It supplies a basic verified case for divisor-sum checks but has no parent theorems in the current dependency graph. It touches the elementary number-theoretic scaffolding used for handling concrete divisor sums in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.