Fortuna's conjecture on the companion Lyapunov equation at the first open cell: an exact verification at a degree-five companion matrix with a complex-conjugate pair

Abstract

Let a(s)=sⁿ+aₙ₋₁sⁿ⁻¹+…+a₀ be a Hurwitz polynomial, A its companion matrix and X the solution of the Lyapunov equation XA+A^(T) X=-Q with Q=Q^(T)succeq 0. Fortuna's conjecture, as stated by Ferrante (arXiv:2606.16492), asserts that X is entrywise nonnegative. Ferrante proves it when A has only real eigenvalues, records that the cases n ≤ 4 can be settled by brute force and that the diagonal and the two corner entries are always nonnegative, and names the removal of the real-root assumption as the main open question. We give an exact verification in a cell outside those bounds: at the companion matrix of (s+1)³(s²+s+1)=s⁵+4s⁴+7s³+7s²+4s+1, whose spectrum contains exp(± 2π i/3) and which is not diagonalizable, the solution for every rank-one Q=qq^(T) is entrywise nonnegative, each of its fifteen distinct entries being written as an explicit sum of squares in q with rational coefficients; the solution is also shown to be unique among symmetric matrices by an explicit inversion of the Lyapunov operator over ℚ. Two identities valid for every degree and every spectrum are recorded: 2a₀X_(1,n)=Q₁₁, which turns Ferrante's corner remark into a value, and X_(k,k-1)=aₖ₋₁X_(k,n)-Qₖₖ/2. Controls show that the companion form and the Hurwitz hypothesis are both needed and that the conclusion is strictly stronger than Xsucceq 0. Recomputing Ferrante's counterexample to total nonnegativity exactly over ℚ, we find that the minor he names, the leading 2 × 2 principal minor, is positive (+4355916893/28812000), as it must be when Xsucceq 0, and that the negative minor is the non-principal one on rows {1,2} and columns {2,3}, equal to -51562093/72030. Outside the formal development we report a floating-point-free search (57,678 rational instances at n=5, no counterexample), a symbolic verification along the one-parameter family (s+1)³(s²+ps+1), p>0, and the identification, for n ≤ 5, of the inverse of the matrix of the quadratic form Xₙₙ with the Hermite matrix of a, whose (n,n) entry is 2aₙ₋₁; this yields X_(n,n-1) ≥ 0 for every Hurwitz a of degree at most 5. Every pinned statement is verified in Lean 4 against Mathlib without compiled evaluation.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-09-07 03:53 UTC

   File fingerprint

   878e0af82fc8d7380979c5237363d9732831550280cc070d91ac4ce6664c02a6