Cubic collapsibility when $a^2/3-b$ is represented by $x^2+xy+y^2$

Let $\alpha \in \mathbb{C}$ be an algebraic number of degree $3$ and write its monic minimal polynomial over $\mathbb{Q}$ as

Where the degree-$3$ case sits. Suppose $f$ is split — degree $\ge 1$, nonzero rational leading coefficient, all roots rational — and $f(\alpha) = k \in \mathbb{Q}$. Then $m \mid f - k$. A nonzero polynomial of degree $1$ or $2$ cannot be divisible by the cubic $m$, and $f - k$ is nonzero because $\deg f \ge 1$; so no collapsing polynomial has degree $1$ or $2$. If $\deg f = 3$ then $f - k = \lambda m$ with $\lambda$ the leading coefficient of $f$, so $\lambda^{-1} f = m + k'$ is a monic split cubic for some $k' \in \mathbb{Q}$; conversely any monic split cubic congruent to a constant modulo $m$ collapses $\alpha$. Hence

Substituting $r_i = \rho_i - a/3$ removes the quadratic term and the two conditions collapse to a single one: writing $\rho_1 = \rho$, $\rho_2 = \sigma$, $\rho_3 = -(\rho+\sigma)$,

The left-hand side is the norm form of $\mathbb{Q}(\sqrt{-3})$ — the norm form of the Eisenstein integers $\mathbb{Z}[\omega]$. The right-hand side is $-d$, where $x^{3} + dx + e$ is the depressed cubic obtained from $m$ by $x \mapsto x - a/3$. So the hypothesis below says exactly: $-d$ is represented over $\mathbb{Q}$ by $x^{2}+xy+y^{2}$, equivalently (classically) $-d$ is a norm from $\mathbb{Q}(\sqrt{-3})$, equivalently $-d \ge 0$ and every prime $p \equiv 2 \pmod 3$ occurs in $-d$ to an even exponent. Since the form is positive definite, $d \le 0$ is necessary; in particular every totally real cubic ($\Delta = -4d^{3}-27e^{2} > 0$ forces $d < 0$) passes the sign test, and every cubic with $d > 0$ fails it outright.

This statement — the reachable half. It asserts that when the representation exists, $\alpha$ is collapsible. The proof is short and constructive, and is given here in full so that the reader can judge the split rather than take it on trust. Given $\rho,\sigma \in \mathbb{Q}$ with $\rho^{2}+\rho\sigma+\sigma^{2} = a^{2}/3 - b$, put

Then $e_1(r) = -a$ and $e_2(r) = b$ by the computation above, so $f = x^{3} + a x^{2} + b x - e_3(r) = m - \bigl(c + e_3(r)\bigr)$, and therefore

while $f$ is split by construction with $\deg f = 3 > 0$. The Lean work is the packaging: the multiset of roots demanded by IsSplit, the degree of a product of three monic linear factors, and the symmetric-function identity.

What this half is worth. It is genuinely easier than the parent, not merely weaker — the argument above is complete. What it retires is the region of cubics that collapse in degree $3$; by the equivalence above that is exactly the region where a collapsing polynomial of degree $\le 3$ exists at all. Examples: any $\alpha$ with $\alpha^{3} \in \mathbb{Q}$ (take $\rho = \sigma = 0$, $f = x^{3}$), and, less trivially, the root of $x^{3}-3x+10$, where $\rho = \sigma = 1$ gives $f = (x-1)^{2}(x+2) = m - 8$.

Non-vacuity, checked and not asserted. Both halves of this split are inhabited, and both witnesses are machine-checked in Lean (including the irreducibility of the two cubics, via the rational root theorem). A root of $x^{3}-2$ satisfies this hypothesis ($a=b=0$, take $\rho=\sigma=0$); a root of $x^{3}+x+1$ satisfies its negation ($a=0$, $b=1$, so $a^{2}/3-b = -1 < 0$, which the positive-definite form never represents), and is the subject of the sibling node CollapsibleCubics.cubic_collapsible_of_not_normForm_repr.

Formalization note. The hypothesis IsIntegral ℚ α is carried over verbatim from the parent so that the case split typechecks against it; it is redundant, since (minpoly ℚ α).natDegree = 3 already forces it (a non-integral element has minimal polynomial $0$). The coefficients $a$ and $b$ appear as (minpoly ℚ α).coeff 2 and (minpoly ℚ α).coeff 1; the division by $3$ is division in $\mathbb{Q}$. The hypothesis is stated inline rather than through a new definition, in exactly the same words as in the sibling node, so that the two halves are visibly complementary.