\documentclass[11pt,letterpaper]{article}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[margin=1.02in]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{graphicx,longtable,booktabs,array,calc,float,needspace}
\usepackage{microtype,xurl}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={The rank-one Dixmier conjecture for elements of mass at most six},pdfauthor={Idris Ali Shaik},pdfsubject={Mass bounds and sparse scalar equations in the first Weyl algebra},pdfkeywords={Dixmier conjecture, Weyl algebra, homogeneous components, sparse polynomials, Newton polygon}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\numberwithin{equation}{section}
\providecommand{\tightlist}{\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\providecommand{\pandocbounded}[1]{#1}
\setlength{\emergencystretch}{1.5em}
\setlength{\parskip}{0.2em}
\renewcommand{\topfraction}{0.85}
\renewcommand{\textfraction}{0.1}
\renewcommand{\floatpagefraction}{0.85}
\title{The rank-one Dixmier conjecture for elements of mass at most six}
\author{Idris Ali Shaik\\[0.35em]\small Independent researcher (unaffiliated)\\\small\href{https://orcid.org/0009-0009-9699-9712}{ORCID: 0009-0009-9699-9712}\\\small\href{mailto:shaikidris@apache.org}{shaikidris@apache.org}}
\date{6 October 2026}
\newcounter{none}
\begin{document}
\maketitle
\begin{abstract}
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.
\end{abstract}
\textbf{2020 Mathematics Subject Classification.} Primary 16S32; Secondary 16W20, 16W50.

\textbf{Keywords.} Dixmier conjecture; Weyl algebra; homogeneous components; sparse polynomials; Newton polygon.

\noindent\footnotesize Copyright \(\copyright\) 2026 Idris Ali Shaik. Licensed under \href{https://creativecommons.org/licenses/by/4.0/}{CC BY 4.0}.\normalsize

\section{Introduction}\label{sec:1}

Let \(K\) be a field of characteristic zero. Write \[
A_1(K)=K\langle X,Y\rangle/(YX-XY-1),
\qquad [U,V]=UV-VU.
\] The rank-one Dixmier conjecture \cite{D68} asks whether every pair with commutator one generates \(A_1(K)\). Equivalently, it asks whether every unital \(K\)-algebra endomorphism of \(A_1(K)\) is an automorphism: the assignments \(X\mapsto P\), \(Y\mapsto Q\) define an endomorphism exactly when \([Q,P]=1\); generation is surjectivity, and simplicity of \(A_1(K)\) ensures injectivity.

The three-variable Jacobian counterexamples described in \cite{Ga26} and \cite{T26}, together with the implication \(\mathrm{DC}_n\Rightarrow\mathrm{JC}_n\) in \cite{BCW82} (see also \cite[Introduction]{BK07}), rule out the Dixmier conjecture in ranks at least three: adjoining unchanged coordinates extends a three-variable counterexample to every higher dimension. This implication does not settle the rank-one question studied here.

Give \(A_1(K)\) the \(\mathbb Z\)-grading determined by \(\deg X=1\) and \(\deg Y=-1\). For the homogeneous decomposition \(P=\sum_jP_j\), put \[
m(P)=\#\{j:P_j\ne0\}.
\] Following Bavula and Levandovskyy \cite{BL20}, we call \(m(P)\) the mass of \(P\). It counts homogeneous components, not monomials: one component may contain arbitrarily many Poincaré--Birkhoff--Witt (PBW) monomials \(X^iY^j\).

A bound on mass restricts the graded support while allowing arbitrarily large polynomial degrees. Bavula and Levandovskyy proved generation when both members have mass at most two \cite{BL20}. Han and Tan showed that mass at most two on one member suffices \cite[Theorem 3.15]{HT24}. Guccione, Guccione and Valqui raised the one-member bound to four \cite[Corollary 4.3]{G24}. We extend that conclusion to six components.

\Needspace{6\baselineskip}
\begin{theorem}\label{theorem:1-1}

Let \(K\) be any field of characteristic zero and let \(P,Q\in A_1(K)\). If \[
[Q,P]=1\qquad\text{and}\qquad m(P)\le6,
\] then \(K\langle P,Q\rangle=A_1(K)\).

\end{theorem}

The conclusion also holds when \(m(Q)\le6\), by applying the theorem to \((Q,-P)\), since \([-P,Q]=1\). Thus both members of a nongenerating pair with commutator one have mass at least seven. The five-component case is included, and no bound is imposed on the degree of either member or the mass of \(Q\), the mate of \(P\).

Theorem~\ref{theorem:1-1} is formally proved in Lean 4 with Mathlib and registered as Palomar entry PALOMAR-2026-10-05-000006, version 2 \cite{S26}. The checked proof uses only \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound}.

The proof uses the Newton configurations in \cite{G24}. The main issue is the case of a face crossing from positive to negative grade. The homogeneous companion condition alone cannot exclude every five-component configuration: \cite[Remark 4.4]{G24} gives such a configuration. We classify the sparse scalar solutions permitted by that condition and then exclude the remaining binomial-power face using at most one Newton cut. Mass preservation is needed for the initial case reduction. Once the face is fixed, the cut produces an endpoint forbidden by the published geometric restrictions; no mass bound on the transformed pair is needed.

For a nonzero polynomial \(S\), write \(t(S)\) for its number of nonzero monomials. For a hypothetical counterexample with mass at most six and a strict negative crossing in direction \((\rho,-s)\), with coprime integers \(\rho>s\ge1\), Lemma~\ref{lemma:5-1} reduces the leading symbol to \(\mu R^2\), where \(R=xr(w)\), \(w=x^s y^\rho\), and the homogeneous companion is \(F=xyf(w)\). Here \(x,y\) are commuting variables recording the PBW monomials \(X^iY^j\). The leading symbol is the sum of the terms on the corresponding Newton face (Section~\ref{sec:4}), and \(x^iy^j\) has grade \(i-j\). With the Poisson convention of Section~\ref{sec:4}, the identity \(\{R,F\}=R\) is precisely the equation below. The terms of \(R^2\) have distinct grades \(2-(\rho-s)n\), so \(t(r^2)\le m(P)\). The scalar input is the following classification.

\Needspace{6\baselineskip}
\begin{theorem}\label{theorem:1-2}

Let \(\rho>s\ge1\) be integers. Suppose that \(r,f\in\mathbb C[w]\), that \(r\) is nonconstant with \(r(0)=1\), and that \begin{equation}\label{eq:1-1}
(\rho-s)wf r'-(f+\rho wf'+1)r=0.
\end{equation} If \(t(r^2)\le6\), then there is a \(\lambda\in\mathbb C^\times\) such that \begin{equation}\label{eq:1-2}
\rho=2s+1,\qquad
r=(1-\lambda w)^2,\qquad f=\lambda w-1.
\end{equation} Thus \(r^2\) has exactly five terms.

\end{theorem}

The geometric exclusion has a broader form that does not require a mass bound. Here a counterexample pair means \(P,Q\in A_1(\mathbb C)\) with \([Q,P]=1\) and \(\mathbb C\langle P,Q\rangle\ne A_1(\mathbb C)\). The notation \(\ell_{\rho,-s}\) for the leading symbol is defined in Section~\ref{sec:4}.

\Needspace{6\baselineskip}
\begin{theorem}[pure-power face exclusion]\label{theorem:1-3}

Let \(q\ge2\) and \(s\ge0\) be integers such that \(\rho=(qs+1)/(q-1)\) is an integer. Let \(p\) be prime and \(\alpha,\mu\in\mathbb C^\times\). No counterexample pair has \begin{equation}\label{eq:1-3}
\ell_{\rho,-s}(P)
=\mu x^p(1+\alpha x^s y^\rho)^{pq}.
\end{equation} No mass or degree bound is imposed on either operator.

\end{theorem}

For \(p=q=2\), the face \eqref{eq:1-3} is \(\mu R^2\) with \(r\) as in \eqref{eq:1-2} and \(\alpha=-\lambda\). This is the specialization required for Theorem~\ref{theorem:1-1}. Section~\ref{sec:5} proves the exclusion using at most one Newton cut.

The scalar proof is independent of the Weyl-algebra inputs. The equation forces a repeated root and primitive exponent support (defined in Section~\ref{sec:2}). A root of multiplicity four in a square with six monomial terms imposes four linear moment conditions on its coefficients, leaving a two-dimensional Vandermonde kernel. A second such root forces real coefficients after rescaling, with the two distinguished roots nonreal and conjugate. The values of \(wf'(w)\) prescribed by the equation then rule out real roots of \(f\), and therefore of \(r\). Both degrees are even, contradicting \((\rho-s)\deg r-\rho\deg f=1\) from Lemma~\ref{lemma:3-1}. The remaining one-double-root case is governed by a sign-preserving coefficient recurrence.

Zheglov \cite{Z26} has proposed a proof of the unrestricted rank-one conjecture. The argument here does not use that claim; its external structural inputs are stated in Section~\ref{sec:4}. The scalar classification is an independent polynomial result.

Section~\ref{sec:2} proves the sparse-root lemmas, and Section~\ref{sec:3} proves Theorem~\ref{theorem:1-2}. Sections~\ref{sec:4} and~\ref{sec:5} give the Newton inputs and prove Theorem~\ref{theorem:1-1}, ending with descent from \(\mathbb C\) to any characteristic-zero field. Section~\ref{sec:6} discusses seven-term scalar solutions and other boundary examples, distinguishing them from the pure-power face exclusion. Appendix~\ref{sec:A} records two further coefficient-nonvanishing results for scalar families; neither is needed for the main theorem.

Theorem~\ref{theorem:1-1} is formalized in Lean 4 \cite{S26}; the verification note after Section~\ref{sec:6} describes its scope.

For the scalar and Newton arguments below we work over \(\mathbb C\) and write \(A_1=A_1(\mathbb C)\). The final step of the proof of Theorem~\ref{theorem:1-1} returns to the general field \(K\).

\textbf{Notation guide.} The main notation and its defining sections are collected below.

{\def\LTcaptype{none} % do not increment counter
\begin{longtable}[]{@{}>{\raggedright\arraybackslash}p{\dimexpr 0.42\linewidth-2\tabcolsep\relax}>{\raggedright\arraybackslash}p{\dimexpr 0.46\linewidth-2\tabcolsep\relax}>{\raggedright\arraybackslash}p{\dimexpr 0.12\linewidth-2\tabcolsep\relax}@{}}
\toprule\noalign{}
\begin{minipage}[b]{\linewidth}\raggedright
Notation
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Meaning
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Section
\end{minipage} \\
\midrule\noalign{}
\endhead
\bottomrule\noalign{}
\endlastfoot
\(X,Y\); \(x,y\) & Weyl generators; commuting variables recording PBW monomials & 1, 4.1 \\
\(m(P)\) & Number of nonzero homogeneous components for grade \(i-j\) & 1 \\
\(t(S)\) & Number of nonzero monomials of a polynomial \(S\) & 1 \\
\(\delta,e,L\) & \(\rho-s,\deg r,\deg f\) in the scalar proof & 3 \\
\(v_{\rho,\sigma}(P)\), \(\ell_{\rho,\sigma}(P)\) & Maximum weight and leading symbol & 4.1 \\
\(\operatorname{st}_{\rho,\sigma}(P)\), \(\operatorname{en}_{\rho,\sigma}(P)\) & Face endpoints with smallest and largest \(y\)-exponent, for \(\rho>0\) & 4.1 \\
\(\operatorname{Dir}(P)\) & Directions whose face contains at least two monomials & 4.1 \\
\end{longtable}
}

\section{Repeated roots of sparse polynomials}\label{sec:2}

The mass estimate will ultimately count terms on a Newton face. We begin with the classical multiplicity bound \cite[Lemma 1]{Bri01}; see also \cite[Lemma 1]{M07}. We include its short proof, then identify the additional rigidity when a six-term polynomial has two roots of multiplicity four.

We say that a polynomial with nonzero constant coefficient has \textbf{primitive exponent support} if the greatest common divisor of its positive exponents is one. Rescaling the variable by a nonzero constant preserves this property and its number of terms.

\Needspace{6\baselineskip}
\begin{lemma}\label{lemma:2-1}

If a nonzero polynomial \(S\) has \(t\) terms, every nonzero root of \(S\) has multiplicity at most \(t-1\).

\end{lemma}

\begin{proof} Write \(S(w)=\sum_{i=1}^t c_iw^{n_i}\), with distinct nonnegative integers \(n_i\) and \(c_i\ne0\). At a nonzero root \(\alpha\) of multiplicity at least \(t\), the first \(t\) Euler derivatives, obtained by powers of the Euler operator \(w\,d/dw\), vanish, since each \((w\,d/dw)^j\) is a linear combination of ordinary derivatives of orders at most \(j\), with polynomial coefficients: \[
\sum_{i=1}^t c_i\alpha^{n_i}n_i^j=0,
\qquad 0\le j<t.
\] The coefficient matrix is Vandermonde and invertible. This would force every \(c_i\alpha^{n_i}\) to be zero. \end{proof}

\Needspace{6\baselineskip}
\begin{lemma}\label{lemma:2-2}

Let \[
S(w)=\sum_{i=0}^{5}c_iw^{n_i},\qquad
0=n_0<n_1<\cdots<n_5,
\] where all \(c_i\ne0\), \(c_0=1\), and \(\gcd(n_1,\ldots,n_5)=1\). If \(S\) has two distinct nonzero roots of multiplicity at least four, these are its only such roots. After a nonzero scaling of the variable, \(S\) has real coefficients and these two roots are nonreal conjugates on the unit circle.

\end{lemma}

\begin{proof} Scale the first root to one, keeping the notation \(S\). Set \[
D_i=\prod_{j\ne i}(n_i-n_j).
\] The Euler derivatives of orders zero through three give \begin{equation}\label{eq:2-1}
\sum_{i=0}^5 c_i n_i^k=0,\qquad 0\le k\le3.
\end{equation} This system has a two-dimensional kernel. Lagrange interpolation gives \[
z^k=\sum_{i=0}^5 n_i^k\frac{\prod_{j\ne i}(z-n_j)}{D_i},
\qquad 0\le k\le4.
\] Comparing the coefficients of \(z^5\) yields \[
\sum_{i=0}^5\frac{n_i^k}{D_i}=0,
\qquad 0\le k\le4.
\] The vectors \((D_i^{-1})_i\) and \((n_iD_i^{-1})_i\) are linearly independent and satisfy \eqref{eq:2-1}. Consequently \begin{equation}\label{eq:2-2}
c_i=\frac{a+bn_i}{D_i},\qquad a=D_0\in\mathbb R\setminus\{0\},
\quad b\in\mathbb C.
\end{equation} The value of \(a\) follows from \(c_0=1\).

Let \(\beta\ne1\) be a second root of multiplicity at least four. The vector \((c_i\beta^{n_i})_i\) satisfies the same system and has zeroth coordinate one. Thus, for some \(d\in\mathbb C\), \begin{equation}\label{eq:2-3}
\beta^{n_i}(a+bn_i)=a+dn_i,
\qquad 0\le i\le5.
\end{equation}

Suppose first that \(\tau=2\log|\beta|\ne0\). The real function \[
G(t)=e^{\tau t}|a+bt|^2-|a+dt|^2
\] vanishes at the six distinct real points \(n_i\). Rolle's theorem, applied three times, implies that \(G'''\) has at least three distinct zeros. On the other hand, \begin{equation}\label{eq:2-4}
G'''(t)=e^{\tau t}(\partial_t+\tau)^3|a+bt|^2.
\end{equation} The second factor is a nonzero polynomial of degree at most two: \(\partial_t+\tau\) is invertible on polynomials when \(\tau\ne0\), and \(|a+bt|^2\) has degree at most two and nonzero constant term \(a^2\). This contradiction proves \(|\beta|=1\).

Taking squared absolute values in \eqref{eq:2-3} now shows that the two quadratic polynomials \(|a+bt|^2\) and \(|a+dt|^2\) agree at six points, hence are identical. Since \(a\) is real and nonzero, their coefficients give \[
\operatorname{Re}d=\operatorname{Re}b,\qquad |d|=|b|.
\] Therefore \(d=b\) or \(d=\overline b\). If \(d=b\), the nonzero coefficients in \eqref{eq:2-2} imply \(\beta^{n_i}=1\) for every \(i\). The order of this root of unity divides every \(n_i\), hence their greatest common divisor one. Thus \(\beta=1\), a contradiction. It follows that \(d=\overline b\ne b\), so \(b\) is nonreal and \begin{equation}\label{eq:2-5}
b\notin\mathbb R,\qquad
c_i\beta^{n_i}=\overline{c_i}.
\end{equation} Every further root of multiplicity at least four, distinct from one, would give the same right side in \eqref{eq:2-5}. Division of the corresponding equalities and primitivity identify that root with \(\beta\).

Choose \(\eta\) with \(\eta^2=\beta\) and \(|\eta|=1\). Equation \eqref{eq:2-5} gives \[
\overline{c_i\eta^{n_i}}
=\overline{c_i}\eta^{-n_i}=c_i\eta^{n_i}.
\] Hence \(S(\eta w)\) has real coefficients. Its two distinguished roots are \(\eta\) and \(\overline\eta\). They are nonreal, since a real \(\eta\) on the unit circle would give \(\beta=1\). \end{proof}

\Needspace{6\baselineskip}
\begin{lemma}\label{lemma:2-3}

A five-term polynomial with nonzero constant coefficient and primitive exponent support has at most one nonzero root of multiplicity at least four.

\end{lemma}

\begin{proof} Normalize its constant coefficient and one such root to one. The four Euler equations now have a one-dimensional Vandermonde kernel. At another such root \(\beta\), the vector \((c_i\beta^{n_i})_i\) belongs to the same kernel and has the same zeroth coordinate as \((c_i)_i\). Thus \(\beta^{n_i}=1\) for every support exponent. Primitivity gives \(\beta=1\). \end{proof}

\section{The scalar rigidity theorem}\label{sec:3}

For Lemma~\ref{lemma:3-1}, assume only the polynomial and differential-equation hypotheses of Theorem~\ref{theorem:1-2}; no bound on \(t(r^2)\) is needed. Put \[
\delta=\rho-s,\qquad e=\deg r,\qquad L=\deg f.
\] The sparse-root lemmas control the number and position of double roots of \(r\). The differential equation supplies the complementary information: it prescribes the derivative of \(f\) at each root and couples the two polynomial degrees by an integer identity. We first establish these facts.

\Needspace{6\baselineskip}
\begin{lemma}\label{lemma:3-1}

The following statements hold:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\tightlist
\item
  \(f(0)=-1\), \(L\ge1\), and \begin{equation}\label{eq:3-1}
\delta e=1+\rho L,\qquad L<e.
\end{equation}
\item
  \textbf{Root containment.} Every root \(\alpha\) of \(r\) is a simple root of \(f\). If its multiplicity in \(r\) is \(j\), then \begin{equation}\label{eq:3-2}
\alpha f'(\alpha)(\delta j-\rho)=1.
\end{equation} A root \(\gamma\) of \(f\) outside the roots of \(r\) satisfies \begin{equation}\label{eq:3-3}
\gamma f'(\gamma)=-1/\rho.
\end{equation} In particular, all roots of \(f\) are simple and nonzero.
\item
  For fixed \(r\), equation \eqref{eq:1-1} has at most one solution \(f\) in \(\mathbb C[[w]]\). Both \(r\) and \(r^2\) have primitive exponent support.
\end{enumerate}

\end{lemma}

\begin{proof} Evaluation at zero gives \(f(0)=-1\). A constant solution would therefore be \(f=-1\), in which case \eqref{eq:1-1} would force \(r'=0\). Thus \(L\ge1\). Comparison of the coefficients of degree \(e+L\) gives \eqref{eq:3-1}, and \(\rho>\delta>0\) implies \(L<e\).

Every root of \(r\) is nonzero. At a root \(\alpha\) of multiplicity \(j\), a nonzero value of \(f(\alpha)\) would leave an unmatched term of order \(j-1\) in \eqref{eq:1-1}. Thus \(f(\alpha)=0\). A zero of \(f\) of order at least two would leave the term \(-r\) unmatched at order \(j\). Comparison at that order for a simple zero gives \eqref{eq:3-2}. At a zero of \(f\) outside \(r\), direct substitution gives \eqref{eq:3-3}, which also proves simplicity there.

If a nonzero difference of two formal solutions starts with \(cw^j\), the lowest coefficient of the homogeneous difference equation is \(-(1+\rho j)c\), which cannot vanish. This proves uniqueness.

Suppose \(r\in\mathbb C[w^g]\) for an integer \(g>1\). For every \(g\)-th root of unity \(\zeta\), the polynomial \(f(\zeta w)\) solves the same equation as \(f(w)\): the operator \(w\,d/dw\) commutes with scaling. Uniqueness yields \(f\in\mathbb C[w^g]\). Then \(g\) divides both \(e\) and \(L\), contradicting \eqref{eq:3-1}. Finally, if \(r^2\in\mathbb C[w^g]\), then \(r(\zeta w)^2=r(w)^2\); their constant coefficients are both one, so \(r(\zeta w)=r(w)\). This would contradict the primitivity of \(r\). \end{proof}

We now impose \(t(r^2)\le6\). Apply Lemma~\ref{lemma:2-1} to \(r^2\): a root of \(r\) of multiplicity \(j\) gives \(2j+1\le t(r^2)\le6\), so \(j\le2\). There is at least one double root, since otherwise root containment in Lemma~\ref{lemma:3-1} would give \(e\le L\). A double root of \(r\) has multiplicity four in \(r^2\), so Lemma~\ref{lemma:2-1} gives \(t(r^2)\ge5\).

\Needspace{6\baselineskip}
\begin{lemma}\label{lemma:3-2}

The polynomial \(r\) has exactly one double root.

\end{lemma}

\begin{proof} If \(t(r^2)=5\), Lemma~\ref{lemma:2-3} gives the conclusion.

\textbf{Real form.} Suppose \(t(r^2)=6\) and that \(r\) has at least two double roots. Lemma~\ref{lemma:2-2} shows that there are exactly two. After a scaling, \(r^2\) has real coefficients and these roots are a nonreal conjugate pair.

Apply the same scaling to \(r\) and \(f\); equation \eqref{eq:1-1} is unchanged. The normalized square root \(r\) itself is real, since \(\overline r^2=r^2\) and both constant coefficients are one. The formal uniqueness in Lemma~\ref{lemma:3-1} then makes \(f\) real as well.

\textbf{Real-root signs.} The two double roots of \(r\) are nonreal. A real root \(\gamma\) of \(f\) therefore is either a simple root of \(r\) or is not a root of \(r\). Equation \eqref{eq:3-2} with \(j=1\) and equation \eqref{eq:3-3} give, respectively, \begin{equation}\label{eq:3-4}
\gamma f'(\gamma)=-1/s
\quad\text{or}\quad
\gamma f'(\gamma)=-1/\rho.
\end{equation} Both are negative. But a real polynomial with \(f(0)=-1\) and simple roots has \(\gamma f'(\gamma)>0\) at the first root reached along either real ray from zero. Indeed, at the first positive root it crosses from negative values with positive derivative; at the first negative root its derivative is negative. Therefore \(f\) has no real roots. Root containment gives the same conclusion for \(r\).

\textbf{Parity.} Both polynomials are real and have only nonreal roots, so \(e\) and \(L\) are even. This contradicts the integer identity \[
(\rho-s)e-\rho L=1.
\] The six-term case with at least two double roots is impossible. \end{proof}

\begin{proof}[Proof of Theorem~\ref{theorem:1-2}] Scale the unique double root to one. Every other root of \(r\) is simple. Root containment and \(L<e\) give \begin{equation}\label{eq:3-5}
L=e-1,\qquad \rho=se+1,\qquad f=\frac{r}{w-1}.
\end{equation} Indeed, root containment first gives \(f=c\,r/(w-1)\), and \(r(0)=1\), \(f(0)=-1\) force \(c=1\). The degree identity \eqref{eq:3-1} with \(L=e-1\) gives \(\rho=se+1\). Substitution in \eqref{eq:1-1}, followed by multiplication by \((w-1)^2/r\), yields \begin{equation}\label{eq:3-6}
-sw(w-1)r'+((\rho-1)w+1)r=(w-1)^2.
\end{equation} Write \(r=\sum_{j=0}^e u_jw^j\), with \(u_0=1\). Its coefficients satisfy \begin{equation}\label{eq:3-7}
(sj+1)u_j+s(e-j+1)u_{j-1}=b_j,\qquad 1\le j\le e,
\end{equation} where \(b_1=-2\), \(b_2=1\), and \(b_j=0\) for \(j\ge3\). In particular, \[
u_1=-\frac{se+2}{s+1}<0,\qquad
u_2=\frac{1-s(e-1)u_1}{2s+1}>0.
\] For \(3\le j\le e\), equation \eqref{eq:3-7} gives \[
u_j=-\frac{s(e-j+1)}{sj+1}u_{j-1}.
\] Hence \((-1)^j u_j>0\) for every \(j\). All summands contributing to each coefficient of \(r^2\) have the same sign. Each degree from zero to \(2e\) occurs, with coefficient of sign \((-1)^j\) in degree \(j\), so \begin{equation}\label{eq:3-8}
t(r^2)=2e+1.
\end{equation} The bound \(t(r^2)\le6\), together with \(e\ge2\), forces \(e=2\). Equations \eqref{eq:3-5}--\eqref{eq:3-7} give \(r=(1-w)^2\), \(f=w-1\), and \(\rho=2s+1\). Undoing the scaling proves \eqref{eq:1-2}. \end{proof}

\section{Newton faces and structural results}\label{sec:4}

The scalar theorem will exclude the crossing faces in a published Newton classification. This section states the exact structural inputs and fixes the conventions needed to apply them. All source result numbers refer to the versioned arXiv texts specified in the bibliography.

\subsection{Newton polygon and leading symbols}\label{sec:4.1}

Write a Weyl operator in PBW order, with all powers of \(X\) to the left, as \(P=\sum p_{ij}X^iY^j\). Its support is the set of pairs \((i,j)\) with \(p_{ij}\ne0\). Its convex hull is the \textbf{Newton polygon} of \(P\). We use commuting variables \(x,y\) to record the PBW monomials. For an integer direction \((\rho,\sigma)\) with \(\gcd(\rho,\sigma)=1\) and \(\rho+\sigma>0\), let \[
v_{\rho,\sigma}(P)=\max_{p_{ij}\ne0}(\rho i+\sigma j),\qquad
\ell_{\rho,\sigma}(P)
=\sum_{\rho i+\sigma j=v_{\rho,\sigma}(P)}p_{ij}x^iy^j.
\] The \((\rho,\sigma)\)-\textbf{face} is the part of the Newton polygon on the line \(\rho i+\sigma j=v_{\rho,\sigma}(P)\); the polynomial \(\ell_{\rho,\sigma}(P)\) records its support terms. Throughout, \(\deg P=v_{1,1}(P)\) denotes total degree in the PBW generators. An operator is \textbf{subrectangular} with vertex \((a,b)\) if \((a,b)\) belongs to its support and its support is contained in \([0,a]\times[0,b]\).

For \(\rho>0\), the face's starting and ending points, denoted \(\operatorname{st}_{\rho,\sigma}(P)\) and \(\operatorname{en}_{\rho,\sigma}(P)\), are the support points with smallest and largest \(y\)-exponent. We suppress the direction subscript when it is fixed. A direction belongs to \(\operatorname{Dir}(P)\) when this face contains at least two monomials. The grade of a point \((i,j)\) is \(i-j\). A face is a \textbf{strict crossing} if its starting grade is positive and its ending grade is negative. Figure~\ref{fig:crossing} illustrates these definitions.

\begin{figure}[!htbp]
\centering
\includegraphics[width=.70\textwidth]{figures/crossing-face.png}
\caption{An illustrative support with a strict crossing in direction \((3,-1)\). The face lies on \(3i-j=6\); its starting point has grade \(2\) and its ending point has grade \(-2\). Dashed lines have constant grade \(i-j\). The figure illustrates the definitions and makes no claim about the existence of a Weyl mate.}\label{fig:crossing}
\end{figure}

\textbf{Grade count.} Distinct monomials on a positive-sum face have distinct grades: the linear forms \(\rho i+\sigma j\) and \(i-j\) are independent. The number of terms on such a face of \(P\) is therefore at most \(m(P)\). Here and below, a \((\rho,\sigma)\)-homogeneous polynomial is supported on one weight line; this is distinct from homogeneity for the grading \(i-j\).

Our Poisson convention is \[
\{a,b\}=a_yb_x-a_xb_y,
\] which is the leading-bracket convention for \([Y,X]=1\). When the leading Poisson bracket is nonzero, it is the leading symbol of the commutator: \(\ell_{\rho,\sigma}([U,V])=
\{\ell_{\rho,\sigma}(U),\ell_{\rho,\sigma}(V)\}\) when the right side is nonzero. Products of leading symbols multiply in every positive-sum direction.

Recall that a counterexample pair \((P,Q)\) satisfies \([Q,P]=1\) and \(\mathbb C\langle P,Q\rangle\ne A_1\). Changing the sign of the mate reconciles this convention with the order \([P,Q]=1\) used in \cite{G24}, without changing the mass or leading support of \(P\).

\subsection{Structural results of Guccione, Guccione and Valqui}\label{sec:4.2}

Propositions~\ref{proposition:4-1}--\ref{proposition:4-3} supply the homogeneous companion, the case reduction and the degree bound used in Section~\ref{sec:5}. Section~\ref{sec:4.3} states the cut and corner restrictions used to prove Theorem~\ref{theorem:1-3}.

\Needspace{6\baselineskip}
\begin{proposition}[positivity and companion]\label{proposition:4-1}

For a counterexample pair, the maximum and minimum grades of \(P\) have opposite signs, and \(v_{\rho,\sigma}(P)>0\) in every positive-sum direction. Moreover, in each such direction there are a nonzero homogeneous polynomial \(R\), a scalar \(\mu\ne0\), an integer \(k\ge2\), and a homogeneous polynomial \(F\) such that \begin{equation}\label{eq:4-1}
\ell_{\rho,\sigma}(P)=\mu R^k,\qquad
v_{\rho,\sigma}(F)=\rho+\sigma,\qquad \{R,F\}=R.
\end{equation} We call \(F\) the homogeneous companion of \(R\).

\end{proposition} These are \cite[Propositions 1.2, 1.4 and 2.6]{G24}. They apply equally to the other member of a counterexample pair.

\Needspace{6\baselineskip}
\begin{proposition}[case reduction]\label{proposition:4-2}

After at most the Fourier exchange \(X\mapsto Y\), \(Y\mapsto-X\), every counterexample pair is in at least one of the following alternatives:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\tightlist
\item
  \(P\) has a strict crossing face with \(\rho>0\) and \(-\rho<\sigma\le0\).
\item
  \(m(P)\ge10\).
\item
  Its total-degree leading symbol is \begin{equation}\label{eq:4-2}
\ell_{1,1}(P)=\lambda(y-\alpha x)^u(y-\beta x)^v,
  \quad \lambda\alpha\beta\ne0,\quad \alpha\ne\beta,
  \quad u,v\ge1.
\end{equation}
\end{enumerate}

\end{proposition}

This formulation is justified by the following source case analysis.

\textbf{Derivation from the cited case analysis.} We collect \cite[Remark 3.3, Proposition 4.1 and the proof of Theorem 4.2]{G24}. Cases 1, 2 and 5 of \cite[Proposition 4.1]{G24} provide the strict crossing, specifically its displayed condition (4.14). Cases 3 and 6 give the bound ten, Case 4 gives a bound strictly greater than sixteen, and Case 7 has the form \eqref{eq:4-2}. The table matches each total-degree symbol configuration to the source cases and the resulting alternative. An endpoint is \textbf{axial} if it lies on a coordinate axis; the \textbf{horizontal ending grade} means the grade of \(\operatorname{en}_{1,0}(P)\).

{\def\LTcaptype{none} % do not increment counter
\begin{longtable}[]{@{}>{\raggedright\arraybackslash}p{\dimexpr 0.35\linewidth-2\tabcolsep\relax}>{\raggedright\arraybackslash}p{\dimexpr 0.2\linewidth-2\tabcolsep\relax}>{\raggedright\arraybackslash}p{\dimexpr 0.45\linewidth-2\tabcolsep\relax}@{}}
\toprule\noalign{}
\begin{minipage}[b]{\linewidth}\raggedright
Total-symbol configuration in \cite[Remark 3.3]{G24}
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Cases of \cite[Proposition 4.1]{G24}
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Applicable alternative
\end{minipage} \\
\midrule\noalign{}
\endhead
\bottomrule\noalign{}
\endlastfoot
One monomial involving both variables & 1 & Fourier exchange gives a subrectangular operator with negative horizontal ending grade; strict crossing \\
A pure power of \(y\) & 2, 3 & Negative horizontal ending grade gives a crossing; positive grade gives mass at least ten \\
A pure power of \(x\) & 2, 3, after Fourier exchange & Fourier exchange reduces to the preceding row \\
One distinct nonzero root, both axial endpoints & 4 & Mass at least seventeen \\
One distinct nonzero root, only the starting endpoint axial & 5, 6, after Fourier exchange & Fourier exchange reduces to the following row \\
One distinct nonzero root, only the ending endpoint axial & 5, 6 & Negative horizontal ending grade gives a crossing; positive grade gives mass at least ten \\
Two distinct nonzero roots & 7 & Both endpoints are axial, giving \eqref{eq:4-2} \\
\end{longtable}
}

The endpoint exclusions and the geometric identifications in these rows are part of the cited source reduction. In particular, a zero endpoint grade is excluded there using \cite[Theorem 4.1(3)]{G13}. The Fourier exchange sends each grade to its negative and therefore preserves mass. We use no other change of the polynomial pair in this case reduction.

\Needspace{6\baselineskip}
\begin{proposition}[degree bound]\label{proposition:4-3}

Every counterexample pair satisfies \(\gcd(\deg P,\deg Q)>15\), and hence \(\deg P,\deg Q\ge16\).

\end{proposition} This follows from \cite[Corollary 7.4]{G13}, since the quantity bounded there is the minimum degree gcd over all counterexample pairs.

\subsection{The maximum-root cut and forbidden corner}\label{sec:4.3}

We use the maximum-root cut and the forbidden corner in \cite[Propositions 5.3 and 5.6]{G13}, with the arXiv v3 numbering. Fix a positive integer \(l\). The cut may introduce fractional powers of \(X\), so it takes place in \[
\mathcal A_l=\mathbb C[X^{1/l},X^{-1/l}][Y;d/dX].
\] An \textbf{exact pair} in this ring means a pair satisfying \([Q,P]=1\).

For a direction \((\rho,\sigma)\) with \(\rho>0\), write \(\operatorname{st}_{\rho,\sigma}(P)=(u_0,v_0)\) and put \(z=x^{-\sigma/\rho}y\). There is a polynomial \(f_P(z)\), with nonzero constant coefficient, such that \(\ell_{\rho,\sigma}(P)=x^{u_0}y^{v_0}f_P(z)\). The \textbf{cut polynomial} is \(z^{v_0}f_P(z)\): equivalently, \(\ell_{\rho,\sigma}(P)=x^{u_0+v_0\sigma/\rho}z^{v_0}f_P(z)\). Choose a root \(\lambda_0\) of this polynomial with maximum multiplicity \(M\). With \(l'=\operatorname{lcm}(l,\rho)\), the cut is the automorphism \(\varphi\) of \(\mathcal A_{l'}\) fixing \(X^{1/l'}\) and sending \(Y\) to \(Y+\lambda_0X^{\sigma/\rho}\). Write \(P_+=\varphi(P)\), \(Q_+=\varphi(Q)\). The source permits \(\lambda_0=0\) if zero has maximum multiplicity. Then \(\varphi\) is the identity, and the proposition still supplies a lower shared direction. In our application \(v_0=0\) and all roots of the cut polynomial are nonzero.

The cut theorem requires an exact pair, a shared direction \((\rho,\sigma)\in\operatorname{Dir}(P)\cap\operatorname{Dir}(Q)\), positive weights, vanishing leading bracket, nonintegral weight ratios in both orders, and negative ending grades for both operators. It gives a new shared direction \((\rho',\sigma')\) with \(\rho'>0\) and \(\sigma'/\rho'<\sigma/\rho\), preserving the commutator, positive weights and their ratio. The new ending point is \begin{equation}\label{eq:4-3}
\left(u_0+\frac{(v_0-M)\sigma}{\rho},M\right).
\end{equation} For a polynomial starting pair, \(l=1\) and the cut takes place in \(\mathcal A_\rho\).

The forbidden-corner statement says that, for an exact pair in \(\mathcal A_l\) with a direction \((\rho,\sigma)\in\operatorname{Dir}(P)\cap\operatorname{Dir}(Q)\), positive weights, \(\sigma\le0\), and reduced ratio \(v(Q)/v(P)=n/d\) with coprime \(n,d>1\), one cannot have \begin{equation}\label{eq:4-4}
\frac1d\operatorname{en}(P)
=\left(h_0-\frac1l,h_0\right),\qquad h_0\ge2.
\end{equation} It does not require vanishing of the leading bracket at that direction. We apply at most one cut and verify its hypotheses in Section~\ref{sec:5}.

\section{Exclusion of crossing faces and proof of the main theorem}\label{sec:5}

The negative-direction crossing of Lemma~\ref{lemma:5-1} and the horizontal crossing of Lemma~\ref{lemma:5-2} lead to the same binomial-power face under the six-component bound. We first prove an exclusion for a broader pure-power family; its specialization \(p=q=2\) will close both cases. The remaining Newton configurations are eliminated by their mass or degree bounds.

\begin{proof}[Proof of Theorem~\ref{theorem:1-3}] After reducing the mate, we obtain the normalized endpoint \((q-1/\rho,q)\), prohibited by \eqref{eq:4-4}: directly when \(s=0\), and after one Newton cut when \(s>0\).

\textbf{Leading bracket.} The parameter identity gives \(\rho-s=(s+1)/(q-1)>0\) and \(\gcd(\rho,s)=1\), since every common divisor divides \((q-1)\rho-qs=1\). Put \(R=x(1+\alpha x^s y^\rho)^q\), so the displayed face is \(A=\mu R^p\) of weight \(p\rho\). Let \(B=\ell_{\rho,-s}(Q)\) and \(\omega=v_{\rho,-s}(Q)>0\), using Proposition~\ref{proposition:4-1}. A nonzero \(\{B,A\}\) would be the leading symbol of \([Q,P]\), of weight \(p\rho+\omega-(\rho-s)>0\). Since the commutator is one, \(\{B,A\}=0\).

\textbf{Mate exponent.} The weighted Euler identities are \[
\rho xA_x-syA_y=p\rho A,\qquad
\rho xB_x-syB_y=\omega B.
\] Combining them with \(A_yB_x=A_xB_y\) gives \[
p\rho A B_x=\omega B A_x,\qquad
p\rho A B_y=\omega B A_y.
\] Thus \(B^{p\rho}/A^{\omega}\) is a nonzero constant in \(\mathbb C(x,y)\). Comparison of irreducible-factor orders gives \(\rho\operatorname{ord}_{\pi}B=\omega\operatorname{ord}_{\pi}R\) for every irreducible polynomial \(\pi\). Because \(\operatorname{ord}_xR=1\), the number \(j=\omega/\rho\) is a positive integer. The same comparisons give \begin{equation}\label{eq:5-1}
B=\nu R^j,\qquad \nu\ne0.
\end{equation}

\textbf{Mate descent.} While \(p\mid j\), replace \(Q\) by \(Q-\nu\mu^{-j/p}P^{j/p}\). The replacement is a polynomial mate with the same commutator and generated subalgebra, so it remains a counterexample pair. Its positive integer weight strictly decreases. Proposition~\ref{proposition:4-1} and the Euler argument apply to each resulting counterexample pair, so the descent terminates with \(p\nmid j\). The possibility \(j=1\) is excluded by Proposition~\ref{proposition:4-1} applied to the mate: \(\nu R\) has \(x\)-adic order one and cannot be a proper polynomial power. Thus \(j>1\); primality of \(p\) gives \(\gcd(j,p)=1\), so both weight ratios are nonintegral.

For the reduced mate, the six hypotheses of \cite[Proposition 5.3]{G13} are explicit:

{\def\LTcaptype{none} % do not increment counter
\begin{longtable}[]{@{}>{\raggedright\arraybackslash}p{\dimexpr 0.28\linewidth-2\tabcolsep\relax}>{\raggedright\arraybackslash}p{\dimexpr 0.72\linewidth-2\tabcolsep\relax}@{}}
\toprule\noalign{}
\begin{minipage}[b]{\linewidth}\raggedright
Source hypothesis
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Verification
\end{minipage} \\
\midrule\noalign{}
\endhead
\bottomrule\noalign{}
\endlastfoot
(a) Exact relation & \([Q,P]=1\), preserved by mate subtraction \\
(b) Shared direction & Both leading symbols are nonmonomial powers of \(R\) \\
(c) Positive weights & \(v(P)=p\rho>0\), \(v(Q)=j\rho>0\) \\
(d) Zero leading bracket & The preceding weight and Euler argument \\
(e) Both ratios nonintegral & \(j,p>1\) and \(\gcd(j,p)=1\) \\
(f) Negative ending grades & Endpoints \((p+pqs,pq\rho)\), \((j+jqs,jq\rho)\) have grades \(-p\rho\), \(-j\rho\), since \(q(\rho-s)=\rho+1\) \\
\end{longtable}
}

\textbf{Horizontal direction.} If \(s=0\), then \((q-1)\rho=1\), hence \(q=2\) and \(\rho=1\). The original ending point of \(P\) is \((p,2p)\). Apply \eqref{eq:4-4} directly in \(\mathcal A_1\), with direction \((1,0)\), reduced denominator \(d=p\) and height \(h_0=2\). The normalized endpoint is \((1,2)\), a contradiction. No cut is needed.

\textbf{Negative direction.} Suppose \(s>0\). With cut coordinate \(z=x^{s/\rho}y\), the univariate cut polynomial is \(\mu(1+\alpha z^\rho)^{pq}\). All its roots are nonzero and have multiplicity \(pq\). Formula \eqref{eq:4-3}, applied to starting point \((p,0)\), gives \[
\operatorname{en}_{\rho',\sigma'}(P_+)
=\operatorname{st}_{\rho,-s}(P_+)
=\left(p+\frac{pqs}{\rho},pq\right)
\quad\text{in }\mathcal A_\rho.
\] By \cite[Proposition 5.3(1), (3), (4), (6)]{G13}, the new shared direction has \(\rho'>0\) and \(\sigma'/\rho'<-s/\rho<0\). The corner hypotheses are therefore satisfied:

{\def\LTcaptype{none} % do not increment counter
\begin{longtable}[]{@{}>{\raggedright\arraybackslash}p{\dimexpr 0.3\linewidth-2\tabcolsep\relax}>{\raggedright\arraybackslash}p{\dimexpr 0.7\linewidth-2\tabcolsep\relax}@{}}
\toprule\noalign{}
\begin{minipage}[b]{\linewidth}\raggedright
Corner hypothesis
\end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
Verification after the cut
\end{minipage} \\
\midrule\noalign{}
\endhead
\bottomrule\noalign{}
\endlastfoot
Exact pair in \(\mathcal A_l\) & \(l=\rho\); the cut preserves \([Q_+,P_+]=1\) \\
Shared direction and positive weights & \cite[Proposition 5.3(1), (3), (4)]{G13} \\
Nonpositive second coordinate of the direction & \(\sigma'/\rho'<-s/\rho<0\) and \(\rho'>0\) \\
Reduced ratio, both entries greater than one & \(n/d=j/p\), with \(j,p>1\) coprime \\
Prohibited endpoint & Height \(h_0=q\ge2\), as computed below \\
\end{longtable}
}

Since \((q-1)\rho=qs+1\), normalization by the actual reduced denominator \(p\) gives \[
\frac1p\operatorname{en}_{\rho',\sigma'}(P_+)
=\left(1+\frac{qs}{\rho},q\right)
=\left(q-\frac1\rho,q\right),
\] contrary to \eqref{eq:4-4}. \end{proof}

The prime hypothesis is used to obtain the reduced denominator \(p\). For a composite outer exponent, a surviving mate exponent can have a common factor, or make the reciprocal ratio integral; the same corner argument then need not apply. In particular, Theorem~\ref{theorem:1-3} does not assert an exclusion for every pure-power face. Its case \(p=q=2\), \(s=1\) excludes the configuration in \cite[Remark 4.4]{G24}.

\Needspace{6\baselineskip}
\begin{lemma}[negative crossing]\label{lemma:5-1}

A counterexample pair with \(m(P)\le6\) has no strict crossing in a direction \((\rho,-s)\) with coprime integers \(\rho>s\ge1\).

\end{lemma}

\begin{proof} Proposition~\ref{proposition:4-1} and the starting grade give \[
\ell_{\rho,-s}(P)=\mu R^k,\qquad
R=x^a y^b r(w),\quad w=x^s y^\rho,
\quad k\ge2,\quad a>b\ge0.
\] The integral points on the weight line differ by multiples of \((s,\rho)\); extracting its first monomial gives this form. The face has at least two monomials, so \(r\) is nonconstant. Absorbing its nonzero constant coefficient into the scalar normalizes \(r(0)=1\). Every nonnegative integral solution of \(\rho i-sj=\rho-s\) has the form \((i,j)=(1+sn,1+\rho n)\), \(n\ge0\). Thus the homogeneous companion in \eqref{eq:4-1} is \(F=xyf(w)\).

Put \(H=a-b\), \(W=\rho a-sb\), and \(\delta=\rho-s\). The equation \(\{R,F\}=R\) becomes \begin{equation}\label{eq:5-2}
\delta wf r'-(Hf+Wwf'+1)r=0.
\end{equation} Here \(f(0)=-1/H\). If \(f\) were constant, \eqref{eq:5-2} would give \(\delta wf r'=0\), contradicting the nonconstancy of \(r\). With \(e=\deg r\) and \(L=\deg f\), degree comparison gives \(\delta e=H+WL\). Every root of \(r\) is a simple root of \(f\), by the same local order comparison as in Lemma~\ref{lemma:3-1}. If \(M\) is the largest root multiplicity of \(r\), then \[
e\le ML,\qquad M\ge e/L>W/\delta>a.
\] The final inequality follows from \(W/\delta=a+s(a-b)/\delta>a\), since \(a>b\), \(s>0\), and \(\delta>0\).

A root of \(r^k\) of multiplicity \(kM\), together with Lemma~\ref{lemma:2-1} and the grade count of Section~\ref{sec:4}, yields \[
6\ge m(P)\ge t(r^k)\ge kM+1\ge k(a+1)+1.
\] Therefore \(k=2\), \(a=1\), \(b=0\), and \(M=2\). Equation \eqref{eq:5-2} is now \eqref{eq:1-1}, with \(t(r^2)\le6\). Theorem~\ref{theorem:1-2} gives \(r=(1-\lambda w)^2\) and \(\rho=2s+1\). The face is therefore \eqref{eq:1-3} with \(p=q=2\) and \(\alpha=-\lambda\), excluded by Theorem~\ref{theorem:1-3}. \end{proof}

\Needspace{6\baselineskip}
\begin{lemma}[horizontal crossing]\label{lemma:5-2}

A counterexample pair with \(m(P)\le6\) has no strict crossing in direction \((1,0)\).

\end{lemma}

\begin{proof} Proposition~\ref{proposition:4-1} gives \begin{equation}\label{eq:5-3}
\ell_{1,0}(P)=\mu(x^ag(y))^k,\qquad F=xf(y),
\qquad fg'-af'g=g.
\end{equation} Here \(g,f\in\mathbb C[y]\), with \(g\ne0\), and \(k\ge2\). The crossing condition is \(\operatorname{ord}_0g<a<\deg g\), so \(a\ge1\) and \(g\) is nonconstant. At a root \(\beta\) of \(g\) of multiplicity \(j\), local order comparison gives a simple root of \(f\) and \begin{equation}\label{eq:5-4}
(j-a)f'(\beta)=1.
\end{equation} In particular, no root of \(g\) has multiplicity \(a\).

A constant \(f=c\) would give \(cg'=g\), which is impossible for a nonzero polynomial \(g\). If \(\deg f=1\), all roots of \(g\) lie at its single root and have total multiplicity \(\deg g>a\). If \(\deg f\ge2\), degree comparison in \eqref{eq:5-3} gives \(\deg g=a\deg f\); root containment then gives a root of multiplicity at least \(a\), hence at least \(a+1\) by \eqref{eq:5-4}. Such a root is nonzero because \(\operatorname{ord}_0g<a\).

The grade count of Section~\ref{sec:4} therefore gives \(k(a+1)+1\le6\), forcing \(k=2\) and \(a=1\). Also \(g(0)\ne0\), since \(\operatorname{ord}_0g<a=1\). Lemma~\ref{lemma:2-1} bounds all root multiplicities of \(g\) by two, and \eqref{eq:5-4} excludes simple roots. Write \(g=ch^2\) with \(h\) squarefree, and write \(f=h\kappa\) by root containment. Equation \eqref{eq:5-3} reduces to \begin{equation}\label{eq:5-5}
\kappa h'-h\kappa'=1.
\end{equation} Equation \eqref{eq:5-5} ensures that \(\kappa\) is nonzero and is not a scalar multiple of \(h\). If \(\deg h\ne\deg\kappa\), the degree of the left side is \(\deg h+\deg\kappa-1\), so, since \(h\) is nonconstant, \(\deg h=1\) and \(\deg\kappa=0\). If the degrees are equal, subtract a scalar multiple of \(h\) from \(\kappa\). The new \(\kappa\) is nonzero and has smaller degree; equation \eqref{eq:5-5} is unchanged, so the unequal-degree argument applies. In either case \(\deg h=1\), so \(g=ch^2\) has a single double root. Thus \(g=c'(1+\alpha y)^2\), \(c'\alpha\ne0\). The leading face is \eqref{eq:1-3} with \(p=q=2\) and \(s=0\), again excluded by Theorem~\ref{theorem:1-3}. \end{proof}

\begin{proof}[Proof of Theorem~\ref{theorem:1-1}] First take \(K=\mathbb C\). Suppose that a counterexample pair has \(m(P)\le6\). Apply Proposition~\ref{proposition:4-2}, using the mass-preserving Fourier exchange if necessary. For its crossing alternative, \(\sigma<0\) gives \(\rho>s=-\sigma\ge1\), covered by Lemma~\ref{lemma:5-1}; if \(\sigma=0\), coprimality forces \((\rho,\sigma)=(1,0)\), covered by Lemma~\ref{lemma:5-2}. Its mass bound ten is incompatible with the hypothesis.

It remains to consider \eqref{eq:4-2}. Put \(D=\deg P=u+v\). Proposition~\ref{proposition:4-3} gives \(D\ge16\). The polynomial \((z-\alpha)^u(z-\beta)^v\) has a nonzero root of multiplicity at least \(\lceil D/2\rceil\), and so has at least \(\lceil D/2\rceil+1\ge9\) terms by Lemma~\ref{lemma:2-1}. These are distinct grades on the total-degree face. Hence \(m(P)\ge9\), the final contradiction.

All cases are excluded over \(\mathbb C\).

Now let \(K\) be any characteristic-zero field and let \(P,Q\) satisfy the hypotheses of the theorem. Let \(K_0\) be the subfield of \(K\) generated over \(\mathbb Q\) by their finitely many coefficients. This finitely generated field embeds in \(\mathbb C\): map a finite transcendence basis to algebraically independent complex numbers and extend the embedding across the remaining finite algebraic extension. Identify \(K_0\) with its image under this embedding. The embedded operators have the same masses and satisfy the same commutator relation. The complex case just proved makes each of \(X,Y\) a complex linear combination of finitely many words in the embedded \(P,Q\).

Fix the words appearing in such an expression for \(X\) and expand them in the PBW basis. Equating the coefficients to those of \(X\) is a finite linear system over \(K_0\). Its coefficient and augmented matrix ranks are unchanged on extending scalars to \(\mathbb C\). Solvability over \(\mathbb C\) therefore implies solvability over \(K_0\), so \(X\in K_0\langle P,Q\rangle\). The same argument applies to \(Y\). Returning through the coefficient embedding and extending scalars from \(K_0\) to \(K\) proves the conclusion. \end{proof}

\section{The boundary of the scalar classification}\label{sec:6}

Several elementary examples delimit the scalar argument. First, \[
(\rho,s)=(2,1),\qquad r=(1-w)^3,\qquad f=w-1
\] satisfies \eqref{eq:1-1} and has \(t(r^2)=7\). Thus Theorem~\ref{theorem:1-2} cannot be extended to seven terms with the same conclusion. Nevertheless, Theorem~\ref{theorem:1-3} with \(p=2,q=3,s=1,\alpha=-1\) excludes the associated face \(\mu x^2(1-xy^2)^6\) from any counterexample pair. The scalar equation alone misses this geometric obstruction.

With seven terms, the equal-modulus conclusion of Lemma~\ref{lemma:2-2} fails. The polynomial \[
\begin{aligned}
(1+\sqrt{-3}\,w+w^2)^4
={}&1+4\sqrt{-3}\,w-14w^2-21w^4\\
&{}-14w^6+4\sqrt{-3}\,w^7+w^8
\end{aligned}
\] has two roots of multiplicity four with different absolute values.

Primitivity is essential: \((1-w^3)^4(1+2w^3)^2\) has six terms and three roots of multiplicity four. The differential equation excludes this imprimitive possibility through \eqref{eq:3-1} and formal uniqueness.

Integrality also enters the scalar theorem: with \((\rho,s)=(5/2,1)\), the polynomials \(r=(1+w^2)^2\) and \(f=-(1+w^2)\) satisfy \eqref{eq:1-1}. Here \(r\) has two double roots, at \(w=i\) and \(w=-i\), a possibility excluded by Theorem~\ref{theorem:1-2} for integer parameters. The seven-term example proves sharpness of the scalar classification, not optimality of the six-component generation theorem. The pure-power exclusion disposes of this particular face, but does not classify all seven-component configurations. Appendix~\ref{sec:A} records two scalar families for which the coefficient method remains effective.

\textbf{Formal verification.} The Lean development \cite{S26} realizes the Weyl algebra as polynomial differential operators, proves its equivalence with the generators-and-relations presentation, and identifies mass with the number of occupied PBW grades. The six inputs are the opposite-grade and homogeneous-companion conclusions of Proposition~\ref{proposition:4-1}, the case reduction of Proposition~\ref{proposition:4-2}, the degree bound of Proposition~\ref{proposition:4-3}, the maximum-root cut followed by the corner exclusion, and the polynomial corner exclusion \eqref{eq:4-4}. They are proved within the development; the exported theorem has no hypothesis assuming those inputs. The declaration \texttt{Dixmier.Palomar.massSixGeneration} passed comparison with the reference Lean statement and the Lean, nanoda and con-ron kernel checks in the official verification recorded in \cite{S26}. The permitted axioms are \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound}. The formalization is registered as Palomar entry PALOMAR-2026-10-05-000006, version 2; its versioned source and verification record are given in \cite{S26}.

\appendix

\section{Coefficient nonvanishing in two scalar families}\label{sec:A}

The sign induction in Section~\ref{sec:3} forces coefficient nonvanishing in two further scalar families. Proposition~\ref{proposition:A-2} treats polynomials with no simple roots and one additional root of the companion. Proposition~\ref{proposition:A-3} treats three double roots and two simple roots, with no additional companion roots. Both give exact monomial counts for every positive integer power. Neither is needed for Theorem~\ref{theorem:1-1}. Throughout this appendix, \(r,f\) satisfy \eqref{eq:1-1}, \(r(0)=1\), and \(\rho>s\ge1\) are integers. Assume that every root of \(r\) has multiplicity at most two, with at least one double root.

\Needspace{6\baselineskip}
\begin{proposition}[factor equation]\label{proposition:A-1}

There are squarefree pairwise coprime polynomials \(A,B,C\), normalized by \(A(0)=B(0)=1\), \(C(0)=-1\), such that \[
 r=AB^2,\qquad f=ABC.
\] Here \(B\) records the double roots, \(A\) the simple roots, and \(C\) the roots of \(f\) that do not occur in \(r\). Put \[
 a=\deg A,\quad D=\deg B,\quad c=\deg C,\quad h=\rho-2s.
\] Then \(h\) is a positive integer and \begin{equation}\label{eq:A-1}
wC(hAB'-sA'B)-AB(\rho wC'+C)=1,\qquad
 hD=sa+\rho c+1.
\end{equation}

\end{proposition}

\begin{proof} Root containment and simplicity of the roots of \(f\) follow from Lemma~\ref{lemma:3-1}. They give the stated factorization, with the normalization fixed by the constant coefficients. Set \(e=\deg r\), \(L=\deg f\), \(\delta=\rho-s\). Root multiplicities at most two give \(e\le2L\). Since \(\delta e=1+\rho L\), it follows that \((\rho-2s)L\ge1\), so \(h>0\). Substituting the factorization in \eqref{eq:1-1} and canceling \(AB^2\) gives the first identity in \eqref{eq:A-1}. Its leading coefficient, or equivalently \(e=a+2D\) and \(L=a+D+c\) in the degree identity, gives the second. \end{proof}

\Needspace{6\baselineskip}
\begin{proposition}[no simple root and one root of \(f\) outside \(r\), all degrees]\label{proposition:A-2}

Suppose the hypotheses of Proposition~\ref{proposition:A-1} hold with \(A=1\), \(D\ge2\), and \(c=1\). Then \(h>1\), and after scaling \(C=w-1\), the coefficients \(B=\sum_{n=0}^D b_nw^n\) satisfy \[
 b_0=1,\qquad
 b_n=-\frac{h(D-n+1)}{hn-1}b_{n-1}\quad(1\le n\le D).
\] Consequently, for every integer \(k\ge1\), \[
 t(r^k)=2Dk+1,\qquad r=B^2.
\] In particular no member of this family has \(t(r^2)=7\).

\end{proposition}

\begin{proof} The degree equation gives \(hD=\rho+1\). Scaling is permitted because the linear coefficient of \(C\) is nonzero. The scalar equation is \[
 hw(w-1)B'-((\rho+1)w-1)B=1.
\] Its degree-\(n\) coefficient gives the displayed recurrence. When \(h=1\), the degree-one equation is \(0=-D\), impossible since \(D\ge2\). In the present integer parameter domain \(h>0\), therefore \(h>1\). Every recurrence multiplier is strictly negative. Thus \((-1)^n b_n>0\) for all \(0\le n\le D\). All products contributing to a coefficient of \(B^{2k}\) have the same sign, and every degree from zero to \(2Dk\) occurs. Hence no coefficient can cancel. This proves the assertion for arbitrary \(D\) and \(k\). \end{proof}

\Needspace{6\baselineskip}
\begin{proposition}[three double roots and two simple roots, every slope]\label{proposition:A-3}

Suppose the hypotheses of Proposition~\ref{proposition:A-1} hold with \((D,a,c)=(3,2,0)\). Then after scaling, \(A\) and \(B\) have strictly positive coefficients. For every integer \(k\ge1\), \(t(r^k)=8k+1\). In particular \(t(r^2)=17\), so the case \((D,a,c)=(3,2,0)\) cannot occur under the additional bound \(t(r^2)\le7\), for any admissible integer pair \(\rho>s\ge1\).

\end{proposition}

\begin{proof} The degree equation gives \(2s+1=3h\). Write \(A=1+uw+vw^2=\sum_{i=0}^2 a_iw^i\), \(C=-1\), and \(B=\sum_{n=0}^3 b_nw^n\), with \(b_0=1\) and \(v\ne0\). If \(h=1\), then \(s=1\), \(\rho=3\), and \eqref{eq:A-1} becomes \[
-w(AB'-A'B)+AB-1=0.
\] Its coefficients of degrees one through four are \[
2u,\qquad b_1u-b_2+3v,\qquad 2b_1v-2b_3,\qquad b_2v-b_3u.
\] The first three equations give \(u=0\), \(b_2=3v\), and \(b_3=b_1v\). The fourth then gives \(3v^2=0\), a contradiction. Thus \(h>1\). The coefficient recurrence is \[
 (hn-1)b_n=\sum_{i=1}^{\min(n,2)}(1+si-h(n-i))a_i b_{n-i}.
\] If \(u=0\), all odd coefficients through degree three vanish, contrary to \(\deg B=3\). Normalize \(u=1\). The first three equations give \[
\begin{aligned}
b_1&=\frac{3h+1}{2(h-1)},\\
b_2&=\frac{12h(h-1)v+3h^2+4h+1}{4(h-1)(2h-1)},\\
b_3&=\frac{(h+1)(4h(9h-5)v-(h-1)(3h+1))}
             {8(h-1)(2h-1)(3h-1)}.
\end{aligned}
\] The remaining coefficient equations give the residual \(w^4\phi_h(v)/(16(2h-1))\), where \[
 \phi_h(v)=48h^2v^2-24h(h+1)v+3h^2+4h+1.
\] Its discriminant is \(384h^2(h+1)>0\), and its two roots are positive. To prove \(b_3>0\) for both roots, put \[
 \tau=\frac{(h-1)(3h+1)}{4h(9h-5)},\qquad
 v_*=\frac{h+1}{4h}.
\] Here \(v_*\) is the vertex coordinate, and \[
 v_*-\tau=\frac{3h^2+3h-2}{2h(9h-5)}>0,\qquad
 \phi_h(\tau)=\frac{2(2h-1)(3h+1)^3}{(9h-5)^2}>0.
\] Since the upward-opening quadratic has two distinct real roots, these inequalities put \(\tau\) strictly below its smaller root. Hence \(v>\tau\), so \(b_3>0\); the displayed formulas also give \(b_1,b_2>0\). All coefficients of \(A,B\) are positive, and their powers have a nonzero coefficient in every degree. \end{proof}

For \(D\ge2\), Proposition~\ref{proposition:A-2} gives \(t(r^2)=4D+1\ge9\), while Proposition~\ref{proposition:A-3} gives \(t(r^2)=17\). Thus both factor families are excluded whenever the relevant face has at most seven terms. The first exclusion is uniform in root degree, and the second is uniform in the slope parameters for the stated factor degrees.

These term counts also give mass bounds when a positive-sum face has the specified form \[
\ell_{\rho,-s}(P)=\mu x^u y^v r(x^s y^\rho)^k,
\] where \(u,v\) are nonnegative integers, \(k\ge2\) is an integer, \(\mu\ne0\), and \(r,f\) satisfy \eqref{eq:1-1} and the respective proposition's hypotheses. The grade count of Section~\ref{sec:4} gives \(m(P)\ge2Dk+1\ge4D+1\ge9\) in Proposition~\ref{proposition:A-2}, and \(m(P)\ge8k+1\ge17\) in Proposition~\ref{proposition:A-3}. The face form and normalized scalar equation are hypotheses in these conclusions.

For more general factors, complex coefficients can permit cancellation. A scalar solution alone does not determine whether a polynomial Weyl mate exists.

\section*{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.

\begin{thebibliography}{BCW82}
\small
\raggedright
\bibitem[D68]{D68} J. Dixmier, \emph{Sur les algèbres de Weyl}, Bulletin de la Société Mathématique de France \textbf{96} (1968), 209--242. \href{https://www.numdam.org/articles/10.24033/bsmf.1667/}{DOI: 10.24033/bsmf.1667}.

\bibitem[Ga26]{Ga26} S. Gao, \emph{Counterexamples to the Jacobian conjecture in dimensions greater than two}, arXiv:2608.00222v1 (2026), preprint. \href{https://arxiv.org/abs/2608.00222v1}{Versioned record}.

\bibitem[T26]{T26} T. Tao, \emph{A digestion of the Jacobian conjecture counterexample}, What's New, 21 July 2026, online exposition. \href{https://terrytao.wordpress.com/2026/07/21/a-digestion-of-the-jacobian-conjecture-counterexample/}{Article}.

\bibitem[BCW82]{BCW82} H. Bass, E. H. Connell and D. Wright, \emph{The Jacobian conjecture: reduction of degree and formal expansion of the inverse}, Bulletin of the American Mathematical Society (N.S.) \textbf{7} (1982), no. 2, 287--330. \href{https://doi.org/10.1090/S0273-0979-1982-15032-7}{DOI: 10.1090/S0273-0979-1982-15032-7}.

\bibitem[BK07]{BK07} A. Belov-Kanel and M. Kontsevich, \emph{The Jacobian Conjecture is stably equivalent to the Dixmier Conjecture}, Moscow Mathematical Journal \textbf{7} (2007), no. 2, 209--218. \href{https://arxiv.org/html/math/0512171v2}{arXiv:math/0512171v2}.

\bibitem[BL20]{BL20} V. V. Bavula and V. Levandovskyy, \emph{A remark on the Dixmier Conjecture}, Canadian Mathematical Bulletin \textbf{63} (2020), 6--12. \href{https://doi.org/10.4153/S0008439519000122}{DOI: 10.4153/S0008439519000122}. \href{https://arxiv.org/abs/1812.00042v1}{arXiv:1812.00042v1}.

\bibitem[HT24]{HT24} G. Han and B. Tan, \emph{Some progress in the Dixmier conjecture for \(A_1\)}, Communications in Algebra \textbf{52} (2024), no. 5, 2033--2051. \href{https://doi.org/10.1080/00927872.2023.2280189}{DOI: 10.1080/00927872.2023.2280189}. Result numbering refers to \href{https://arxiv.org/html/2210.00257v1}{arXiv:2210.00257v1}.

\bibitem[G24]{G24} J. A. Guccione, J. J. Guccione and C. Valqui, \emph{Number of homogeneous components of counterexamples to the Dixmier conjecture}, Communications in Algebra \textbf{53} (2025), no. 3, 1307--1319. \href{https://doi.org/10.1080/00927872.2024.2407991}{DOI: 10.1080/00927872.2024.2407991}. Theorem numbering refers to \href{https://arxiv.org/html/2402.11135v1}{arXiv:2402.11135v1}.

\bibitem[Z26]{Z26} A. Zheglov, \emph{The Conjecture of Dixmier for the first Weyl algebra is true}, arXiv:2410.06959v5 (2026), preprint. \href{https://arxiv.org/abs/2410.06959v5}{Versioned record}.

\bibitem[S26]{S26} I. A. Shaik, \emph{The rank-one Dixmier conjecture for elements of mass at most six}, Lean 4 formalization (2026), Palomar entry PALOMAR-2026-10-05-000006, version 2, MIT license. \href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-05-000006&version=2}{Registered formalization}. \href{https://github.com/shaikidris/DixmierMassSix-Palomar/tree/61783d52b6ae44cd2d8d20ad6cb798e7bbbce3ff}{Versioned source}. \href{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/37353942411}{Official verification}.

\bibitem[Bri01]{Bri01} B. Brindza, \emph{Remarks on the number of non-zero coefficients of polynomials}, Acta Mathematica Academiae Paedagogicae Nyíregyháziensis (N.S.) \textbf{17} (2001), no. 2, 77--79. \href{https://www.emis.de/journals/AMAPN/vol17_2/5.html}{Journal archive}.

\bibitem[M07]{M07} S. Mattarei, \emph{Root multiplicities and number of nonzero coefficients of a polynomial}, Journal of Algebra and Its Applications \textbf{6} (2007), no. 3, 469--475. \href{https://doi.org/10.1142/S0219498807002338}{DOI: 10.1142/S0219498807002338}. \href{https://arxiv.org/html/math/0512239v2}{arXiv:math/0512239v2}.

\bibitem[G13]{G13} J. A. Guccione, J. J. Guccione and C. Valqui, \emph{The Dixmier conjecture and the shape of possible counterexamples}, Journal of Algebra \textbf{399} (2014), 581--633. \href{https://doi.org/10.1016/j.jalgebra.2013.10.011}{DOI: 10.1016/j.jalgebra.2013.10.011}. Theorem numbering refers to \href{https://arxiv.org/html/1111.6100v3}{arXiv:1111.6100v3}.

\end{thebibliography}
\end{document}