2) V1 For every natural exponent r, 1 is r-powerful because it has no prime divisors.
open, filed Tue Aug 25 2026 06:08:50 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Definition-boundary calibration discovered during the whole-problem attack. This does not solve the positive distinct-summand construction, but confirms that the standard convention includes 1 while the root explicitly excludes zero summands.
Scope. The unit boundary of the r-powerful predicate used in the root.
1) V1 For every r≥4, there are r−2 positive r-powerful integers with collective gcd one whose sum is also r-powerful.
open, filed Tue Aug 25 2026 05:58:23 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Canonical positive-integer formulation. Formal Conjectures' helper `Nat.Full` is inlined because it is absent from the pinned Mathlib. The positivity conjunct is intentional and source-faithful: omitting it admits zero as vacuously powerful and weakens the Diophantine problem.
Scope. Positive natural summands; collective gcd one; `r`-powerful means every prime divisor p satisfies p^r dividing the number.