isPerfect_fourhundredninetysix
plain-language theorem explainer
496 satisfies the perfect number condition that the sum of its divisors equals twice itself. Number theorists checking small even perfect numbers or exercising decidable predicates in arithmetic function libraries would cite this concrete case. The proof reduces to a native decision procedure that evaluates the sigma function on 496 and confirms the equality.
Claim. The natural number 496 is perfect, i.e., the sum-of-divisors function satisfies $σ_1(496) = 2 · 496$.
background
The predicate isPerfect declares a natural number n perfect precisely when σ_1(n) equals 2n, and supplies a DecidablePred instance so that concrete values become decidable. The surrounding module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ, to support prime-related calculations. The upstream definition states: 'A number n is perfect if σ_1(n) = 2n. We make this decidable for concrete values.'
proof idea
One-line wrapper that applies the native_decide tactic to the decidable predicate isPerfect on the literal 496.
why it matters
The declaration supplies a verified concrete instance inside the arithmetic-functions library that also defines primeCounting. It confirms a known even perfect number (the third) without invoking the general Euclid-Euler theorem on Mersenne primes. No downstream theorems currently depend on it, leaving open whether larger Recognition Science results on divisor sums or prime ladders will invoke it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.