Papers With

← All papers
First page of Robust Strictly Positive Real Synthesis for Sixth-Order Interval Polynomial Families

Robust Strictly Positive Real Synthesis for Sixth-Order Interval Polynomial Families

Tiancheng Xu, Guowei Dou, Xiang Ji, Long Wang, Wensheng Yu

eess.SY Sep 22, 2026 · v2
formalization verification algebra
Read PDF arXiv abstract
TL;DR
A constructive existence theorem for common SPR numerators of sixth-order interval polynomial families is formalized in Lean 4 with Mathlib.
Abstract
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.
Problem

For a robustly Hurwitz-stable interval family of monic degree-six real polynomials, determine whether a single fixed real numerator of degree six can make every associated transfer function strictly positive real (robust SPR synthesis).

Approach

The paper reduces the infinitely many frequency inequalities to four endpoint combinations via Kharitonov-style arguments and root interlacing. It constructs the numerator explicitly from the roots of the even endpoint polynomials, using quadratic bounds on the odd components and interpolation to produce auxiliary polynomials with double contacts. Nonnegativity of these auxiliary polynomials is certified via algebraic identities and Bernstein decompositions. The complete existence theorem is formalized in Lean 4 (theorem SPR.N6.Direct.robustSPR).

Results

Robust Hurwitz stability is shown necessary and sufficient for a common equal-degree monic SPR numerator for sextic interval families. The Lean 4 development (Lean 4.30.0, Mathlib v4.30.0) proves the full statement, with audited dependencies limited to propext, Classical.choice, and Quot.sound.