arXiv eess.SY 系统与控制· Jeffrey Humpherys·· 5 小时前精选AI 评分42
De Cock-De Moor 猜想获证：Lean 4 形式化验证与不定度量下的角度范式
The De Cock--De Moor Conjecture: Proof, Normal Form, and Indefinite Angles
AI 导读
论文证明了 De Cock 和 De Moor 关于三个耦合 Lyapunov 方程解构造的两个矩阵共享特征值的猜想（即《数学系统与控制理论未解决问题》中的 Problem 9.1），在自然的非共振条件下成立，无需稳定性或可对角化假设，并证明两矩阵相似。
推荐理由
论文把悬而未决的 De Cock-De Moor 猜想在非共振条件下给出证明并用 Lean 4 验证，读者可了解其 Cauchy 矩阵结构与有理插值的化归思路。
来源：arXiv eess.SY 系统与控制 · arxiv.org