Cubic collapsibility when every collapsing polynomial has degree $\ge 4$

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 honest residue. It asserts the parent's conclusion for the cubics that the sibling node CollapsibleCubics.cubic_collapsible_of_normForm_repr does not cover: those for which $-d = a^{2}/3 - b$ is not represented over $\mathbb{Q}$ by $x^{2}+xy+y^{2}$. By the equivalence derived above, the hypothesis says precisely:

Be clear about what the split does and does not buy. The sibling half is provable, so this node is logically equivalent to the parent, not weaker than it. The split does not reduce the problem; it locates it. What a solver gains is the extra hypothesis, and that hypothesis is usable in the strong sense: it is a concrete arithmetic condition on the two top coefficients of the minimal polynomial, checkable at sight, and it rules out the entire low-degree search in one line rather than by exhaustion.

Where the mission's own machinery lives. Since $x^{2}+xy+y^{2}$ is positive definite, every cubic whose depressed form has $d > 0$ satisfies this hypothesis. That includes $x^{3}+6x+1$ — the smallest cubic still resisting, the subject of CollapsibleCubics.collapsible_x3_6x_1 — where $d = 6$ and the mission's proved archimedean bound CollapsibleCubics.pi_div_psi_le_natDegree sharpens $\deg f \ge 4$ all the way to $\deg f \ge 32$. The totally real cubics ($\Delta > 0$, so $d < 0$) split between the two halves according to whether $-d$ is a norm from $\mathbb{Q}(\sqrt{-3})$: the first genuinely non-archimedean obstruction available on this mission, and the place where CollapsibleCubics.even_card_roots_between applies.

Non-vacuity, checked and not asserted. This half is inhabited, and the witness is machine-checked in Lean: a root of $x^{3}+x+1$ has minimal polynomial $x^{3}+x+1$ (irreducibility via the rational root theorem), hence $a = 0$, $b = 1$, hence $a^{2}/3 - b = -1$, which $\rho^{2}+\rho\sigma+\sigma^{2} \ge 0$ never equals. So this is not a conjecturally empty case. The complementary half is inhabited by a root of $x^{3}-2$.

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. The negated existential is written inline, in exactly the same words as the positive form in the sibling node, so that the two halves are visibly complementary. Nothing here asserts that a collapsing polynomial of degree $\ge 4$ exists; as on the parent, a disproof — a cubic admitting no split $f$ at all — would refute the general conjecture, and this node should not be assumed true.