isPerfect_twentyeight
plain-language theorem explainer
Verification that 28 satisfies sigma_1(28) = 56. Number theorists building libraries of arithmetic function properties or checking small even perfect numbers would cite this concrete instance. The proof is a one-line native_decide call on the decidable predicate.
Claim. $sigma_1(28) = 2 cdot 28$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The upstream isPerfect definition states that a number n is perfect if sigma 1 n = 2 n, equipped with a DecidablePred instance that reduces to evaluating the sigma equality. This theorem simply instantiates the predicate at the concrete value 28.
proof idea
One-line wrapper that applies native_decide to the decidable proposition isPerfect 28.
why it matters
Supplies a verified concrete example of the perfect-number predicate inside the arithmetic-functions module. No downstream uses appear. It contributes basic number-theory scaffolding to the monolith without engaging the forcing chain, RCL, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.