The rank-one Dixmier conjecture for elements of mass at most six
Let K be a field of characteristic zero and let P,Q in A_1(K) satisfy [Q,P]=1. We prove that P,Q generate A_1(K) if either has mass at most six, meaning at most six nonzero homogeneous components for the grading deg X=1, deg Y=-1, with no degree bound on either element. This extends the four-component theorem of Guccione, Guccione and Valqui. The proof combines their Newton-polygon restrictions with a classification of polynomial pairs r,f satisfying an associated scalar differential equation under the condition that r^2 has at most six monomial terms. The scalar argument uses a two-dimensional Vandermonde kernel, Rolle's theorem, and a sign and parity obstruction. The scalar classification and the mass bound reduce the crossing cases to a binomial-power face. We exclude that face using at most one Newton cut, without a mass bound on the transformed pair. We also exclude a family of pure-power crossing faces with prime outer exponent, without a mass bound. A seven-term scalar solution shows that the scalar classification is sharp, although its associated Weyl face is excluded by the pure-power theorem. Theorem 1.1 is formalized in Lean 4 and registered as Palomar entry PALOMAR-2026-10-05-000006, version 2. Theorem 1.1 is formalized in Lean 4 as Dixmier.Palomar.massSixGeneration. It passed statement comparison and the Lean, nanoda and con-ron kernel checks. The permitted axioms are propext, Classical.choice and Quot.sound. Palomar registration, version 2: https://palomar-registry.org/entry?id=PALOMAR-2026-10-05-000006&version=2Versioned formalization source: https://github.com/shaikidris/DixmierMassSix-Palomar/tree/61783d52b6ae44cd2d8d20ad6cb798e7bbbce3ffOfficial verification record: https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/37353942411 AI assistance. OpenAI Codex assisted with mathematical exploration, Lean formalization, and manuscript preparation. The author reviewed the AI-assisted material and takes full responsibility for the manuscript.
Authors
- Idris Ali Shaik (ORCID: https://orcid.org/0009-0009-9699-9712)
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-10-06
- DOI
- https://doi.org/10.5281/zenodo.23161792
- Primary Topic
- Advanced Topics in Algebra
- Type
- preprint