Complete derivative-zero chains for cubes of complex cubics
ProvedDerivativeChainPrivate.cubicCubeChainRadiusLet be any monic complex cubic and let all its roots lie in a disk of radius centered at an arbitrary complex point . There exists a complete chain through the actual ordinary derivative rows of : for every . Its length satisfies
The initial point is the centroid of the three source roots, counted with multiplicity. The final three points coincide at one root of . Both coordinates are nondecreasing in one common orthonormal coordinate frame. In the formal statement the frame is encoded by unit complex coefficients with , acting by and . 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.
import Mathlib import Definitions.Def_DerivativeChainPrivate_foundations open Polynomial DerivativeChainPrivate set_option autoImplicit false
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 sorryConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.