Archimedean lower bound on the degree of a collapsing

Proved

CollapsibleCubics.pi_div_psi_le_natDegree

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

algebraalgebraic-numbersnumber-theorypolynomials

Let $m(x) = x^3 + dx + e$ be irreducible over $\mathbb{Q}$ with negative discriminant, so that it has one real root and a conjugate pair of non-real roots. Write these as

\alpha_1 = -2u, \qquad \alpha_{2,3} = u \pm iv, \qquad d = v^2 - 3u^2, \quad e = 2u(u^2+v^2),

normalising the sign of $v$ so that $uv > 0$ , and set $\psi = \arctan(3u/v) \in (0, \pi/2)$ . If $f \in \mathbb{Q}[x]$ is split and $f(\alpha) \in \mathbb{Q}$ for a root $\alpha$ of $m$ , then

\frac{\pi}{\psi} \;\le\; \deg f.

Because $m$ is irreducible, $f(\alpha) = c$ forces $m \mid f - c$ , so $f$ takes the same value at all three roots; the ratios $z_i = (\alpha_1 - r_i)/(\alpha_2 - r_i)$ of the linear factors therefore multiply to $1$ . Each $z_i$ lies on a fixed circle through $0$ and $1$ determined by $\psi$ , and strict concavity of $\log\cos$ turns that constraint into the stated bound.

As $\tau = e^2/d^3 \to 0^+$ one has $\psi \to 0$ , so the required degree is unbounded: no uniform degree suffices, and this is the central obstruction to a general construction. For $x^3 + 6x + 1$ the bound already forces $\deg f \ge 32$ .

Formalization Note The parameters $u, v$ enter as real numbers satisfying the factorisation identity for all real $x$ , which is equivalent to the two displayed Vieta relations. The condition $uv > 0$ is a normalisation, not a restriction: $v$ is determined only up to sign. The conclusion compares a real number with the natural-number degree of $f$ , coerced into $\mathbb{R}$ .

Preamble

import Definitions.Def_CollapsibleCubics_basic

Formal statement

import Definitions.Def_CollapsibleCubics_basic

namespace CollapsibleCubics
open Polynomial
theorem pi_div_psi_le_natDegree (d e : ℚ)
    (hirr : Irreducible (X ^ 3 + C d * X + C e : ℚ[X]))
    (u v : ℝ) (hsign : 0 < u * v)
    (huv : ∀ x : ℝ, x ^ 3 + (d : ℝ) * x + (e : ℝ) = (x + 2 * u) * ((x - u) ^ 2 + v ^ 2))
    (α : ℂ) (hα : α ^ 3 + (d : ℂ) * α + (e : ℂ) = 0)
    (f : ℚ[X]) (hf : IsSplit f) (c : ℚ) (hc : aeval α f = (c : ℂ)) :
    Real.pi / Real.arctan (3 * u / v) ≤ f.natDegree := 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. The archimedean obstruction. Both halves are separately machine-checked in the accompanying development (the convexity bound and the Moebius reduction, results L9-L12 and L24); the statement in terms of a collapsing polynomial, as given here, is not yet proved there.

Read-back

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

The statement is universally quantified over: two rational numbers $d$ and $e$ ; two real numbers $u$ and $v$ ; a complex number $\alpha$ ; a polynomial $f$ with rational coefficients; and a rational number $c$ . It asserts that whenever all of the following hold simultaneously, the displayed inequality holds.

Hypotheses.

(Irreducibility.) The polynomial $X^3 + dX + e$ , viewed in the polynomial ring $\mathbb{Q}[X]$ , is irreducible: it is not a unit, and in every factorization of it into two rational polynomials one factor is a nonzero rational constant. (Since its degree is $3$ , this in particular rules out any rational root.)
(Sign condition.) $u\,v > 0$ — i.e. $u$ and $v$ are both nonzero and have the same sign (both positive, or both negative).
(Real factorization.) For every real number $x$ ,

x^3 + d\,x + e \;=\; (x + 2u)\bigl((x-u)^2 + v^2\bigr),

where $d$ and $e$ are read as real numbers via the inclusion $\mathbb{Q} \subseteq \mathbb{R}$ . Comparing coefficients, this identity is equivalent to the two equations

d = v^2 - 3u^2, \qquad e = 2u\,(u^2+v^2).

