isPerfect
plain-language theorem explainer
A natural number n is perfect precisely when the sum of its positive divisors equals twice n. Number theorists checking small even perfect numbers would cite this predicate for concrete verification. The definition is a direct one-line alias to the sigma_1 function together with an inferred decidability instance.
Claim. A natural number $n$ is perfect if $σ_1(n) = 2n$.
background
The sum-of-divisors function $σ_k$ returns the sum of the k-th powers of all positive divisors of its argument. In this module sigma is the abbrev that instantiates ArithmeticFunction.sigma, so sigma 1 n is exactly $σ_1(n)$. The file supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function $μ$ and extending to sigma as a foothold for later Dirichlet algebra.
proof idea
One-line definition that directly equates the predicate to sigma 1 n = 2 * n. The DecidablePred instance is obtained by inferInstanceAs on the resulting equality.
why it matters
The predicate is used by the three concrete theorems isPerfect_six, isPerfect_twentyeight and isPerfect_fourhundredninetysix that verify the first even perfect numbers via native_decide. It supplies the basic interface inside the ArithmeticFunctions module, which itself sits in the NumberTheory.Primes layer. No link to the Recognition Science forcing chain (T0–T8), J-uniqueness or the phi-ladder is present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.