Develop parametric families for A280831

[DomTheDeveloper]

Goal

Record kernel-verified algebraic progress toward Zhi-Wei Sun’s 1680-conjecture (OEIS A280831).

Verified results

The exact module at c39efc8f29479a6111a627fb388a846147a40556 passed ProofPlaygrond targeted audit run 30187962389, including source scanning, compilation of every theorem below, printed-axiom inspection, and rejection of sorryAx and compiler-trust shortcuts.

• every three-square representation is automatically admissible by taking z = 0;
• HasSquareCondition n is preserved by multiplying n by an arbitrary square;
• therefore it is preserved by multiplication by every 4^a;
• any integer identity c^4 + 1680 d = q^2 yields the infinite family
  ((c^2 + 1 + d^2) y^2 + w^2);
• explicit corollaries cover
  • 3 y^2 + w^2,
  • 11 y^2 + w^2,
  • 18 y^2 + w^2.

These are genuine partial results. They do not prove the universal A280831 conjecture; the unresolved core is to cover every odd integer of the form 8b + 7.

[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.