Collapsibility is an affine invariant

Proved

CollapsibleCubics.collapsible_affine

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

algebraalgebraic-numbersnumber-theorypolynomials

Let $K$ be a field containing $\mathbb{Q}$ , let $\alpha \in K$ be collapsible, and let $l, b \in \mathbb{Q}$ with $l \neq 0$ . Then

l\alpha + b \quad \text{is collapsible.}

If $f = a\prod_i (x - r_i)$ is split with $f(\alpha) \in \mathbb{Q}$ , the transformed polynomial $g = a\prod_i \bigl(x - (l r_i + b)\bigr)$ is again split and sends $l\alpha + b$ into $\mathbb{Q}$ .

Applying the statement in both directions (to $l$ and to $l^{-1}$ ) shows that collapsibility depends only on the $\mathbb{Q}$ -affine orbit of $\alpha$ . Two consequences organise the whole problem. First, an arbitrary cubic may be replaced by a depressed one $x^3 + dx + e$ , since completing the cube is an affine change of variable. Second, the scaling $\alpha \mapsto w\alpha$ sends $(d,e)$ to $(w^2 d, w^3 e)$ , so the question depends only on the invariant $\tau = e^2/d^3$ — reducing the search space from two rational parameters to one.

Formalization Note The conclusion asserts only that some split polynomial exists for $l\alpha + b$ ; no relation between the degrees or roots of the two witnesses is claimed, although the natural witness preserves both.

Preamble

import Definitions.Def_CollapsibleCubics_basic

Formal statement

import Definitions.Def_CollapsibleCubics_basic

namespace CollapsibleCubics
theorem collapsible_affine {K : Type*} [Field K] [Algebra ℚ K] {α : K} (h : Collapsible α)
    (l b : ℚ) (hl : l ≠ 0) :
    Collapsible (algebraMap ℚ K l * α + algebraMap ℚ K b) := by sorry
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. Affine invariance as used to reduce to depressed cubics (result L6).

Read-back

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

Fix a field $K$ that is equipped with the structure of a $\mathbb{Q}$ -algebra, so that there is a ring homomorphism $\iota : \mathbb{Q} \to K$ (the structure map); $K$ is universally quantified (implicitly) over all types in an arbitrary universe carrying such a field and $\mathbb{Q}$ -algebra structure. Fix also an element $\alpha \in K$ , again an implicit universally quantified variable.

Call a rational polynomial $f \in \mathbb{Q}[X]$ split when both of the following hold:

$\deg f > 0$ , where the degree here is the natural-number degree (so the zero polynomial and the nonzero constants, both of degree $0$ , are excluded); and
there exist a rational number $a$ and a multiset $R$ of rational numbers with $a \neq 0$ and

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

the product being taken over $R$ with multiplicity. Note $R$ is allowed to be the empty multiset, in which case the product is $1$ and $f = a$ is a nonzero constant — but such an $f$ is ruled out by the degree condition, so in effect $R$ must be nonempty. Nothing forces $\deg f$ to equal the size of $R$ beyond what this equation itself imposes, and repeated roots are permitted.

Call an element $\beta \in K$ collapsible when there exists a polynomial $f \in \mathbb{Q}[X]$ that is split in the above sense, together with a rational number $c$ , such that evaluating $f$ at $\beta$ (via the $\mathbb{Q}$ -algebra evaluation map, i.e. substituting $\beta$ for $X$ and mapping the rational coefficients into $K$ through $\iota$ ) yields the image of $c$ :

f(\beta) \;=\; \iota(c).

The rational number $c$ is existentially quantified, with no constraint on it; in particular $c = 0$ is allowed, and the polynomial $f$ may depend on $\beta$ .

The statement asserts: for every such $K$ , every $\alpha \in K$ , and every pair of rational numbers $l$ and $b$ , if $\alpha$ is collapsible and $l \neq 0$ , then the element

\iota(l) \cdot \alpha + \iota(b) \;\in\; K

is collapsible. Here $l$ and $b$ are explicit arguments ranging over all of $\mathbb{Q}$ , the hypothesis $l \neq 0$ constrains only $l$ , and $b$ is entirely unconstrained (including $b = 0$ ). The hypothesis that $\alpha$ is collapsible is assumed, not derived, and the conclusion is a bare existence claim about some split rational polynomial and some rational constant for the transformed element — no relationship is asserted between the witnessing polynomial for $\alpha$ and the witnessing polynomial for $\iota(l)\alpha + \iota(b)$ , and no claim is made about degrees, root sets, or the value $c$ being preserved. The conclusion is about the specific affine combination $\iota(l)\alpha + \iota(b)$ formed inside $K$ using multiplication and addition of $K$ , where the scalars enter as the images $\iota(l)$ and $\iota(b)$ of the rationals under the structure map.

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