% !TeX program = pdflatex \documentclass[a4paper,11pt]{article} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage[margin=25mm]{geometry} \usepackage{amsmath,amssymb,amsthm,mathtools,booktabs,array} \usepackage{enumitem,xcolor,xurl,authblk,tikz} \usetikzlibrary{arrows.meta,positioning} \usepackage[colorlinks=true,linkcolor=blue!40!black,citecolor=blue!40!black,urlcolor=blue!40!black]{hyperref} \setlength{\emergencystretch}{2em} \setlist{itemsep=2pt,topsep=3pt} \clubpenalty=10000 \widowpenalty=10000 \displaywidowpenalty=10000 \renewcommand{\topfraction}{0.9} \renewcommand{\bottomfraction}{0.8} \renewcommand{\textfraction}{0.07} \renewcommand{\floatpagefraction}{0.85} \numberwithin{equation}{section} \makeatletter \renewcommand\section{\@startsection {section}{1}{\z@}% {-2.4ex \@plus -0.6ex \@minus -0.2ex}% {1.2ex \@plus 0.2ex}% {\normalfont\large\bfseries}} \renewcommand\subsection{\@startsection{subsection}{2}{\z@}% {-1.8ex\@plus -0.4ex \@minus -0.2ex}% {0.9ex \@plus 0.2ex}% {\normalfont\normalsize\bfseries}} \makeatother \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\R}{\mathbb{R}} \newcommand{\C}{\mathbb{C}} \newcommand{\Q}{\mathbb{Q}} \newcommand{\Ree}{\operatorname{Re}} \newcommand{\Imm}{\operatorname{Im}} \newcommand{\degp}{\operatorname{deg}} \newenvironment{leancode}{% \begin{list}{}{\leftmargin=1.4em\rightmargin=0em\topsep=4pt\itemsep=0pt\parsep=0pt}% \item\relax\footnotesize\ttfamily\raggedright\obeylines }{\end{list}} \title{Formalization of Robust Strictly Positive Real Synthesis\\ for Fourth-Order Interval Polynomial Families} \renewcommand{\Affilfont}{\normalfont\fontsize{9}{11}\selectfont} \makeatletter \renewcommand{\maketitle}{% \begin{center} {\Large\bfseries\@title\par}\vspace{0.6em} {\def\rlap##1{##1}\AB@authlist\par} \end{center} \noindent\begin{minipage}{\textwidth} \centering\Affilfont\AB@affillist\par \end{minipage}\par\vspace{0.6em}} \makeatother \author[1]{Tiancheng Xu} \author[1]{Wensheng Yu} \affil[1]{School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, China} \date{} \hypersetup{ pdftitle={Formalization of Robust Strictly Positive Real Synthesis for Fourth-Order Interval Polynomial Families}, pdfauthor={Tiancheng Xu and Wensheng Yu} } \begin{document} \maketitle \begin{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.\ (1990) and proved by Yu and Wang (2001). In this paper, we present a complete formalization of this classical synthesis theorem in the Lean~4 interactive theorem prover. \end{abstract} \noindent\textbf{Keywords:} strictly positive real synthesis; interval polynomial family; Hurwitz stability; proof reconstruction; formal verification; Lean 4 \section{Introduction}\label{sec:intro} \subsection{Background and the Classical Fourth-Order Synthesis Theorem} Strictly positive real (SPR) transfer functions play a fundamental role in passivity analysis, absolute stability, adaptive control, and output-error system identification~\cite{DasguptaBhagwat1987,YuWang2008}. When the denominator coefficients vary independently within closed uncertainty intervals, the robust SPR synthesis problem asks for a single fixed real numerator polynomial that renders the transfer function strictly positive real for every admissible denominator in the family and at all real frequencies. Although Kharitonov's theorem~\cite{Kharitonov1978} reduces robust Hurwitz stability of an interval polynomial family to four vertex polynomials, and robust SPR analysis for a prescribed numerator can similarly be reduced to finite vertex combinations~\cite{AndersonEtAl1990,WangYu2001}, the synthesis problem is existential: the numerator coefficients must be fixed once and for all before the plant varies over the interval box and the frequency varies over the real line. For fourth-order robustly Hurwitz-stable interval polynomial families, Anderson et al.~\cite{AndersonEtAl1990} conjectured in 1990 that a common SPR numerator always exists, proposing an argument based on linear programming. After Betser and Zeheb~\cite{BetserZeheb1993} demonstrated via counterexample that the proposed linear-programming condition was not necessary, Yu and Wang~\cite{YuWangFourth2001} established a complete constructive proof of Anderson's claim in 2001 (see also~\cite{WangYu2001,YuWangAckermann2004,YuWang2008}). In the classical proof~\cite{YuWangFourth2001,YuWang2008}, each fourth-order Hurwitz denominator $a(s)$ determines a convex feasible region $\Omega^a = \Omega_e^a \cup \Omega_t^a \subset \R^2$ bounded by an ellipse and tangent lines in the space of cubic numerator parameters $(x, y)$. Nonemptiness of the four-vertex intersection $\bigcap_{i=1}^4 \Omega^{a_i}$ is proved by intersecting chords connecting tangency points---splitting into cases according to whether the odd-part root endpoints coincide or are strictly separated---followed by two sequential small-parameter perturbations justified by compactness infima on bounded frequency intervals. \subsection{Formalization Obstacles, Proof Reconstruction, and Related Work} Our goal in this work is to construct a complete, kernel-verified formal proof of the fourth-order interval SPR synthesis theorem in the Lean~4 theorem prover~\cite{MouraUllrich2021} using the mathlib library~\cite{Mathlib2020}. As witnessed across modern formalized mathematics, paper proofs that rely on geometric region intersections, implicit nondegeneracy conventions, and qualitative ``sufficiently small parameter'' arguments often require structural reformulation into explicit algebraic invariants and quantitative bounds before they can be checked effectively by a proof assistant kernel. For instance, Dahmen, H\"olzl, and Lewis~\cite{DahmenHolzlLewis2019}, in formalizing the solution to the cap set problem in Lean, systematically separated the reuse of mathlib's algebraic hierarchy from the combinatorics reformulations needed for dependent type theory. Mahboubi and Sibut-Pinote~\cite{MahboubiSibutPinote2021}, in their formal proof of the irrationality of $\zeta(3)$, combined \emph{a posteriori} verification of expanded polynomial identities with explicit quantitative estimates to replace qualitative asymptotic steps. Likewise, Li and Paulson~\cite{LiPaulson2019}, in formalizing the Budan--Fourier theorem and polynomial root counting in Isabelle/HOL, demonstrated both the substantial infrastructure required for general complex/real root counting via Sturm chains and Cauchy indices and the utility of Taylor shifts in root isolation. Specifically, mechanizing the classical fourth-order interval SPR synthesis proof directly faces three main formalization obstacles: bridging the semantic open left-half-plane root predicate to fourth-order Routh--Hurwitz inequalities, constructing a common cubic candidate without branching on whether coefficient intervals degenerate to single points, and eliminating nonconstructive compactness infima and sequential small-parameter limits while respecting the strict quantifier order ``there exists one numerator for all box members and all real frequencies.'' To address these challenges, we develop a formalization-oriented proof reconstruction (Sections~\ref{sec:hurwitz}--\ref{sec:lift}): a degree-six horizontal translation polynomial bridges semantic Hurwitz stability directly to the third Routh--Hurwitz determinant and the two-vertex positive root band; a chord intersection anchored at the strictly separated roots of the worst-case even part provides a degeneracy-uniform cubic candidate with piecewise square-plus-linear lower bounds and a closed-form positive margin over the entire frequency half-axis; and a single explicit perturbation parameter simultaneously restores zero-frequency strictness and lifts the numerator to a monic quartic polynomial. The complete proof chain is verified by the Lean~4 kernel within 598 lines of code using only the three standard foundational axioms. \section{Formal Specification and Proof Overview}\label{sec:spec} \subsection{Mathematical Statement and Quantifier Structure} A real polynomial $a(s) \in \R[s]$ is \emph{Hurwitz stable} if all of its complex roots lie in the open left half-plane $\{z \in \C : \Ree z < 0\}$, and a polynomial family is \emph{robustly Hurwitz stable} if every member is Hurwitz stable. Following the equal-degree frequency-domain SPR convention~\cite{YuWang2008}, for a fourth-order Hurwitz-stable denominator $a(s)$ and a monic fourth-order real numerator $b(s)$, the transfer function $b(s)/a(s)$ is strictly positive real on the imaginary axis if \begin{equation}\label{eq:spr-def} \Ree\frac{b(i\omega)}{a(i\omega)} > 0 \qquad (\forall\,\omega \in \R). \end{equation} \begin{theorem}[Fourth-Order Interval SPR Synthesis~\cite{AndersonEtAl1990,YuWangFourth2001}]\label{thm:main} Let $l_j \le u_j$ ($1 \le j \le 4$) be real interval endpoints, and consider the fourth-order monic independent closed interval polynomial family \begin{equation}\label{eq:box} K = \bigl\{\, a(s) = s^4 + a_1 s^3 + a_2 s^2 + a_3 s + a_4 : l_j \le a_j \le u_j,\ 1 \le j \le 4 \,\bigr\}. \end{equation} If $K$ is robustly Hurwitz stable, then there exists a single monic real polynomial $b(s)$ of degree four such that \begin{equation}\label{eq:target} \Ree\frac{b(i\omega)}{a(i\omega)} > 0 \qquad (\forall\,a \in K,\ \forall\,\omega \in \R). \end{equation} \end{theorem} In the logical prefix $\forall K$, $\exists b$, $\forall a \in K$, $\forall \omega \in \R$ of Theorem~\ref{thm:main}, the quantifier order (uniform witness constraint) governs the entire formalization: the common numerator $b(s)$ and all intermediate construction parameters (the cubic coefficients $x, y$, the uniform frequency margin $m$, and the perturbation parameter $\varepsilon$) must be defined solely in terms of the eight box endpoints $(l_j, u_j)$, prior to introducing $a \in K$ or $\omega \in \R$. Setting the squared frequency $t = \omega^2 \ge 0$, decompose any denominator $a \in K$ and candidate real numerator $b(s)$ into their even and odd parts along the imaginary axis: \begin{equation}\label{eq:even-odd} a(i\omega) = E_a(t) + i\omega O_a(t), \qquad E_a(t) = t^2 - a_2 t + a_4, \qquad O_a(t) = a_3 - a_1 t, \end{equation} and $b(i\omega) = E_b(t) + i\omega O_b(t)$. Define the real frequency pairing polynomial \begin{equation}\label{eq:pairing} Q_{a,b}(t) \coloneqq \Ree\bigl[b(i\omega)\overline{a(i\omega)}\bigr] = E_b(t)E_a(t) + t\,O_b(t)O_a(t). \end{equation} Because every Hurwitz-stable $a \in K$ is nonvanishing on the imaginary axis, $|a(i\omega)|^2 = E_a(\omega^2)^2 + \omega^2 O_a(\omega^2)^2 > 0$ and $\Ree[b(i\omega)/a(i\omega)] = Q_{a,b}(\omega^2)/|a(i\omega)|^2$. Consequently,~\eqref{eq:target} holds for all $a \in K$ and $\omega \in \R$ if and only if $Q_{a,b}(t) > 0$ for all $a \in K$ and all $t \ge 0$. \subsection{Formal Encoding in Lean 4}\label{subsec:boundaries} In \path{Lean/SPR/Common/Hurwitz.lean} and \path{Lean/SPR/N4/Basic.lean}, the core data structures, predicates, and top-level synthesis target are formalized as follows (shown verbatim from the source files, omitting only docstrings and rendering mathematical symbols in standard notation): \begin{leancode} def SPR.IsHurwitz (a : $\R$[X]) : Prop := \quad $\forall$ z : $\C$, (a.map (algebraMap $\R$ $\C$)).IsRoot z $\to$ z.re < 0 \smallskip structure Poly4 where (a1 a2 a3 a4 : $\R$) \smallskip def Poly4.poly (a : Poly4) : $\R$[X] := \quad X \^{} 4 + C a.a1 * X \^{} 3 + C a.a2 * X \^{} 2 + C a.a3 * X + C a.a4 \smallskip structure Box4 where \quad lower : Poly4 \quad upper : Poly4 \quad ordered1 : lower.a1 $\le$ upper.a1 \quad ordered2 : lower.a2 $\le$ upper.a2 \quad ordered3 : lower.a3 $\le$ upper.a3 \quad ordered4 : lower.a4 $\le$ upper.a4 \smallskip def Box4.Contains (K : Box4) (a : Poly4) : Prop := \quad K.lower.a1 $\le$ a.a1 $\wedge$ a.a1 $\le$ K.upper.a1 $\wedge$ \quad K.lower.a2 $\le$ a.a2 $\wedge$ a.a2 $\le$ K.upper.a2 $\wedge$ \quad K.lower.a3 $\le$ a.a3 $\wedge$ a.a3 $\le$ K.upper.a3 $\wedge$ \quad K.lower.a4 $\le$ a.a4 $\wedge$ a.a4 $\le$ K.upper.a4 \smallskip def Box4.RobustlyHurwitz (K : Box4) : Prop := \quad $\forall$ a, K.Contains a $\to$ SPR.IsHurwitz a.poly \smallskip def FrequencySPR (a b : $\R$[X]) : Prop := \quad $\forall$ w : $\R$, 0 < ((b.eval$_2$ (algebraMap $\R$ $\C$) ((w : $\C$) * Complex.I)) / \quad\quad (a.eval$_2$ (algebraMap $\R$ $\C$) ((w : $\C$) * Complex.I))).re \smallskip def RobustSPRStatement : Prop := \quad $\forall$ K : Box4, K.RobustlyHurwitz $\to$ \quad\quad $\exists$ b : $\R$[X], b.Monic $\wedge$ b.natDegree = 4 $\wedge$ \quad\quad\quad $\forall$ a : Poly4, K.Contains a $\to$ FrequencySPR a.poly b \end{leancode} \subsection{Proof Overview and Dependency Architecture}\label{subsec:overview} The formal proof decomposes Theorem~\ref{thm:main} into a five-stage unidirectional pipeline, illustrated in Figure~\ref{fig:pipeline}. Table~\ref{tab:modules} summarizes the five core source files (598 lines in total) plus the public entry point \path{Lean/Main.lean}, their declaration counts, and their proof reconstructions relative to~\cite{YuWangFourth2001,YuWang2008}. \begin{figure}[!htbp] \centering \begin{tikzpicture}[ node distance=3.8mm and 6mm, stage/.style={ rectangle, rounded corners=2pt, draw=black!75, thick, fill=gray!6, text width=142mm, inner sep=4.5pt, font=\footnotesize }, arr/.style={-{Stealth[length=2.2mm,width=1.6mm]}, thick, draw=black!75} ] \node[stage] (s1) { \textbf{Stage 1: Semantic Hurwitz Predicate \& Positive Coefficients} (\path{Common/Hurwitz.lean}, 77 lines)\\ Input: $\texttt{SPR.IsHurwitz } p$ ($\Ree z < 0$ for all complex roots). Uses mathlib's Gauss--Lucas theorem to prove derivative stability (\path{hurwitz_derivative}) and induction on derivative order to prove $p.\texttt{coeff}(n) > 0$ (\path{hurwitz_coeff_pos}). }; \node[stage, below=of s1] (s2) { \textbf{Stage 2: Degree-6 Translation Polynomial \& Third Hurwitz Determinant} (\path{N4/Hurwitz.lean} Part 1, 129 lines)\\ For $a \in K$, defines the Taylor shift $a_r(s)=a(s+r)$ (\path{shifted}) and degree-6 expansion $H(r)=\Delta_3(a_r)=64r^6+\cdots+\Delta_3(a)$ (\path{determinantPolynomial}). Proves $H(r)$ has no root on $[0,\infty)$, yielding $\Delta_3(a) = H(0) > 0$ (\path{hurwitz_determinant}). }; \node[stage, below=of s2] (s3) { \textbf{Stage 3: Two-Vertex Test \& Common Positive Root Band} (\path{N4/Hurwitz.lean} Part 2, 65 lines)\\ Applies $E_*(a_3/a_1) = -\Delta_3/a_1^2 < 0$ (\path{determinant_ratio}) to two actual box vertices $a^-, a^+ \in K$ to extract the positive roots $0<\alpha 0$ (\path{stable_box_band}). }; \node[stage, below=of s3] (s4) { \textbf{Stage 4: Degeneracy-Uniform Cubic Candidate \& Closed-Form Margin} (\path{N4/Basic.lean} \& \path{N4/Construction.lean} Part 1, 170 lines)\\ Sets $x=\frac{l_1 u_1}{l_1+u_1}$ and $y=\frac{u_1\alpha+l_1\beta}{l_1+u_1}$ (\path{weights}), establishes piecewise square-plus-linear lower bounds on $[0,y]$ and $[y,\infty)$ (\path{residual_lower_left/right}), and bisects at midpoints to prove $\forall a\in K,\ \forall t\ge 0,\ F_a(t)\ge m>0$ (\path{uniform_margin}). }; \node[stage, below=of s4] (s5) { \textbf{Stage 5: Single-Step Quartic Lift, Quotient Bridge \& Final Assembly} (\path{N4/Construction.lean} Part 2, \path{N4/Synthesis.lean} \& \path{Main.lean})\\ Fixes $\varepsilon = \frac{m}{2u_2(u_2^2+1)} > 0$, proves $Q_{a,\widetilde{b}}(t) > 0$ (\path{correction_positive}), bridges via complex evaluation (\path{candidate_pairing}) to $\Ree[b(i\omega)/a(i\omega)] > 0$ (\path{quotient_positive}), and completes \path{SPR.N4.Direct.robustSPR}. }; \draw[arr] (s1) -- (s2); \draw[arr] (s2) -- (s3); \draw[arr] (s3) -- (s4); \draw[arr] (s4) -- (s5); \end{tikzpicture} \caption{Formalization pipeline and declaration dependency graph for fourth-order interval SPR synthesis.}\label{fig:pipeline} \end{figure} \begin{table}[!htbp] \centering \caption{Lean~4 module structure, code statistics, and proof reconstructions relative to~\cite{YuWangFourth2001,YuWang2008}.}\label{tab:modules} \vspace{3pt} \footnotesize \setlength{\tabcolsep}{4pt} \renewcommand{\arraystretch}{1.18} \begin{tabular}{@{}>{\raggedright\arraybackslash}p{35mm}>{\raggedright\arraybackslash}p{25mm}>{\raggedright\arraybackslash}p{40mm}>{\raggedright\arraybackslash}p{47mm}@{}} \toprule Module Path & Lines / Decls & Key Lean~4 Declarations & Proof Reconstruction vs.~\cite{YuWangFourth2001,YuWang2008} \\ \midrule \mbox{\path{Common/Hurwitz.lean}} & 77 lines (1 def, 6 thms) & \path{IsHurwitz}, \path{eval_pos}, \path{hurwitz_derivative}, \path{hurwitz_coeff_pos} & Derivative induction via mathlib's Gauss--Lucas theorem instead of quadratic root pairing \\ \mbox{\path{N4/Basic.lean}} & 80 lines (2 structs, 11 defs) & \path{Poly4}, \path{Box4}, \path{weight}, \path{middle}, \path{margin}, \path{candidate}, \path{RobustSPRStatement} & Non-strict bounds $l_j \le u_j$ preserving all degenerate boxes; parameters defined purely from $K$ \\ \mbox{\path{N4/Hurwitz.lean}} & 194 lines (3 defs, 12 thms) & \path{shifted}, \path{determinantPolynomial}, \path{hurwitz_determinant}, \path{stable_box_band} & Degree-6 translation polynomial $H(r)=\Delta_3(a(s+r))$ proving $\Delta_3(a)>0$; two-vertex root band \\ \mbox{\path{N4/Construction.lean}} & 173 lines (1 def, 7 thms) & \path{weights}, \path{residual_lower_left}, \path{residual_lower_right}, \path{uniform_margin}, \path{correction_positive} & Chords anchored at $(\alpha,\beta)$ avoiding degeneracy splits; explicit $m>0$ and $\varepsilon>0$ replacing limits \\ \mbox{\path{N4/Synthesis.lean}} \& \mbox{\path{Main.lean}} & 74 lines (3 thms) + 1 entry thm & \path{candidate_pairing}, \path{quotient_positive}, \path{synthesis}, \path{SPR.N4.Direct.robustSPR} & Deduces $a(i\omega)\ne 0$ and complex quotient positivity directly from positive real pairing \\ \bottomrule \end{tabular} \end{table} \section{Bridging Hurwitz Stability via Horizontal Translation}\label{sec:hurwitz} \subsection{Classical Proof Requirement and Formalization Obligations} The starting point of the classical synthesis proof is that every monic Hurwitz-stable quartic polynomial $a(s) = s^4 + a_1 s^3 + a_2 s^2 + a_3 s + a_4$ satisfies the two necessary algebraic conditions \begin{equation}\label{eq:hurwitz-nec} a_j > 0 \quad (1 \le j \le 4) \qquad \text{and} \qquad \Delta_3(a) \coloneqq a_1 a_2 a_3 - a_3^2 - a_1^2 a_4 > 0. \end{equation} In informal treatments,~\eqref{eq:hurwitz-nec} is either cited from the general Routh--Hurwitz theorem or derived by pairing complex-conjugate and negative real roots to factor $a(s) = (s^2 + ps + q)(s^2 + rs + h)$ with $p, q, r, h > 0$, which expands to $\Delta_3(a) = pr\bigl[(q - h)^2 + (p + r)(ph + rq)\bigr] > 0$. In an interactive theorem prover, however, the hypothesis is given semantically by the root predicate $\texttt{SPR.IsHurwitz}(a.\texttt{poly})$ ($\Ree z < 0$ for all complex roots). Formalizing either paper argument directly would impose a heavy auxiliary obligation: \begin{enumerate}[label=(\roman*),leftmargin=2.2em] \item Formalizing the existence of a real factorization into two monic quadratic factors from the Fundamental Theorem of Algebra and complex conjugation in mathlib, and linking the open left-half-plane root condition to positivity of each quadratic factor's coefficients; or \item Developing a full complex half-plane root-counting theory via Cauchy indices, Sturm chains, or the argument principle, as carried out by Li and Paulson~\cite{LiPaulson2019} in Isabelle/HOL. \end{enumerate} Because fourth-order synthesis requires only the one-way necessary conditions~\eqref{eq:hurwitz-nec}, building general root-counting or conjugate-factorization machinery solely for degree four would disproportionately expand the formalization effort. \subsection{Gauss--Lucas Derivative Induction and the Degree-Six Translation Polynomial} To establish~\eqref{eq:hurwitz-nec} directly from $\texttt{SPR.IsHurwitz}$ with minimal infrastructure, we split the bridge into a degree-independent derivative induction and an \emph{a posteriori} polynomial translation identity. First, mathlib provides the real-root sign lemma \path{zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg} (if $p \in \R[X]$ has nonnegative leading coefficient and all real roots strictly below $x$, then $p(x) > 0$) and the complex Gauss--Lucas theorem \path{Polynomial.rootSet_derivative_subset_convexHull_rootSet} (the roots of $p'$ lie in the convex hull of the roots of $p$). In \path{Lean/SPR/Common/Hurwitz.lean}, we combine the convexity of $\{z \in \C : \Ree z < 0\}$ with the Gauss--Lucas theorem to prove that differentiation preserves Hurwitz stability (\path{hurwitz_derivative}), and induct on the derivative order $n$ to establish $n!\,p.\texttt{coeff}(n) = (p^{(n)})(0) > 0$: \begin{leancode} theorem hurwitz\_coeff\_pos \{p : $\R$[X]\} (hp : IsHurwitz p) \quad\quad (hlc : 0 < p.leadingCoeff) (n : $\mathbb{N}$) (hn : n $\le$ p.natDegree) : \quad\quad 0 < p.coeff n \end{leancode} Instantiating \path{hurwitz_coeff_pos} at $n = 3, 2, 1, 0$ immediately yields $a_1, a_2, a_3, a_4 > 0$ (\path{hurwitz_coefficients}). Second, to prove $\Delta_3(a) > 0$ without factoring $a(s)$, we use the observation that when $a_1, a_3 > 0$, the vanishing of $\Delta_3(a)$ characterizes the presence of a purely imaginary root $s = i\sqrt{a_3/a_1}$. Consequently, if we apply a horizontal Taylor shift by $r \in \R$, \begin{equation}\label{eq:shifted-def} a_r(s) \coloneqq a(s + r) = s^4 + a_{r,1}s^3 + a_{r,2}s^2 + a_{r,3}s + a_{r,4}, \end{equation} then any zero of $\Delta_3(a_r) = 0$ at $r \ge 0$ produces a purely imaginary root $i\omega_r$ of $a_r(s)$ and hence a complex root $z = r + i\omega_r$ of $a(s)$ in the closed right half-plane $\Ree z = r \ge 0$, contradicting $\texttt{SPR.IsHurwitz}(a.\texttt{poly})$. Following the \emph{a posteriori} algebraic verification paradigm~\cite{MahboubiSibutPinote2021}, we define the expanded degree-six polynomial $H(r) \coloneqq \Delta_3(a_r)$ (\path{determinantPolynomial} in \path{Lean/SPR/N4/Hurwitz.lean}; see Appendix~\ref{app:translation}, equation~\eqref{eq:det-poly-full} for the full expansion): \begin{equation}\label{eq:det-poly-short} H(r) = 64r^6 + 96a_1 r^5 + (48a_1^2 + 32a_2)r^4 + \cdots + \Delta_3(a), \end{equation} and verify the polynomial evaluation identity $H(r) = \Delta_3(a_r)$ (\path{determinantPolynomial_eval}) by a three-line \texttt{ring} proof. This yields a self-contained proof of Lemma~\ref{lem:hurwitz-det}. \begin{lemma}[Positivity of the Third Hurwitz Determinant, \path{hurwitz_determinant}]\label{lem:hurwitz-det} If a monic quartic polynomial $a(s) = s^4 + a_1 s^3 + a_2 s^2 + a_3 s + a_4$ satisfies $\texttt{SPR.IsHurwitz}(a.\texttt{poly})$, then $a_1, a_2, a_3, a_4 > 0$ and $\Delta_3(a) = a_1 a_2 a_3 - a_3^2 - a_1^2 a_4 > 0$. \end{lemma} \begin{proof} Positivity of $a_1, a_2, a_3, a_4$ is given by \path{hurwitz_coefficients}. The polynomial $H(r)$ in~\eqref{eq:det-poly-short} has degree six and positive leading coefficient $64 > 0$. Suppose $H(r) = 0$ for some $r \in \R$. If $r \ge 0$, then $a_1, a_2, a_3 > 0$ imply $a_{r,1} = a_1 + 4r > 0$ and $a_{r,3} = a_3 + 2a_2 r + 3a_1 r^2 + 4r^3 > 0$. Setting $\omega_r = \sqrt{a_{r,3}/a_{r,1}} > 0$, direct algebraic verification shows $a_r(i\omega_r) = 0$ (\path{determinant_zero_root}; see Appendix~\ref{app:translation}), and the shift identity $a_r(z) = a(r + z)$ (\path{eval_shifted}) gives a root $z = r + i\omega_r$ of $a(s)$ with $\Ree z = r \ge 0$, contradicting $\texttt{SPR.IsHurwitz}(a.\texttt{poly})$. Thus every real root of $H(r)$ is strictly negative, and applying \path{zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg} at $r = 0$ yields $\Delta_3(a) = H(0) > 0$. \end{proof} \subsection{Resulting Formal Interface: Two-Vertex Test and Common Positive Root Band} Because the lower endpoint tuple $(l_1, l_2, l_3, l_4)$ belongs to $K$ (\path{lower_contains}), Lemma~\ref{lem:hurwitz-det} implies $0 < l_j \le u_j$ ($1 \le j \le 4$). Set \begin{equation}\label{eq:abbreviations} l = l_1, \qquad u = u_1, \qquad A = l_2, \qquad C = u_4, \qquad U = u_2, \end{equation} and define the worst-case even part across the box: \begin{equation}\label{eq:worst-even} E_*(t) \coloneqq t^2 - At + C, \qquad\text{so that}\qquad E_a(t) \le E_*(t) \quad (\forall\,a \in K,\ \forall\,t \ge 0). \end{equation} Evaluating the identity $E_a(a_3/a_1) = -\Delta_3(a)/a_1^2$ (\path{determinant_ratio}) at the two Kharitonov vertices (\path{aL} and \path{aR} in \path{stable_box_band}) \begin{equation}\label{eq:two-vertices} a^-(s) = s^4 + u s^3 + A s^2 + l_3 s + C \in K, \qquad a^+(s) = s^4 + l s^3 + A s^2 + u_3 s + C \in K \end{equation} packages Stage~2 into the root-band interface \path{stable_box_band} consumed by Stage~4: \begin{lemma}[Common Positive Root Band, \path{stable_box_band}]\label{lem:root-band} Suppose $K$ is robustly Hurwitz stable. Then $D \coloneqq A^2 - 4C > 0$, and $E_*(t) = t^2 - At + C$ has two distinct positive roots \begin{equation}\label{eq:roots} \alpha = \frac{A - \sqrt{D}}{2} > 0, \qquad \beta = \frac{A + \sqrt{D}}{2} > \alpha, \end{equation} satisfying $A = \alpha + \beta$, $C = \alpha\beta$, and \begin{equation}\label{eq:root-band} 0 < \alpha < \frac{l_3}{u} \le \frac{u_3}{l} < \beta. \end{equation} In particular, whether or not any intervals $[l_j, u_j]$ degenerate to single points, the two odd-endpoint slacks \begin{equation}\label{eq:slacks} \delta_- \coloneqq l_3 - u\alpha > 0, \qquad \delta_+ \coloneqq l\beta - u_3 > 0 \end{equation} are strictly positive. \end{lemma} \begin{proof} Applying Lemma~\ref{lem:hurwitz-det} and $E_a(a_3/a_1) = -\Delta_3(a)/a_1^2$ to $a^-, a^+ \in K$ yields \begin{equation}\label{eq:negative-even-tests} E_*\!\left(\frac{l_3}{u}\right) = -\frac{\Delta_3(a^-)}{u^2} < 0, \qquad E_*\!\left(\frac{u_3}{l}\right) = -\frac{\Delta_3(a^+)}{l^2} < 0. \end{equation} From $E_*(l_3/u) < 0$ we obtain $D = A^2 - 4C > (2l_3/u - A)^2 \ge 0$, which together with $A, C > 0$ gives $0 < \alpha < \beta$ and $E_*(t) = (t - \alpha)(t - \beta)$. Since $E_*(q) < 0 \iff \alpha < q < \beta$ and $0 < l_3/u \le u_3/l$, inequalities~\eqref{eq:negative-even-tests} immediately imply~\eqref{eq:root-band} and~\eqref{eq:slacks}. \end{proof} \section{Unified Cubic Candidate and Explicit Frequency Margin}\label{sec:cubic} \subsection{Classical Proof Requirement and the Degeneracy Branching Obstacle} For a monic cubic candidate $b_0(s) = s^3 + xs^2 + ys$ without constant or quartic terms, we have $E_{b_0}(t) = -xt$ and $O_{b_0}(t) = y - t$, so the real frequency pairing $Q_{a,b_0}(t)$ factors through $t$: \begin{equation}\label{eq:residual} F_a(t) \coloneqq \frac{Q_{a,b_0}(t)}{t} = a_1(t - y)t + a_3(y - t) - x E_a(t). \end{equation} In the classical proof~\cite{YuWangFourth2001,YuWang2008}, the set of $(x,y)$ where $F_a(t) > 0$ for all $t \ge 0$ is described geometrically as $\Omega^a = \Omega_e^a \cup \Omega_t^a$, and nonemptiness of $\Omega^{a^-} \cap \Omega^{a^+}$ is proved by intersecting chords anchored at the odd-part roots $(0, l_3/u)$ and $(0, u_3/l)$. When $l = u$ and $l_3 = u_3$ (for example, when the first and third coefficient intervals degenerate to single points), $l_3/u$ and $u_3/l$ coincide, forcing the classical proof to split into two cases ($l_3/u = u_3/l$ vs.\ $l_3/u < u_3/l$) with different candidate formulas; moreover, once $(x,y) \in \bigcap_{i=1}^4 \Omega^{a_i}$ is chosen, positivity of $F_a(t)$ is used qualitatively via compactness on bounded frequency intervals. In a formal proof, branching the definition of $(x,y)$ on $l_3/u = u_3/l$ vs.\ $l_3/u < u_3/l$ would duplicate every subsequent algebraic identity and frequency bound across two candidate definitions, while invoking compactness infima would require formalizing joint continuity and asymptotic uniformity over $K \times [0, \infty)$. \subsection{Unified Chord Intersection Anchored at the Even-Part Roots} To eliminate case distinctions on interval degeneracy from the candidate definition, we observe in \path{Lean/SPR/N4/Basic.lean} and \path{Construction.lean} that while $l_3/u$ and $u_3/l$ may coincide, the two positive roots $\alpha < \beta$ of $E_*(t)$ guaranteed by Lemma~\ref{lem:root-band} \textbf{are always strictly separated} (even for a singleton family, Hurwitz stability forces $D > 0$ and $\alpha < \beta$). We therefore anchor the two chords at $(0, \alpha), (u, \beta)$ and $(0, \beta), (l, \alpha)$: \begin{equation}\label{eq:chord-lines} u y - x\beta = (u - x)\alpha, \qquad l y - x\alpha = (l - x)\beta. \end{equation} Solving~\eqref{eq:chord-lines} yields the single closed-form parameter pair (\path{weight} and \path{middle} in \path{Basic.lean}): \begin{equation}\label{eq:xy} x = \frac{lu}{l + u}, \qquad y = \frac{u\alpha + l\beta}{l + u}, \qquad b_0(s) = s^3 + xs^2 + ys. \end{equation} \begin{lemma}[Algebraic Properties of the Unified Cubic Parameters, \path{weights}]\label{lem:weights} For any real numbers satisfying $0 < l \le u$ and $0 < \alpha < \beta$, the parameters $x, y$ in~\eqref{eq:xy} satisfy~\eqref{eq:chord-lines} and \begin{equation}\label{eq:xy-range} 0 < x < l \le u, \qquad \alpha < y < \beta. \end{equation} \end{lemma} \begin{proof} Since $l, u > 0$ and $\alpha < \beta$, we have $l + u > 0$, $l - x = l^2/(l + u) > 0$, $u - x = u^2/(l + u) > 0$, $y - \alpha = l(\beta - \alpha)/(l + u) > 0$, and $\beta - y = u(\beta - \alpha)/(l + u) > 0$. Clearing denominators (\texttt{field\_simp; ring}) verifies both identities in~\eqref{eq:chord-lines}. \end{proof} \subsection{Piecewise Square-Plus-Linear Lower Bounds and Closed-Form Margin} The chord equations~\eqref{eq:chord-lines} are designed so that when $a_1, a_2, a_3, a_4$ are replaced by their worst-case box endpoints on $[0, y]$ and $[y, \infty)$, respectively, the even-part term $-x E_*(t) = -x(t-\alpha)(t-\beta)$ combines with the leading odd term into an exact square around $\alpha$ or $\beta$, leaving the strictly positive linear slack $\delta_-(y-t)$ or $\delta_+(t-y)$ from Lemma~\ref{lem:root-band}. \begin{lemma}[Whole-Box Piecewise Square-Plus-Linear Lower Bounds, \path{residual_lower_left} and \path{residual_lower_right}]\label{lem:square-bounds} For every $a \in K$, the reduced pairing $F_a(t)$ in~\eqref{eq:residual} satisfies \begin{align} F_a(t) &\ge (u - x)(t - \alpha)^2 + \delta_-(y - t) \qquad (0 \le t \le y), \label{eq:left-square}\\ F_a(t) &\ge (l - x)(t - \beta)^2 + \delta_+(t - y) \qquad (t \ge y). \label{eq:right-square} \end{align} \end{lemma} The step-by-step algebraic derivation of Lemma~\ref{lem:square-bounds} is given in Appendix~\ref{app:piecewise}. Observe that in~\eqref{eq:left-square}, as $t \in [0, y]$ approaches $y$, the linear slack $\delta_-(y - t)$ vanishes while the square term $(u - x)(t - \alpha)^2$ is bounded below by $(u-x)(y-\alpha)^2 > 0$; conversely, near $t = \alpha$, the linear slack is bounded below by $\delta_-(y-\alpha) > 0$. Bisecting $[\alpha, y]$ at $(\alpha + y)/2$ and $[y, \beta]$ at $(\beta + y)/2$ converts this complementarity into an explicit closed-form positive margin $m > 0$ over $[0, \infty)$ (\path{margin} in \path{Basic.lean} and \path{uniform_margin} in \path{Construction.lean}): \begin{leancode} theorem uniform\_margin \{K : Box4\} \{$\alpha$ $\beta$ : $\R$\} \quad\quad (hl : 0 < K.lower.a1) (hab : $\alpha$ < $\beta$) \quad\quad (hA : K.lower.a2 = $\alpha$ + $\beta$) (hC : K.upper.a4 = $\alpha$ * $\beta$) \quad\quad (hlo : K.upper.a1 * $\alpha$ < K.lower.a3) \quad\quad (hhi : K.upper.a3 < K.lower.a1 * $\beta$) : \quad\quad let x := weight K.lower.a1 K.upper.a1 \quad\quad let y := middle K.lower.a1 K.upper.a1 $\alpha$ $\beta$ \quad\quad 0 < margin K x y $\alpha$ $\beta$ $\wedge$ \quad\quad $\forall$ a, K.Contains a $\to$ $\forall$ t, 0 $\le$ t $\to$ margin K x y $\alpha$ $\beta$ $\le$ residual a x y t \end{leancode} \begin{lemma}[Explicit Uniform Frequency Margin on $[0, \infty)$, \path{uniform_margin}]\label{lem:uniform-margin} Set $d_- \coloneqq y - \alpha > 0$ and $d_+ \coloneqq \beta - y > 0$, and define the box-dependent constant \begin{equation}\label{eq:margin} m \coloneqq \min\left\{ \frac{\delta_- d_-}{2},\ \frac{(u - x)d_-^2}{4},\ \frac{\delta_+ d_+}{2},\ \frac{(l - x)d_+^2}{4} \right\} > 0. \end{equation} Then for every $a \in K$ and every $t \ge 0$, \begin{equation}\label{eq:uniform-margin} F_a(t) \ge m > 0 \qquad \text{and} \qquad Q_{a,b_0}(t) = t\,F_a(t) \ge mt. \end{equation} \end{lemma} \begin{proof} By Lemmas~\ref{lem:root-band} and~\ref{lem:weights}, $\delta_\pm > 0$, $d_\pm > 0$, $u - x > 0$, and $l - x > 0$, so all four arguments of $\min$ in~\eqref{eq:margin} are strictly positive and $m > 0$. Fix $a \in K$ and $t \ge 0$. For $0 \le t \le y$ (\path{left_margin}): if $t \le (\alpha + y)/2$, then $y - t \ge d_-/2$ and~\eqref{eq:left-square} gives $F_a(t) \ge \delta_- d_-/2 \ge m$; if $(\alpha + y)/2 < t \le y$, then $t - \alpha > d_-/2 > 0$ and~\eqref{eq:left-square} gives $F_a(t) \ge (u - x)d_-^2/4 \ge m$. Symmetrically, for $t \ge y$ (\path{right_margin}), splitting~\eqref{eq:right-square} at $(\beta + y)/2$ yields $F_a(t) \ge \delta_+ d_+/2 \ge m$ when $t \ge (\beta + y)/2$ and $F_a(t) \ge (l - x)d_+^2/4 \ge m$ when $y \le t < (\beta + y)/2$. \end{proof} \section{Single-Step Quartic Perturbation and Quotient Bridge}\label{sec:lift} \subsection{Classical Proof Requirement and the Single-Step Perturbation Budget} By~\eqref{eq:uniform-margin}, the cubic candidate $b_0(s) = s^3 + xs^2 + ys$ satisfies $Q_{a,b_0}(t) \ge mt > 0$ for all $t > 0$, but vanishes at $t = 0$ ($Q_{a,b_0}(0) = 0$) and has degree three rather than four. In~\cite{YuWangFourth2001,YuWang2008}, this is resolved by two sequential perturbations: first adding a sufficiently small constant $\varepsilon_1 > 0$ to achieve strict positivity at $t = 0$, and then adding $\varepsilon_2 s^4$ with a second sufficiently small parameter $\varepsilon_2 > 0$. To avoid nested existential limits and strictly respect the quantifier order $\forall K \to \exists b \to \forall a \in K \to \forall \omega \in \R$, we perturb the constant and quartic terms simultaneously by adding $\varepsilon(s^4 + 1)$. Since $(i\omega)^4 + 1 = t^2 + 1 > 0$ for $t = \omega^2$, we define the unnormalized and normalized quartic numerators (\path{candidate} in \path{Basic.lean}): \begin{equation}\label{eq:corrected-numerator} \widetilde{b}(s) \coloneqq b_0(s) + \varepsilon(s^4 + 1), \qquad b(s) \coloneqq \frac{\widetilde{b}(s)}{\varepsilon} = s^4 + \frac{1}{\varepsilon}s^3 + \frac{x}{\varepsilon}s^2 + \frac{y}{\varepsilon}s + 1. \end{equation} For any $a \in K$, the real pairing of $\widetilde{b}(s)$ with $a(s)$ (\path{correctedPairing} in \path{Construction.lean}) is \begin{equation}\label{eq:lift-identity} Q_{a,\widetilde{b}}(t) = t\,F_a(t) + \varepsilon(t^2 + 1)E_a(t). \end{equation} To choose a single $\varepsilon > 0$ depending only on $K$ that works for all $a \in K$ and all $t \ge 0$, we bound the region where the perturbation term $\varepsilon(t^2 + 1)E_a(t)$ can be negative: \begin{itemize} \item At $t = 0$, $Q_{a,\widetilde{b}}(0) = \varepsilon E_a(0) = \varepsilon a_4 \ge \varepsilon l_4 > 0$ for any $\varepsilon > 0$; \item For $t > 0$ with $E_a(t) \ge 0$, the perturbation $\varepsilon(t^2 + 1)E_a(t) \ge 0$ reinforces $t F_a(t) \ge mt > 0$; \item For $t > 0$ with $E_a(t) = t^2 - a_2 t + a_4 < 0$, since $a_4 \ge l_4 > 0$ and $a_2 \le u_2 = U$, we have $t^2 < t^2 + a_4 < a_2 t \le Ut$. Dividing by $t > 0$ yields the a priori frequency bound $0 < t < U$, while dropping $t^2 + a_4 > 0$ gives $E_a(t) > -a_2 t \ge -Ut$. \end{itemize} Consequently, whenever $E_a(t) < 0$, $t$ is confined to $(0, U)$ and $(t^2 + 1)E_a(t) \ge -U(U^2 + 1)t$, which is linear in $t$ just like the lower bound $mt$ for $t F_a(t)$. Setting \begin{equation}\label{eq:epsilon} \varepsilon \coloneqq \frac{m}{2U(U^2 + 1)} > 0 \qquad (U = u_2 > 0) \end{equation} ensures that the negative perturbation consumes at most half of the linear margin $mt$ (\path{correction_positive}): \begin{lemma}[Strict Positivity of the Perturbed Quartic Pairing, \path{correction_positive}]\label{lem:strict-lift} With $m > 0$ defined by~\eqref{eq:margin} and $\varepsilon > 0$ defined by~\eqref{eq:epsilon}, the perturbed pairing~\eqref{eq:lift-identity} satisfies $Q_{a,\widetilde{b}}(t) > 0$ for every $a \in K$ and every $t \ge 0$. \end{lemma} \begin{proof} For any $a \in K$, we have $a_4 \ge l_4 > 0$ and $a_2 \le U$. (1) If $t = 0$, then $Q_{a,\widetilde{b}}(0) = \varepsilon a_4 > 0$. (2) If $t > 0$ and $E_a(t) \ge 0$, Lemma~\ref{lem:uniform-margin} gives $Q_{a,\widetilde{b}}(t) \ge mt > 0$. (3) If $t > 0$ and $E_a(t) < 0$, the bounds $0 < t < U$, $t^2 + 1 \le U^2 + 1$, and $E_a(t) \ge -Ut$ give $(t^2 + 1)E_a(t) \ge -U(U^2 + 1)t$. Combining this with~\eqref{eq:uniform-margin} and~\eqref{eq:epsilon} yields \[ Q_{a,\widetilde{b}}(t) \ge mt - \varepsilon U(U^2 + 1)t = \frac{m}{2}t > 0. \qedhere \] \end{proof} \subsection{Complex Quotient Bridge and Assembly of the Main Theorem}\label{subsec:quotient-bridge} In the final module (\path{Lean/SPR/N4/Synthesis.lean}), the real inequality $Q_{a,\widetilde{b}}(\omega^2) > 0$ is connected to the complex quotient predicate $\texttt{FrequencySPR}(a.\texttt{poly}, b)$. In mathlib, complex division $B / A$ is a total function (evaluating to $0$ if $A = 0$) with real part $(B / A).\texttt{re} = (B.\texttt{re} \cdot A.\texttt{re} + B.\texttt{im} \cdot A.\texttt{im}) / \texttt{Complex.normSq}(A)$. Rather than proving $a(i\omega) \ne 0$ separately from $\texttt{SPR.IsHurwitz}$, \path{Synthesis.lean} discharges both nonvanishing of the denominator and positivity of the quotient in two steps: \begin{enumerate}[label=(\roman*),leftmargin=2.2em] \item \path{candidate_pairing}: Using the imaginary-axis evaluation decomposition \path{eval_imaginary} and $\varepsilon \ne 0$, \texttt{field\_simp} and \texttt{ring} prove that for all $\omega \in \R$, \begin{equation}\label{eq:candidate-pairing-lean} \varepsilon\bigl[\Ree b(i\omega)\,\Ree a(i\omega) + \Imm b(i\omega)\,\Imm a(i\omega)\bigr] = Q_{a,\widetilde{b}}(\omega^2). \end{equation} \item \path{quotient_positive}: Since $\varepsilon > 0$ and $Q_{a,\widetilde{b}}(\omega^2) > 0$,~\eqref{eq:candidate-pairing-lean} implies $\Ree b(i\omega)\,\Ree a(i\omega) + \Imm b(i\omega)\,\Imm a(i\omega) > 0$. If $a(i\omega)$ were zero, this inner product would vanish; hence $a(i\omega) \ne 0$, $|a(i\omega)|^2 = \texttt{Complex.normSq}(a(i\omega)) > 0$, and dividing by $|a(i\omega)|^2$ yields $\Ree[b(i\omega)/a(i\omega)] > 0$. \end{enumerate} The main theorem \path{synthesis} (exported as \path{SPR.N4.Direct.robustSPR} in \path{Lean/Main.lean}) assembles all five stages (shown verbatim from \path{Synthesis.lean}, omitting only the three lines checking $\varepsilon > 0$): \begin{leancode} theorem synthesis (K : Box4) (hK : K.RobustlyHurwitz) : \quad\quad $\exists$ b : $\R$[X], b.Monic $\wedge$ b.natDegree = 4 $\wedge$ \quad\quad\quad $\forall$ a : Poly4, K.Contains a $\to$ FrequencySPR a.poly b := by \quad obtain $\langle\alpha, \beta,$ h$\alpha$, hab, hA, hC, hlo, hhi, hl1, hl4, hU$\rangle$ := \quad\quad stable\_box\_band hK \quad let x := weight K.lower.a1 K.upper.a1 \quad let y := middle K.lower.a1 K.upper.a1 $\alpha$ $\beta$ \quad let m := margin K x y $\alpha$ $\beta$ \quad obtain $\langle$hm, hF$\rangle$ := uniform\_margin hl1 hab hA hC hlo hhi \quad let U := K.upper.a2 \quad let $\varepsilon$ := m / (2 * U * (U \^{} 2 + 1)) \quad ... \quad refine $\langle$(candidate x y $\varepsilon$).poly, (poly\_degree \_).2, (poly\_degree \_).1, ?\_$\rangle$ \quad intro a ha \quad apply quotient\_positive h$\varepsilon$ \quad intro t ht \quad exact correction\_positive hm hU h$\varepsilon$ hsmall ha.2.2.2.1 \quad\quad (hl4.trans\_le ha.2.2.2.2.2.2.1) ht (hF a ha t ht) \end{leancode} \begin{remark}[Paper-Level Supplement on the Hurwitz Stability of the Constructed Numerator]\label{rem:numerator-hurwitz} As noted in Section~\ref{subsec:boundaries}, the formalized theorem \path{SPR.N4.Direct.robustSPR} verifies the equal-degree imaginary-axis predicate \path{FrequencySPR}. Mathematically, the monic quartic numerator $b(s)$ in~\eqref{eq:corrected-numerator} is itself Hurwitz stable, as can be seen in two ways: (a) \emph{Analytic route}: Fix any $a \in K$. Since $a(s)$ is Hurwitz stable, $f(s) = b(s)/a(s)$ is analytic on $\Ree s \ge 0$, satisfies $\lim_{|s|\to\infty} f(s) = 1$, and has $\Ree f(i\omega) > 0$ on $\R$; applying the harmonic minimum principle on large right-half disks shows $\Ree f(s) > 0$ on $\Ree s \ge 0$, so $b(s)$ has no zeros in $\Ree s \ge 0$. (b) \emph{Algebraic route}: For $b(s) = s^4 + \varepsilon^{-1}s^3 + (x/\varepsilon)s^2 + (y/\varepsilon)s + 1$, all four coefficients are positive and $\Delta_3(b) = (xy - \varepsilon y^2 - \varepsilon)/\varepsilon^3$; replacing $\varepsilon$ in~\eqref{eq:epsilon} by $\varepsilon^* = \min\bigl\{\frac{m}{2U(U^2+1)},\, \frac{xy}{2(y^2+1)}\bigr\} > 0$ guarantees $\Delta_3(b) > 0$ directly while preserving Lemma~\ref{lem:strict-lift}. Neither argument is encoded as a separate Lean declaration in the current repository. \end{remark} \section{Illustrative Examples, Limitations, and Reproducibility}\label{sec:examples} \subsection{Nondegenerate Box and Completely Degenerate Singleton Examples} We illustrate how the formalized formulas operate identically on a full-width four-interval box and on a completely degenerate singleton family. \paragraph{Example 1 (Nondegenerate Four-Interval Box).} Consider the robustly Hurwitz-stable fourth-order interval family $K$ defined by \[ a_1 \in [2, 3], \qquad a_2 \in [5, 6], \qquad a_3 \in [4, 6], \qquad a_4 \in [3, 4]. \] Here $l = 2$, $u = 3$, $A = 5$, $C = 4$, and $U = 6$. The worst-case even part $E_*(t) = t^2 - 5t + 4 = (t - 1)(t - 4)$ has discriminant $D = 9$ and positive roots $\alpha = 1$, $\beta = 4$, with $1 = \alpha < l_3/u = 4/3 < u_3/l = 3 < 4 = \beta$ and endpoint slacks $\delta_- = 4 - 3 = 1 > 0$, $\delta_+ = 8 - 6 = 2 > 0$. Equations~\eqref{eq:xy} and~\eqref{eq:margin} give \[ x = \frac{6}{5}, \qquad y = \frac{11}{5}, \qquad d_- = \frac{6}{5}, \qquad d_+ = \frac{9}{5}, \qquad m = \min\left\{\frac{3}{5},\ \frac{81}{125},\ \frac{9}{5},\ \frac{81}{125}\right\} = \frac{3}{5}. \] With $2U(U^2 + 1) = 444$, equation~\eqref{eq:epsilon} gives $\varepsilon = \frac{3/5}{444} = \frac{1}{740}$, and~\eqref{eq:corrected-numerator} yields the exact integer-coefficient monic common SPR numerator \begin{equation}\label{eq:example-nondeg} b(s) = s^4 + 740s^3 + 888s^2 + 1628s + 1. \end{equation} \paragraph{Example 2 (Completely Degenerate Singleton Family).} Consider the singleton family $K = \{(s + 1)^4 = s^4 + 4s^3 + 6s^2 + 4s + 1\}$, where all four intervals have zero width: $l = u = 4$, $A = U = 6$, $l_3 = u_3 = 4$, and $l_4 = C = 1$. Here the odd-part root endpoints $l_3/u = u_3/l = 1$ coincide. Nevertheless, $E_*(t) = t^2 - 6t + 1$ has $D = 32 > 0$ and strictly separated roots $\alpha = 3 - 2\sqrt{2} < \beta = 3 + 2\sqrt{2}$. Evaluating~\eqref{eq:xy}--\eqref{eq:epsilon} without modification gives $x = 2$, $y = 3$, $\delta_\pm = 8(\sqrt{2} \pm 1) > 0$, $d_\pm = 2\sqrt{2}$, $m = \min\{8(2 - \sqrt{2}),\, 4,\, 8(2 + \sqrt{2}),\, 4\} = 4$, $\varepsilon = 4/444 = 1/111$, and \begin{equation}\label{eq:example-deg} b(s) = s^4 + 111s^3 + 222s^2 + 333s + 1. \end{equation} While $b(s) = (s+1)^4$ trivially satisfies $b(i\omega)/a(i\omega) \equiv 1 > 0$ for this singleton, Example~2 shows that the degeneracy-uniform formulas produce a valid witness without branching on interval widths. \subsection{Conservative Margins and Practical Control Limitations}\label{subsec:limitations} As Examples~1 and~2 illustrate, the constructed monic numerators have relatively large intermediate coefficients ($1/\varepsilon \sim 10^2\text{--}10^3$). This is a direct consequence of three conservative bounding choices made to streamline formal verification: \begin{enumerate}[label=(\arabic*),leftmargin=2.2em] \item \textbf{Decoupled worst-case even and odd bounds}: Stages~3 and~4 bound $E_a(t)$ globally by $E_*(t) = t^2 - l_2 t + u_4$ while independently setting $(a_1, a_3)$ to $(u_1, l_3)$ on $[0,y]$ and $(l_1, u_3)$ on $[y,\infty)$; \item \textbf{Midpoint bisection for the uniform margin}: To avoid formalizing constrained quadratic minimization and vertex-location case splits, Lemma~\ref{lem:uniform-margin} bounds the sum of the square and linear terms via midpoint bisection; \item \textbf{Cubic scaling in the perturbation denominator}: Lemma~\ref{lem:strict-lift} bounds $(t^2+1)E_a(t)$ over $0 < t < U = u_2$ by $-U(U^2+1)t$, causing $\varepsilon^{-1} = 2U(U^2+1)/m$ to scale cubically with $u_2$. \end{enumerate} Accordingly, our explicit formulas are designed to provide an algebraically transparent, kernel-checkable proof of universal mathematical existence, rather than to optimize controller gain or numerical conditioning. In practical control synthesis, once existence is guaranteed by Theorem~\ref{thm:main}, one can select well-conditioned numerator coefficients within the nonempty convex intersection $\bigcap_{i=1}^4 \Omega^{a_i}$ via linear matrix inequalities (LMIs) or convex optimization~\cite{YuWang2008}. \subsection{Library Reuse, Project Infrastructure, and Reproducibility}\label{subsec:repro} Following the reporting practice of~\cite{DahmenHolzlLewis2019}, we distinguish three categories of formal components (all new code resides in the project namespace \path{SPR} and has not been upstreamed to mathlib, so we do not claim it as a mathlib contribution): \begin{itemize} \item \textbf{Reused mathlib infrastructure}: Univariate polynomials (\path{Polynomial}) and complex evaluation (\texttt{eval}$_2$), the complex Gauss--Lucas theorem (\path{rootSet_derivative_subset_convexHull_rootSet}), the real-root sign lemma (\path{zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg}), real square roots (\path{Real.sqrt}), complex norm-square positivity (\path{Complex.normSq_pos}), and arithmetic/ring automation (\texttt{ring}, \texttt{field\_simp}, \texttt{linarith}, \texttt{nlinarith}, \texttt{positivity}). \item \textbf{Degree-independent project infrastructure (\path{Lean/SPR/Common/Hurwitz.lean})}: Defines the semantic predicate \path{SPR.IsHurwitz} for polynomials of arbitrary degree and proves positivity on $[0,\infty)$ (\path{eval_pos}), stability of derivatives (\path{hurwitz_derivative}), and strict positivity of all coefficients (\path{hurwitz_coeff_pos}). This module places no restriction on polynomial degree and is reusable across higher-order SPR formalizations. \item \textbf{Fourth-order synthesis and axiom auditor (\path{Lean/SPR/N4/}, \path{Main.lean}, \path{Audit.lean})}: The four modules in \path{Lean/SPR/N4/} (521 lines, 22 explicit theorem declarations, plus 1 entry theorem in \path{Main.lean}, generating 58 fourth-order theorem constants in the compiled environment) implement Stages~2--5. During \texttt{lake build}, \path{Lean/Audit.lean} traverses the environment's constant table via \path{Lean.collectAxioms} to verify that every theorem (including private helpers) depends only on Lean's three standard axioms (\path{propext}, \path{Classical.choice}, and \path{Quot.sound}), validated against a negative test injecting a forbidden axiom. \end{itemize} The formalization is locked to Lean~4.30.0 and mathlib~v4.30.0. All source files, toolchain locks, and build instructions are publicly available at \url{https://github.com/dgjszy/quartic-spr-proof}, where running \texttt{lake build} replays the complete verification and axiom audit. \section{Conclusion}\label{sec:conclusion} We have presented a formalization-oriented proof reconstruction and complete Lean~4 verification of the fourth-order interval SPR synthesis theorem of Yu and Wang~\cite{YuWangFourth2001}. By combining a degree-six horizontal translation polynomial for the third Hurwitz determinant, a degeneracy-uniform chord-intersection candidate, piecewise square-plus-linear lower bounds with an explicit frequency margin, and a quantifier-preserving single-step quartic perturbation, the formal proof covers all nondegenerate and degenerate fourth-order interval boxes and all real frequencies within 598 lines of kernel-checked Lean~4 code. \section*{Acknowledgements} Generative AI tools were used to assist with algebraic calculations, proof development, and manuscript editing. All AI-generated suggestions were verified against the mathematical arguments and the formal development; the formal claims are supported by Lean kernel checking, and full responsibility for the final manuscript rests with the authors. The complete Lean~4 formalization is publicly available at \url{https://github.com/dgjszy/quartic-spr-proof}. \appendix \section{Algebraic Expansions and Piecewise Lower-Bound Details}\label{app:details} \subsection{Horizontal Translation Polynomial and Third Hurwitz Determinant}\label{app:translation} For a monic quartic polynomial $a(s) = s^4 + a_1 s^3 + a_2 s^2 + a_3 s + a_4$ and $r \in \R$, binomial expansion of the horizontally shifted polynomial $a_r(s) = a(s + r)$ (\path{shifted} in \path{Lean/SPR/N4/Hurwitz.lean}) gives the shifted coefficients \begin{equation}\label{eq:shifted-coeffs} \begin{aligned} a_{r,1} &= a_1 + 4r, & a_{r,2} &= a_2 + 3a_1 r + 6r^2, \\ a_{r,3} &= a_3 + 2a_2 r + 3a_1 r^2 + 4r^3, & a_{r,4} &= a_4 + a_3 r + a_2 r^2 + a_1 r^3 + r^4. \end{aligned} \end{equation} Substituting~\eqref{eq:shifted-coeffs} into $\Delta_3(a_r) = a_{r,1}a_{r,2}a_{r,3} - a_{r,3}^2 - a_{r,1}^2 a_{r,4}$ and collecting powers of $r$ yields the degree-six polynomial $H(r)$ (\path{determinantPolynomial}): \begin{equation}\label{eq:det-poly-full} \begin{aligned} H(r) ={}& 64r^6 + 96a_1 r^5 + (48a_1^2 + 32a_2)r^4 + (8a_1^3 + 32a_1 a_2)r^3 \\ & + (4a_2^2 + 8a_1^2 a_2 + 4a_1 a_3 - 16a_4)r^2 + (2a_1 a_2^2 + 2a_1^2 a_3 - 8a_1 a_4)r + \Delta_3(a). \end{aligned} \end{equation} In Lemma~\ref{lem:hurwitz-det}, if a monic quartic $p(s) = s^4 + p_1 s^3 + p_2 s^2 + p_3 s + p_4$ satisfies $p_1 > 0$, $p_3 > 0$, and $\Delta_3(p) = p_1 p_2 p_3 - p_3^2 - p_1^2 p_4 = 0$, then at $\omega = \sqrt{p_3/p_1} > 0$ ($\omega^2 = p_3/p_1$) its odd part vanishes, $O_p(\omega^2) = p_3 - p_1(p_3/p_1) = 0$, and its even part is \[ E_p(\omega^2) = \left(\frac{p_3}{p_1}\right)^2 - p_2\left(\frac{p_3}{p_1}\right) + p_4 = -\frac{p_1 p_2 p_3 - p_3^2 - p_1^2 p_4}{p_1^2} = -\frac{\Delta_3(p)}{p_1^2} = 0. \] Hence $p(i\omega) = E_p(\omega^2) + i\omega O_p(\omega^2) = 0$ (\path{determinant_zero_root}). Applying this to $p = a_r$ ($r \ge 0$) gives $a(r + i\omega_r) = a_r(i\omega_r) = 0$. \subsection{Derivation of the Piecewise Square-Plus-Linear Bounds (Lemma~\ref{lem:square-bounds})}\label{app:piecewise} \begin{proof}[Proof of Lemma~\ref{lem:square-bounds}] For any $a \in K$, we have $l \le a_1 \le u$, $A \le a_2$, $l_3 \le a_3 \le u_3$, and $a_4 \le C$. Since $x > 0$ (Lemma~\ref{lem:weights}) and $t \ge 0$, we have for all $t \ge 0$ \[ -x E_a(t) = -x(t^2 - a_2 t + a_4) \ge -x(t^2 - At + C) = -x(t - \alpha)(t - \beta). \] (1) When $0 \le t \le y$, we have $(t - y)t \le 0$ and $y - t \ge 0$, so $a_1(t - y)t \ge u(t - y)t$ and $a_3(y - t) \ge l_3(y - t)$. Substituting these into~\eqref{eq:residual} gives \[ \begin{aligned} F_a(t) &\ge u(t - y)t + l_3(y - t) - x(t - \alpha)(t - \beta) \\ &= u(t - \alpha)(t - y) + u\alpha(t - y) + l_3(y - t) - x(t - \alpha)(t - \beta) \\ &= (t - \alpha)\bigl[u(t - y) - x(t - \beta)\bigr] + (l_3 - u\alpha)(y - t). \end{aligned} \] By the first chord identity in~\eqref{eq:chord-lines}, $u y - x\beta = (u - x)\alpha$, so \[ u(t - y) - x(t - \beta) = (u - x)t - (uy - x\beta) = (u - x)(t - \alpha), \] which together with $\delta_- = l_3 - u\alpha$ yields~\eqref{eq:left-square} (\path{residual_lower_left}). (2) Symmetrically, when $t \ge y$, we have $(t - y)t \ge 0$ and $y - t \le 0$, so $a_1(t - y)t \ge l(t - y)t$ and $a_3(y - t) \ge u_3(y - t) = -u_3(t - y)$. Substituting these into~\eqref{eq:residual} and applying the second chord identity $l y - x\alpha = (l - x)\beta$ gives \[ \begin{aligned} F_a(t) &\ge l(t - y)t - u_3(t - y) - x(t - \alpha)(t - \beta) \\ &= (t - \beta)\bigl[l(t - y) - x(t - \alpha)\bigr] + (l\beta - u_3)(t - y) = (l - x)(t - \beta)^2 + \delta_+(t - y), \end{aligned} \] which establishes~\eqref{eq:right-square} (\path{residual_lower_right}). \end{proof} \bibliographystyle{plain} \bibliography{references} \end{document}