Split polynomials and collapsible numbers

Definition

CollapsibleCubics_basic

by quesswho · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraalgebraic-numbersnumber-theorypolynomials

A polynomial $f \in \mathbb{Q}[x]$ is split if $\deg f \ge 1$ and $f$ factors completely into linear factors over $\mathbb{Q}$ :

f(x) \;=\; a\prod_{i=1}^{n}(x - r_i), \qquad a \in \mathbb{Q}^{\times}, \quad r_1,\dots,r_n \in \mathbb{Q}.

Equivalently, $f$ is a rational polynomial of strictly positive degree all of whose roots are rational. Split polynomials are the simplest non-constant maps defined over $\mathbb{Q}$ that can be applied to an algebraic number.

Let $K$ be a field containing $\mathbb{Q}$ , with structure map $\iota : \mathbb{Q} \to K$ . An element $\alpha \in K$ is collapsible if some split polynomial sends it into $\mathbb{Q}$ :

\exists\, f \text{ split}, \ \exists\, c \in \mathbb{Q}: \qquad f(\alpha) = \iota(c).

This is the one-step notion, also written $1$ -collapsible. It is strictly stronger than eventual collapsibility, which asks only that some finite composition $f_k \circ \cdots \circ f_1$ of split polynomials send $\alpha$ into $\mathbb{Q}$ .

These two definitions are the vocabulary in which every statement of this mission is phrased, and they are reusable for the degree- $4$ and higher cases of the same problem.

Formalization Note The factorisation is recorded as a multiset of rational roots, so repeated roots are permitted and the leading coefficient is carried separately. Collapsibility is stated for $\alpha$ in an arbitrary field $K$ carrying a $\mathbb{Q}$ -algebra structure, rather than only for $K = \mathbb{C}$ , so every consequence applies verbatim to a root taken in $\mathbb{R}$ , in $\mathbb{C}$ , or in the quotient $\mathbb{Q}[x]/(m)$ . The value $c$ is not required to be nonzero.

Definition code

import Mathlib

namespace CollapsibleCubics

open Polynomial

/-- A polynomial over `ℚ` is *split* if it has degree at least `1` and factors into rational
linear factors: `f = C a * ∏ (X - rᵢ)` with `a ≠ 0` and all `rᵢ ∈ ℚ`. -/
def IsSplit (f : ℚ[X]) : Prop :=
  0 < f.natDegree ∧ ∃ (a : ℚ) (rs : Multiset ℚ), a ≠ 0 ∧
    f = C a * (rs.map fun r => X - C r).prod

set_option linter.dupNamespace false in
/-- An element `α` of a field `K` containing `ℚ` is *collapsible* if some split rational
polynomial `f` sends it into `ℚ`, i.e. `f α ∈ ℚ`. -/
def Collapsible {K : Type*} [Field K] [Algebra ℚ K] (α : K) : Prop :=
  ∃ f : ℚ[X], IsSplit f ∧ ∃ c : ℚ, aeval α f = algebraMap ℚ K c

end CollapsibleCubics

Source

Miles, *Collapsible algebraic numbers*, blog post, 2026-08-20, https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ (definitions of *split* polynomial and of *1-collapsible*; statement that the degree-3 case of one-step collapsibility is open). Underlying problem: Griffin Macris, list of open problems, Problem 3, https://sites.google.com/view/griffinmacris/open-problems. Definitions as stated verbatim in the blog post.

Read-back

What the Lean code literally says, in plain math · claude-opus-5

IsSplit — This defines a predicate on a single-variable polynomial $f$ with rational coefficients (an element of $\mathbb{Q}[X]$ ). The predicate $\mathrm{IsSplit}(f)$ holds precisely when both of the following are true:

The natural-number degree of $f$ is strictly positive, i.e. $\deg f > 0$ where the degree is taken in $\mathbb{N}$ (so that the zero polynomial and all nonzero constants, both of which have natural degree $0$ , are excluded);
There exist a rational number $a$ and a multiset $R$ of rational numbers (a finite unordered collection of rationals with multiplicity, possibly empty) such that $a \neq 0$ and

f \;=\; a \cdot \prod_{r \in R} (X - r),

where the product is taken over the multiset $R$ with each element repeated according to its multiplicity, and the empty multiset yields the empty product $1$ . Here $a$ and $r$ are coerced into $\mathbb{Q}[X]$ as constant polynomials.

Note that the equation is an equality of polynomials, and no relationship between the size of $R$ and $\deg f$ is asserted separately — it is only whatever follows from the equation itself. The existentially quantified data $a$ and $R$ are not required to be unique. The degree condition is stated as a separate conjunct rather than being derived from the factorization.

Collapsible — This defines a predicate on an element $\alpha$ , where the ambient setting consists of: a type $K$ at an arbitrary universe level (an implicit argument), an instance making $K$ a field, and an instance making $K$ a $\mathbb{Q}$ -algebra (both typeclass arguments), together with a canonical structure map $\iota : \mathbb{Q} \to K$ supplied by that algebra structure. The predicate $\mathrm{Collapsible}(\alpha)$ holds precisely when there exists a polynomial $f \in \mathbb{Q}[X]$ such that:

$f$ satisfies $\mathrm{IsSplit}$ as unfolded above — that is, $\deg f > 0$ in $\mathbb{N}$ , and $f = a \prod_{r \in R}(X - r)$ for some nonzero rational $a$ and some finite multiset $R$ of rational numbers; and
there exists a rational number $c$ with

f(\alpha) \;=\; \iota(c),

where $f(\alpha)$ denotes the evaluation of $f$ at $\alpha$ under the $\mathbb{Q}$ -algebra map — i.e. the image of $f$ under the unique $\mathbb{Q}$ -algebra homomorphism $\mathbb{Q}[X] \to K$ sending $X$ to $\alpha$ — and $\iota(c)$ is the image of $c$ under the structure map $\mathbb{Q} \to K$ .

The rational number $c$ is existentially quantified and unconstrained: in particular $c = 0$ is permitted, so the condition includes the case $f(\alpha) = 0$ . Both $f$ and $c$ are merely asserted to exist, with no uniqueness or minimality requirement, and no constraint tying $\deg f$ to any invariant of $\alpha$ such as its degree over $\mathbb{Q}$ (indeed $\alpha$ is not assumed algebraic over $\mathbb{Q}$ ). No hypothesis relates the roots in $R$ to $\alpha$ . The definition applies to every element $\alpha$ of every such $K$ , including $\alpha$ lying in the image of $\mathbb{Q}$ and including $K = \mathbb{Q}$ itself.

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by quesswho · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph