Audit missing positivity assumptions in Lander–Parkin–Selfridge

[DomTheDeveloper]

Finding

The canonical Lean declaration omits the positivity assumptions for k, n, and m that are stated in the prose.

As a regression witness, k = 1, n = 0, and m = 0 make both sums empty and equal while forcing the false conclusion 1 ≤ 0.

This is a formalization defect, not a counterexample to the mathematical Lander–Parkin–Selfridge conjecture.

Verification

Focused audit run 30209679826 passed:

• source scan rejecting proof holes and trust escapes;
• exact regression-module compilation under the pinned Lean toolchain;
• exact theorem axiom audit with no sorryAx.

Corrective action

The canonical declaration should add explicit positivity hypotheses for k, n, and m, matching its prose. The correction is now tracked under _PRs/queue/lander-parkin-selfridge-statement-fix.md in PR #270.

Keep this PR as draft regression evidence; do not treat it as a solved-conjecture or upstream-ready submission.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.