lyapunov_stability() does not verify P positive definite or Q positive semidefinite

[mzargham]

Summary

lyapunov_stability() in symproof/library/control.py (lines 175–237) only verifies the Lyapunov equation residual but does not check the definiteness conditions its docstring requires.

Problem

The docstring (line 198) states the theorem requires P positive definite and Q positive semidefinite. The implementation only verifies that every entry of A^T P + P A + Q equals zero. It does not verify:

• P ≻ 0 (positive definite)
• Q ⪰ 0 (positive semidefinite)

Without these checks, the sealed bundle certifies that a matrix equation holds but not the stability conclusion the docstring claims.

lyapunov_from_system() (lines 500–612) partially addresses this by checking P positive definite via Sylvester's criterion (lines 593–609), which is correct there since it uses Q.positive (strict). However, it still does not verify Q ⪰ 0.

Suggested fix

• Add leading principal minor checks for P ≻ 0 (Sylvester, strict positivity) to lyapunov_stability()
• Add principal minor checks for Q ⪰ 0 to both functions (or document the omission as an explicit limitation)

Files

• symproof/library/control.py:175-237 — lyapunov_stability()
• symproof/library/control.py:500-612 — lyapunov_from_system()