The De Cock–De Moor Conjecture: Proof, Normal Form, and Indefinite Angles
Jeffrey Humpherys
math.OC
Aug 30, 2026 · v2
eess.SY
TL;DR
The main theorem (the De Cock–De Moor spectral identity) is formally verified in Lean 4 with Mathlib, provided as supplementary source.
Abstract
De Cock and De Moor conjectured that two matrices built from the solutions of three coupled Lyapunov equations always share their eigenvalues, an identity linking principal angles between model subspaces with the canonical correlations between the past and future of a stochastic process. The conjecture was recorded as Problem 9.1 of Unsolved Problems in Mathematical Systems and Control Theory. We prove it under the natural nonresonance condition, without stability or diagonalizability, and show that the two matrices are similar. The proof exposes a Cauchy-matrix structure created by the rank-one perturbation and reduces the problem to rational interpolation, and the main theorem has also been verified in the Lean 4 proof assistant. The same structure gives a normal form that depends only on the poles and zeros of the model. Off the stable set the eigenvalues become squared cosines of angles in an indefinite metric. We prove an inertia theorem for them and show that reflecting a pole or a zero across the unit circle acts on the angles by a principal pivot transform. For several inputs and outputs, where the conjecture fails, we identify the subspaces whose angles do give the canonical correlations. We also relate our approach to the independent proof of Gillberg and Löfberg.
Problem
De Cock and De Moor conjectured that two matrices built from solutions of three coupled Stein/Lyapunov equations share their eigenvalues, linking principal angles between model subspaces with past–future canonical correlations. The conjecture was recorded as Problem 9.1 of Unsolved Problems in Mathematical Systems and Control Theory.
Approach
Under a nonresonance hypothesis, the Stein solutions are diagonalized on the simple-spectrum set, which exposes Cauchy-matrix structure and reduces the problem to rational interpolation via a residue computation. A density and continuity argument then removes the simple-spectrum assumption and yields two basis-free identities that imply similarity. The main theorem is also formalized in Lean 4 with Mathlib, which proves the basis-free identities directly rather than through the density argument.
Results
The conjecture is proved without stability or diagonalizability, and the two matrices are shown to be similar. The paper also gives a normal form depending only on the poles and zeros, an inertia theorem for indefinite-metric angles, and a principal pivot transform description of reflecting poles or zeros across the unit circle. For the multi-channel case, where the conjecture fails, it identifies the subspaces whose angles do give the canonical correlations.