(Root.) $\alpha$ is a complex number with $\alpha^3 + d\,\alpha + e = 0$ , with $d,e$ read as complex numbers. Nothing else is assumed about $\alpha$ : it is not required to be non-real, and it is not tied to $u$ or $v$ except through this equation. Combined with hypothesis 3, $\alpha$ is one of the three numbers $-2u$ , $u + i v$ , $u - i v$ ; combined with hypothesis 1, $\alpha$ is irrational, so $X^3 + dX + e$ is its minimal polynomial over $\mathbb{Q}$ .
(Splitness of $f$ , unfolded.) $f \in \mathbb{Q}[X]$ satisfies the bundle-specific predicate " $f$ is split", which unfolds to: the degree of $f$ is strictly positive, and there exist a rational number $a \neq 0$ and a finite multiset $R = \{r_1,\dots,r_n\}$ of rational numbers (repetitions allowed) such that

f \;=\; a \prod_{j=1}^{n} (X - r_j).

So $f$ is a nonzero rational polynomial that factors completely into linear factors over $\mathbb{Q}$ ; its roots are all rational but need not be distinct, and $n = \deg f \ge 1$ (the multiset cannot be empty, since an empty product would give $f = a$ of degree $0$ ).

(Rational value at $\alpha$ .) Evaluating $f$ at $\alpha$ under the ring map $\mathbb{Q}[X] \to \mathbb{C}$ sending $X \mapsto \alpha$ gives the rational number $c$ , viewed in $\mathbb{C}$ :

f(\alpha) \;=\; a\prod_{j=1}^{n}(\alpha - r_j) \;=\; c .

No sign or nonvanishing condition is imposed on $c$ . Because the cubic is the minimal polynomial of $\alpha$ , this is equivalent to $f(X) - c$ being divisible in $\mathbb{Q}[X]$ by $X^3 + dX + e$ .

Conclusion. Under all of the above,

\frac{\pi}{\arctan\!\left(\dfrac{3u}{v}\right)} \;\le\; \deg f,

a non-strict inequality between real numbers, where $\deg f$ is the (natural-number) degree of $f$ — equivalently the number of linear factors $n$ counted with multiplicity — coerced into $\mathbb{R}$ , and $\arctan$ is the principal inverse tangent with values in $(-\pi/2,\pi/2)$ .

Degenerate and edge cases. The hypotheses are not vacuous: they are jointly satisfiable. For instance $d = -1$ , $e = 1$ gives $X^3 - X + 1$ , which is irreducible over $\mathbb{Q}$ ; its unique real root is $t \approx -1.32472$ , and taking $u = -t/2 \approx 0.66236$ , $v = \sqrt{d + 3u^2} \approx 0.56228$ satisfies $uv > 0$ and the factorization identity; taking $\alpha$ any root of the cubic, $f = X(X-1)(X+1) = X^3 - X$ (split over $\mathbb{Q}$ , degree $3$ ) gives $f(\alpha) = \alpha^3 - \alpha = -1 = c$ . Here the left-hand side is $\pi/\arctan(3u/v) \approx 2.4259 \le 3$ .

The hypotheses force definite signs and root structure. Since $uv > 0$ , neither $u$ nor $v$ is zero, so $3u/v > 0$ and $\arctan(3u/v) \in (0, \pi/2)$ ; hence no division-by-zero junk value arises anywhere in the conclusion, and the left-hand side is a genuine real number strictly greater than $\pi/(\pi/2) = 2$ . Consequently the conclusion is strictly stronger than " $\deg f \ge 2$ ": since $\deg f$ is a natural number exceeding a quantity $> 2$ , the inequality entails $\deg f \ge 3$ . Note also that $v \ne 0$ means the quadratic factor $(x-u)^2 + v^2$ has no real root, so the cubic has exactly one real root, namely $-2u$ , and two genuinely non-real complex-conjugate roots $u \pm i v$ ; its discriminant $-4d^3 - 27e^2$ is negative. Since $-2u$ is a root of an irreducible rational cubic, $u$ is an irrational (cubic) real number, and $u \ne 0$ forces $e = 2u(u^2+v^2) \ne 0$ ; also $d = v^2 - 3u^2$ may be of either sign. The hypotheses do not require $u > 0$ : the case $u < 0, v < 0$ is equally allowed, and then $-2u > 0$ while $3u/v$ is still positive. Finally, $f$ is permitted to have repeated rational roots, and its leading coefficient $a$ may be any nonzero rational; the statement says nothing about existence of such an $f$ — it only bounds the degree of any $f$ that meets the conditions.

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