Prove2Me

Collapsibility of depressed cubics beyond the norm-form case

Open
CollapsibleCubics.depressed_cubic_collapsible_of_not_normForm_repr

by miao · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraalgebraic-numbersnumber-theorypolynomials

Let β∈C\beta\in\mathbb C be algebraic of degree three, and write its monic minimal polynomial as

mβ(X)=X3+dX+e.m_{\beta}(X)=X^3+dX+e.

Assume that the Eisenstein norm form does not represent the negative linear coefficient:

∄r,s∈Q,r2+rs+s2=−d.\nexists r,s\in\mathbb Q,\qquad r^2+rs+s^2=-d.

The theorem asserts that β\beta is collapsible: some nonconstant polynomial over Q\mathbb Q, split completely into rational linear factors, takes β\beta to a rational value.

This is the depressed-cubic normal form of the unresolved half of the one-step cubic collapsibility problem. It removes the inessential quadratic coefficient while retaining exactly the arithmetic obstruction that rules out a collapsing polynomial of degree three. It is intended as the normalized core used after the mission's proved affine-invariance theorem.

Formalization Note The equation “depressed” is expressed by (minpoly ℚ β).coeff 2 = 0; then dd is (minpoly ℚ β).coeff 1. The explicit integrality and degree-three hypotheses match the parent theorem's setting.

Preamble
import Definitions.Def_CollapsibleCubics_basic
Formal statement
namespace CollapsibleCubics
theorem depressed_cubic_collapsible_of_not_normForm_repr (α : ℂ)
    (hint : IsIntegral ℚ α)
    (hdeg : (minpoly ℚ α).natDegree = 3)
    (hdepressed : (minpoly ℚ α).coeff 2 = 0)
    (hrep : ¬ ∃ r s : ℚ, r ^ 2 + r * s + s ^ 2 = -(minpoly ℚ α).coeff 1) :
    Collapsible α := by sorry
end CollapsibleCubics
Source
Normal-form specialization of Miles, *On collapsible algebraic numbers*, 2026-08-20, section ‘The cubic case’ (Affine invariance and Cubic criterion), https://quesswho.github.io/miles-blog/2026/08/20/collapsible/; introduced as the depressed-cubic core of Prove2Me theorem CollapsibleCubics.cubic_collapsible_of_not_normForm_repr (faff93b8-3d73-4841-b243-fe24b2bed4e1).

View graph