Gap parity for split polynomials

Proved

CollapsibleCubics.even_card_roots_between

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

algebraalgebraic-numbersnumber-theorypolynomials

Let $f = a\prod_{r \in R}(x - r)$ be a split rational polynomial, with $a \neq 0$ and $R$ a finite multiset of rational roots. Let $x < y$ be real numbers, neither of them a root of $f$ , at which $f$ takes the same nonzero value:

f(x) = f(y) \neq 0.

Then the number of roots of $f$ lying strictly between $x$ and $y$ , counted with multiplicity, is even.

The mechanism is the sign of $f$ : since $f$ splits over $\mathbb{R}$ , it changes sign exactly at its roots, counted with multiplicity, so equal values at the two endpoints force an even number of sign changes in between.

The application is to the totally real case. If $\Delta = -4d^3 - 27e^2 > 0$ , the cubic has three real conjugates $\alpha_1 < \alpha_2 < \alpha_3$ , and a collapsing $f$ takes the same nonzero rational value at all three. The theorem then says that each of the two gaps $(\alpha_1, \alpha_2)$ and $(\alpha_2, \alpha_3)$ contains an even number of roots of $f$ . This is the only archimedean constraint known when $\Delta > 0$ — the degree bound available for $\Delta < 0$ has no analogue there — and it halves the effective search space.

Formalization Note Roots are counted with multiplicity, as elements of the multiset $R$ . The hypotheses are satisfiable but not always: for an $f$ that is injective on the relevant range, no such pair $x < y$ exists and the statement is vacuous for that $f$ .

Preamble

import Definitions.Def_CollapsibleCubics_basic

Formal statement

import Definitions.Def_CollapsibleCubics_basic

namespace CollapsibleCubics
open Polynomial
theorem even_card_roots_between {f : ℚ[X]} {a : ℚ} {rs : Multiset ℚ} (ha : a ≠ 0)
    (hf : f = C a * (rs.map fun r => X - C r).prod)
    {x y : ℝ} (hxy : x < y) (hr : ∀ r ∈ rs, (r : ℝ) ≠ x ∧ (r : ℝ) ≠ y)
    (hval : (aeval x f : ℝ) = aeval y f) (hne : (aeval x f : ℝ) ≠ 0) :
    Even (rs.filter fun r : ℚ => x < (r : ℝ) ∧ (r : ℝ) < y).card := 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. Archimedean constraint in the totally real case (result L16).

Read-back

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

Fix a nonzero rational number $a$ (that is, $a \neq 0$ ) and a finite multiset $rs$ of rational numbers, and let $f$ be the polynomial with rational coefficients given by

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

where the product runs over the elements of $rs$ with multiplicity (so a rational appearing $k$ times in $rs$ contributes the factor $(X-r)^k$ ); in particular, if $rs$ is empty the product is $1$ and $f$ is the constant polynomial $a$ . Note that $f$ is assumed to be equal to this product — it is not merely assumed to have this shape up to some further factor, and every root of $f$ is therefore accounted for by $rs$ .

Now let $x$ and $y$ be real numbers with $x < y$ , and evaluate $f$ at real arguments via the inclusion $\mathbb{Q} \hookrightarrow \mathbb{R}$ , writing $f(x), f(y) \in \mathbb{R}$ . Assume:

(no root at the endpoints) for every $r$ belonging to $rs$ , the real number $r$ satisfies $r \neq x$ and $r \neq y$ ;
(equal values) $f(x) = f(y)$ as real numbers;
(nonvanishing) $f(x) \neq 0$ (hence also $f(y) \neq 0$ , by the previous assumption).

The conclusion is that the number

\#\{\, r \in rs : x < r < y \,\}

is even, where the count is again taken with multiplicity: it is the cardinality of the sub-multiset of $rs$ obtained by keeping exactly those entries $r$ whose image in $\mathbb{R}$ lies strictly between $x$ and $y$ (both inequalities strict, so entries equal to $x$ or to $y$ would be excluded — though the endpoint hypothesis already rules those out). "Even" here means the cardinality is divisible by $2$ , which includes the value $0$ ; so the statement is satisfied in particular when no element of $rs$ lies strictly inside the interval, e.g. when $rs$ is empty.

Every quantity is a bound variable of the statement: $f$ , $a$ , $rs$ , $x$ , $y$ are all universally quantified, with $f$ , $a$ , $rs$ , $x$ , $y$ implicit and the five hypotheses above explicit. Note that the hypotheses can be simultaneously satisfiable and can also be jointly impossible for particular choices — for instance, for a fixed $f$ that is strictly monotone on the relevant range no pair $x < y$ with $f(x) = f(y)$ exists, and the statement is then vacuous for that $f$ .

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