HEXAGONbeta

Formalization of Robust Strictly Positive Real Synthesis for Fourth-Order Interval Polynomial Families

Primarily AI-generated textHuman understanding: all partscs.LO — Logic in Computer Sciencemath.OC — Optimization and Control

Contributed by Tiancheng Xu ↗, Wensheng Yu

Version 1 / Nov 06, 2026 / CC BY 4.0

Abstract

That every robustly Hurwitz-stable fourth-order interval polynomial family admits a common strictly positive real (SPR) numerator was conjectured by Anderson et al. and proved by Yu and Wang. In this paper, we present a complete formalization of this classical synthesis theorem in the Lean~4 interactive theorem prover.

Tools used

OpenAI
ChatGPT
Lean
Lean

References

  1. Anderson, Brian D. O.; Dasgupta, Soura; Khargonekar, Pramod P.; Kraus, Frantisek J.; Mansour, Mohamed. Robust strict positive realness: characterization and construction. IEEE Transactions on Circuits and Systems, vol. 37, no. 7, pp. 869–876. 1990
  2. Betser, A.; Zeheb, E. Design of robust strictly positive real transfer functions. IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications, vol. 40, no. 9, pp. 573–580. 1993
  3. Dahmen, Sander R.; Hölzl, Johannes; Lewis, Robert Y. Formalizing the solution to the cap set problem. 10th International Conference on Interactive Theorem Proving (ITP 2019), vol. 141, pp. 15:1–15:19. 2019
  4. Dasgupta, Soura; Bhagwat, AS. Conditions for designing strictly positive real transfer functions for adaptive output error identification. IEEE Transactions on Circuits and Systems, vol. 34, no. 7, pp. 731–736. 1987
  5. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 theorem prover and programming language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021
  6. Kharitonov, Vladimir L. The asymptotic stability of the equilibrium state of a family of systems of linear differential equations. Differentsial'nye Uravneniya, vol. 14, no. 11, pp. 2086–2088. 1978
  7. Li, Wenda; Paulson, Lawrence C. Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan–Fourier theorem. Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), pp. 52–64. 2019
  8. Mahboubi, Assia; Sibut-Pinote, Thomas. A formal proof of the irrationality of ζ(3)\zeta(3). Logical Methods in Computer Science, vol. 17, no. 1, pp. 16:1–16:28. 2021
  9. The mathlib Community. The Lean mathematical library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp. 367–381. 2020
  10. Wang, Long; Yu, Wensheng. Robust SPR synthesis for low-order polynomial segments and interval polynomials. Proceedings of the 2001 American Control Conference, vol. 5, pp. 3612–3617. 2001
Show all 13 referencesShow fewer references
  1. Yu, Wensheng; Wang, Long. Anderson's claim on fourth-order SPR synthesis is true. IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications, vol. 48, no. 4, pp. 506–509. 2001
  2. Yu, Wensheng; Wang, Long. Design of robust strictly positive real transfer functions. Networked Control Systems: Theory and Applications, pp. 293–341. 2008
  3. Yu, Wensheng; Wang, Long; Ackermann, Jürgen. Robust strictly positive real synthesis for polynomial families of arbitrary order. Science in China Series F: Information Sciences, vol. 47, no. 4, pp. 475–489. 2004

Version history

  1. v1 · 13 pagesSubmitted by Tiancheng XuInitial depositCurrentNov 06, 2026