A polynomial is split if and for some and . Split polynomials are the simplest non-constant maps defined over that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into .
Say is -collapsible if there are split with , collapsible if it is -collapsible, and eventually collapsible if it is -collapsible for some . Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree : Jordi Ribes settled the cubic case of eventual collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is . For the one-step notion the picture is different — degrees and are settled, and degree is open. That one-step cubic case is this mission's goal.
Let be an algebraic number with . After an affine change of variable over one may assume is a root of a depressed cubic
with discriminant . When the cubic is totally real (three real roots); when it has one real root and a complex-conjugate pair. In the latter case write the roots as
and set , the parameter that controls the archimedean obstruction below. Scaling sends , so the single rational invariant
determines the problem up to scaling: the search space is one rational parameter, not two.
This is the weakest statement that settles the case: it fixes no bound on , and asserts only that some split exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.
The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:
The mission also carries, as a plain theorem rather than a milestone, the single open instance — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.
A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree . A disproof would be at least as informative: a single cubic admitting no split with would separate -collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.
The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing , and it is what rules out a uniform-degree approach.
Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are not proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance and the goal itself are open.
The obvious approach is to write down a split with rational roots and force by solving for the roots. This works when is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.
Suppose and is split with . Irreducibility of forces to be divisible by , hence , hence . Each factor lies on a fixed circle through and determined by , and a convexity argument on then forces
As one has , so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For the bound already gives , which is why that cubic resists the searches that settle its neighbours.
Only one step of this argument is special to cubics: the identification of the circle parameter as . For an algebraic number of any degree with a real conjugate and a non-real conjugate , irreducibility gives the same relation , the images again lie on a circle through and , and the parameter is , which specialises to in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.
In the totally real case () the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of . Whether degrees stay bounded there is itself unsettled.
Representation. IsSplit f says and for a nonzero rational and a multiset of rationals; multiplicities are therefore allowed and the roots need not be distinct. Collapsible α is stated for in an arbitrary field carrying a -algebra structure, not only for , so the results apply verbatim to a root in , in , or in . The goal theorem is stated over , with "cubic" expressed as .
Ruling out a trivialisation. Collapsible places no lower bound on and does not require the value to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: would make , impossible for an irreducible cubic dividing a polynomial that splits over . Constant is excluded by . Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.
Conventions in the archimedean milestones. In the cubic bound the parameters enter as real numbers satisfying the factorisation identity, with the normalisation ; this is not a restriction, since is determined only up to sign and the sign may be chosen. Under it , and the conclusion is with the natural-number degree.
In the general bound the corresponding normalisation is . It forces , so is genuinely non-real and , hence and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when , which the hypothesis excludes and which cannot occur for a depressed cubic with . No degree hypothesis on is needed: possessing both a real and a non-real root already forces .
Infrastructure. A complete development needs Polynomial, Multiset, minpoly, and for the archimedean bound Real.arctan, Complex.arg, and strict concavity of on . The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of of any degree.
import Definitions.Def_CollapsibleCubics_basic
namespace CollapsibleCubics
theorem cubic_collapsible (α : ℂ) (hint : IsIntegral ℚ α)
(hdeg : (minpoly ℚ α).natDegree = 3) :
Collapsible α := by sorry
end CollapsibleCubicsLet be an algebraic number of degree over , that is, an algebraic number whose minimal polynomial over has degree . The claim is that is collapsible: there exists a split polynomial — one of degree at least that factors as with and every — and a rational number with
This is the first open case of the conjecture that every algebraic number is collapsible. Degrees and are settled. Degree is open for this one-step notion, and is not settled by the known cubic result for eventual collapsibility, which permits a composition of several split polynomials rather than a single one.
A proof would close the one-step cubic case. A disproof — a single cubic irrationality admitting no split with — would separate one-step from eventual collapsibility by an explicit example, showing that composition is genuinely necessary.
Formalization Note "Cubic" is expressed as the minimal polynomial of over having degree ; integrality over is stated explicitly, though it already follows from that degree condition. No bound is placed on , and the value is not required to be nonzero — but cannot occur, since it would force the irreducible cubic minimal polynomial to divide a polynomial that splits over .