发表机构
School of Electronic Engineering, Beijing University of Posts and Telecommunications; Center for Systems and Control, College of Engineering, Peking University; Center for Multi-Agent Research, Institute for Artificial Intelligence, Peking University（北京邮电大学电子工程学院; 北京大学工学院系统与控制中心; 北京大学人工智能研究院多智能体研究中心）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对六阶首一实多项式区间族，证明了存在单一六次实分子使所有传递函数严格正实，并给出构造性证明，且已在Lean4中形式化验证。
AI 中文摘要
每个六次首一实多项式的Hurwitz稳定区间族都允许一个六次实分子，使得所有相关的传递函数都严格正实。我们给出了一个构造性证明。该完整存在性定理已在Lean4中形式化。
英文摘要
Every Hurwitz-stable interval family of monic real polynomials of degree six admits a single real numerator of degree six that makes all the associated transfer functions strictly positive real. We give a constructive proof. The complete existence theorem has been formalized in Lean4.
