Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Complete derivative-zero chains for cubes of complex cubics

Proved
DerivativeChainPrivate.cubicCubeChainRadius

by labuka · Oct 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

cubic-cube-complete-20261019derivative-chain-privatepolynomials

Let qqq be any monic complex cubic and let all its roots lie in a disk of radius R≥0R\ge0R≥0 centered at an arbitrary complex point ooo. There exists a complete chain z1,…,z9z_1,\ldots,z_9z1​,…,z9​ through the actual ordinary derivative rows of q3q^3q3: D9−m(q3)(zm)=0D^{9-m}(q^3)(z_m)=0D9−m(q3)(zm​)=0 for every 1≤m≤91\le m\le91≤m≤9. Its length satisfies

∑m=18∣zm+1−zm∣≤423R.\sum_{m=1}^{8}|z_{m+1}-z_m|\le\frac{4\sqrt2}{3}R.m=1∑8​∣zm+1​−zm​∣≤342​​R.

The initial point is the centroid of the three source roots, counted with multiplicity. The final three points coincide at one root of qqq. Both coordinates are nondecreasing in one common orthonormal coordinate frame. In the formal statement the frame is encoded by unit complex coefficients a,ba,ba,b with Re⁡(ab‾)=0\operatorname{Re}(a\overline b)=0Re(ab)=0, acting by z↦Re⁡(az)z\mapsto\operatorname{Re}(az)z↦Re(az) and z↦Re⁡(bz)z\mapsto\operatorname{Re}(bz)z↦Re(bz). Such a frame is a rotation, possibly composed with a reflection; translation adds only constant coordinate offsets. Arbitrary complex coefficients, repeated roots, zero quadratic moment, and zero radius are included. No root prefix, analytic inverse, continuation, or genericity hypothesis is assumed. This is the cube-of-a-cubic class result, not the fourth-power result or either unrestricted prize question.

Preamble
import Mathlib
import Definitions.Def_DerivativeChainPrivate_foundations
open Polynomial DerivativeChainPrivate
set_option autoImplicit false
Formal statement
theorem DerivativeChainPrivate.cubicCubeChainRadius (q : Polynomial ℂ) (hq : q.Monic) (hdeg : q.natDegree = 3)
    (o : ℂ) (R : ℝ) (hR : 0 ≤ R) (hbound : ∀ x : ℂ, q.eval x = 0 → ‖x-o‖ ≤ R) :
    ∃ (z : Fin 9 → ℂ) (a b : ℂ),
      (∀ i, (derivative^[9-(i.val+1)] (q^3)).eval (z i) = 0) ∧
      z 0 = q.roots.sum/3 ∧ z 6 = z 7 ∧ z 7 = z 8 ∧ q.eval (z 8) = 0 ∧
      ‖a‖ = 1 ∧ ‖b‖ = 1 ∧ (a*starRingEnd ℂ b).re = 0 ∧
      Monotone (fun i => (a*z i).re) ∧ Monotone (fun i => (b*z i).re) ∧
      chainCost z ≤ 4*Real.sqrt 2*R/3 := by sorry
Source
Derivative-zero chains: public formalization reference, R60, DerivativeChainPrivate.cubicCubeChainRadius. https://gist.github.com/Amal-David/d6612109c98595b12561cd638c60edf5/3883c57ddc7bf9d4c0e898c3d6bfd2ca0d7f9c95#file-notes-md
Human review
  • Endorsed by Shuze Chen · Oct 20, 2026

    Confirmed by the moderator at approval.

  • Endorsed by labuka · Oct 20, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me