Product criterion for collapsibility

Proved

CollapsibleCubics.collapsible_iff_prod

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

algebraalgebraic-numbersnumber-theorypolynomials

Let $K$ be a field containing $\mathbb{Q}$ and let $\alpha \in K$ . Then $\alpha$ is collapsible if and only if some nonempty finite multiset of rational numbers $r_1, \dots, r_n$ satisfies

\prod_{i=1}^{n}\,(\alpha - r_i) \;\in\; \mathbb{Q}.

The forward direction discards the leading coefficient of a collapsing polynomial; the reverse direction assembles the monic product $\prod_i (x - r_i)$ , which is split because it is nonconstant with all roots rational.

The criterion removes the polynomial from the problem. Collapsibility becomes a purely multiplicative condition: $\alpha$ is collapsible exactly when some finite product of elements $\alpha - r$ , with $r$ ranging over $\mathbb{Q}$ with repetition allowed, is rational — that is, when the classes of the $\alpha - r$ generate a relation in the quotient group $K^{\times}/\mathbb{Q}^{\times}$ with non-negative exponents. Every later statement in this mission is phrased against this reformulation, and the non-negativity of the exponents is precisely what makes the problem hard.

Formalization Note The multiset is required to be nonempty; on the polynomial side this is what the condition $\deg f > 0$ encodes. Multiplicities are allowed on both sides.

Preamble

import Definitions.Def_CollapsibleCubics_basic

Formal statement

import Definitions.Def_CollapsibleCubics_basic

namespace CollapsibleCubics
theorem collapsible_iff_prod {K : Type*} [Field K] [Algebra ℚ K] (α : K) :
    Collapsible α ↔ ∃ rs : Multiset ℚ, rs ≠ 0 ∧
      ∃ c : ℚ, (rs.map fun r => α - algebraMap ℚ K r).prod = algebraMap ℚ K c := 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. Reformulation used throughout the accompanying Lean development (result L5).

Read-back

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

Fix a field $K$ of characteristic zero — more precisely, any field $K$ equipped with a $\mathbb{Q}$ -algebra structure, so that there is a structural ring homomorphism $\iota : \mathbb{Q} \to K$ (written $\iota(c)$ below for the image of a rational $c$ in $K$ ) — and fix an element $\alpha \in K$ . The statement asserts a logical equivalence (an "if and only if", in both directions) between the following two conditions.

Left-hand side. $\alpha$ is collapsible, which by the bundle's definition means: there exists a polynomial $f \in \mathbb{Q}[X]$ such that

$f$ $f$ is split, meaning both that
- $0 < \deg f$ (the degree of $f$ , as a natural number, is strictly positive — this rules out the zero polynomial and all constants), and
- there exist a rational number $a$ and a finite multiset $rs$ of rational numbers (a finite list of rationals with multiplicity, order irrelevant) with $a \neq 0$ and

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

the product being taken over the multiset $rs$ with multiplicity, and equal to the constant polynomial $1$ when $rs$ is empty;

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 \mapsto \alpha$ .

Note that in this definition the two occurrences of the existential data are nested but independent in the following sense: the same $f$ must simultaneously be split and take a rational value at $\alpha$ ; the multiset $rs$ and the leading coefficient $a$ are existentially quantified inside the splitting condition only, and the constant $c$ is quantified separately afterwards.

Right-hand side. There exists a finite multiset $rs$ of rational numbers such that

$rs \neq 0$ , i.e. $rs$ is not the empty multiset (it contains at least one element, counted with multiplicity); and
there exists a rational number $c$ with

\prod_{r \in rs} \bigl(\alpha - \iota(r)\bigr) \;=\; \iota(c),

the product being over the multiset $rs$ with multiplicity, computed in $K$ .

Points the quantifiers silently settle. No hypothesis is placed on $\alpha$ : it may be $0$ , may lie in the image of $\mathbb{Q}$ , or may be transcendental over $\mathbb{Q}$ . No hypothesis is placed on $K$ beyond being a field with a $\mathbb{Q}$ -algebra structure; in particular $K$ is not assumed to be a number field, finite-dimensional over $\mathbb{Q}$ , or algebraically closed. The rational number $c$ on either side is unconstrained — it may be $0$ , so the condition " $f(\alpha)$ is rational" includes the case $f(\alpha) = 0$ , i.e. $\alpha$ being a root of a split rational polynomial. On the right-hand side the multiset $rs$ is required to be nonempty, whereas on the left-hand side the nonemptiness of the corresponding multiset is not stated directly but is imposed indirectly through the requirement $0 < \deg f$ together with $f = a \prod_{r \in rs}(X - r)$ and $a \neq 0$ . Elements of $rs$ may repeat, and no distinctness, ordering, or bound on the number of roots is imposed on either side; in particular the degree of $f$ (equivalently, the size of the multiset) is arbitrary and unbounded. The scalar $a$ appearing on the left-hand side has no counterpart on the right-hand side, where the product is monic by construction.

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