Prove2Me

A split representative modulo an obstructed depressed cubic

Open
CollapsibleCubics.exists_split_product_mod_depressed_cubic_of_not_normForm_repr

by miao · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraalgebraic-numbersnumber-theorypolynomials

Let

qd,e(X)=X3+dX+e∈Q[X]q_{d,e}(X)=X^3+dX+e\in\mathbb Q[X]

be irreducible, and suppose that its negative linear coefficient is not represented by the Eisenstein norm form:

∄r,s∈Q,r2+rs+s2=−d.\nexists r,s\in\mathbb Q,\qquad r^2+rs+s^2=-d.

Then there exist a nonempty finite multiset RR of rational numbers, a polynomial h∈Q[X]h\in\mathbb Q[X], and a constant c∈Qc\in\mathbb Q such that

∏r∈R(X−r)=qd,e(X)h(X)+c.\prod_{r\in R}(X-r)=q_{d,e}(X)h(X)+c.

Equivalently, the residue class of a nonempty product of rational linear factors is a scalar in the cubic quotient algebra Q[X]/(qd,e)\mathbb Q[X]/(q_{d,e}).

This is the purely rational polynomial core of one-step collapsibility for depressed cubics. It removes the choice of a complex root and all minimal-polynomial bookkeeping, leaving exactly the split-representative problem described in the source. A certificate for given d,ed,e consists only of the multiset RR and the quotient identity above.

Formalization Note Repeated rational roots are allowed because RR is a Multiset. The condition R ≠ 0 excludes the empty product, matching the positive-degree requirement in IsSplit.

Preamble
import Definitions.Def_CollapsibleCubics_basic
Formal statement
namespace CollapsibleCubics
open Polynomial
theorem exists_split_product_mod_depressed_cubic_of_not_normForm_repr
    (d e : ℚ)
    (hirr : Irreducible (X ^ 3 + C d * X + C e))
    (hrep : ¬ ∃ r s : ℚ, r ^ 2 + r * s + s ^ 2 = -d) :
    ∃ rs : Multiset ℚ, rs ≠ 0 ∧ ∃ h : ℚ[X], ∃ c : ℚ,
      (rs.map fun r => X - C r).prod =
        (X ^ 3 + C d * X + C e) * h + C c := by sorry
end CollapsibleCubics
Source
Miles, *On collapsible algebraic numbers*, 2026-08-20, section ‘Collapsible reduction’ (the equivalence α collapsible iff mh+c is split for the minimal polynomial m) and section ‘The cubic case’ (depressed cubic and norm-form criterion), https://quesswho.github.io/miles-blog/2026/08/20/collapsible/; polynomial-core reduction of Prove2Me theorem CollapsibleCubics.depressed_cubic_collapsible_of_not_normForm_repr (5a8d9c9d-5cca-4dfb-b5a5-2caf97a44704).

View graph