TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A CARE residual and Lyapunov margin certify a unique stabilizing root in a matrix ball

Statement

Let $\hat{X} = {\hat{X}}^{*}$ be a CARE candidate, ${\hat{A}}_{c} = A - G \hat{X}$ , and $L (E) = {\hat{A}}_{c}^{*} E + E {\hat{A}}_{c}, F_{c} (X) = A^{*} X + X A - X G X + Q .$ Assume ${\hat{A}}_{c}$ is certified Hurwitz, $L$ is invertible on Hermitian matrices, and outward-verified bounds satisfy $κ \geq ∥ L^{- 1} ∥_{F \to F}, r \geq ∥ F_{c} (\hat{X}) ∥_{F}, g \geq ∥ G ∥_{2},$ with $ρ > 0$ such that $κ (r + g ρ^{2}) \leq ρ, 2 κ g ρ < 1.$ Then there is exactly one Hermitian CARE root in the closed Frobenius ball $∥ X - \hat{X} ∥_{F} \leq ρ$ .

If also a verified Hermitian $W ≻ 0$ and $γ > 0$ satisfy $- ({\hat{A}}_{c}^{*} W + W {\hat{A}}_{c}) ⪰ γ I, 2 ∥ W ∥_{2} g ρ < γ,$ then that root is Hurwitz-stabilizing. Under the standard CARE hypotheses of Stabilizability and detectability give the unique stabilizing positive-semidefinite CARE solution, it is the unique stabilizing positive-semidefinite solution.

Facts & Assumptions

Given: The CARE data and matrix norms of Standard CARE and DARE data, equations, and conventions, a Hermitian candidate, and the outward-verified constants in the Statement.

[F1]

Standard CARE and DARE data, equations, and conventions: $F_{c} (X) = A^{*} X + X A - X G X + Q$ and $A_{c} (X) = A - G X$ .

[F2]

A Sylvester equation is uniquely solvable exactly when the spectra are disjoint: $E \mapsto {\hat{A}}_{c}^{*} E + E {\hat{A}}_{c}$ is invertible when $σ ({\hat{A}}_{c}^{*}) \cap (- σ ({\hat{A}}_{c})) = \emptyset$ ; this holds for Hurwitz ${\hat{A}}_{c}$ .

[F3]

Verified point and uniform linear residual certificate data: verified certificate data are mathematical upper bounds; the definition does not claim how a computation establishes them.

[F4]

Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: a finite outward-rounded expression DAG encloses every exact node value.

[F5]

Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison: the operator norm is bounded by the Frobenius norm and $∥ A X B ∥_{F} \leq ∥ A ∥_{2} ∥ X ∥_{F} ∥ B ∥_{2}$ .

[F6]

The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2: operator norms are submultiplicative.

[F7]

Stabilizability and detectability give the unique stabilizing positive-semidefinite CARE solution: under continuous stabilizability and detectability the stabilizing Hermitian positive-semidefinite CARE solution is unique.

[F8]

The Hurwitz Lyapunov integral is the unique solution and has the stated positivity: for Hurwitz $A_{c}$ , the solution of $A_{c}^{*} Y + Y A_{c} = - S$ is the convergent integral $Y = \int_{0}^{\infty} e^{t A_{c}^{*}} S e^{t A_{c}} d t$ , and is positive semidefinite when $S ⪰ 0$ .

[F9]

Every finite-dimensional normed space is Banach: every finite-dimensional normed space is complete, so a Cauchy sequence in the Hermitian matrix ball converges there.

[A1]

The numerical constants $κ, r, g, γ$ and $∥ W ∥_{2}$ are supplied as rigorous upper or lower bounds by the verifier; without valid enclosures this theorem gives no certificate.

Proof

1.1F1F2givenalgebra

For Hermitian $E$ , direct expansion gives $F_{c} (\hat{X} + E) = F_{c} (\hat{X}) + L (E) - E G E .$ Thus the root equation is equivalent to $E = T (E) : = - L^{- 1} F_{c} (\hat{X}) + L^{- 1} (E G E) .$

2.1A1F3F4F5F9step 1.1algebra

By [F5], $∥ E G E ∥_{F} \leq g ∥ E ∥_{F}^{2}$ . The assumptions give $∥ T (E) ∥_{F} \leq κ (r + g ρ^{2}) \leq ρ$ on the closed ball. Also $E G E - F G F = (E - F) G E + F G (E - F),$ so [F5] gives $∥ T (E) - T (F) ∥_{F} \leq 2 κ g ρ ∥ E - F ∥_{F}$ there. The Hermitian matrices form a closed finite-dimensional normed space, complete by [F9]. Iterating $T$ from zero gives successive differences bounded by a geometric sequence of ratio $2 κ g ρ < 1$ , hence a Cauchy sequence. Its limit lies in the closed ball and is a fixed point by continuity. Any two fixed points have distance at most that ratio times their distance, so they coincide.

3.1A1F1F2F6F7F8step 2.1algebra∎

Let $X = \hat{X} + E$ be this root. Its closed loop is $A_{c} (X) = {\hat{A}}_{c} - G E$ . Expanding, $A_{c} (X)^{*} W + W A_{c} (X) = {\hat{A}}_{c}^{*} W + W {\hat{A}}_{c} - E G W - W G E .$ By [F6] and [A1], $∥ E G W + W G E ∥_{2} \leq 2 ∥ W ∥_{2} g ρ < γ$ . Hence the left side is negative definite. For any eigenpair $A_{c} (X) v = λ v$ , $v \neq 0$ , this gives $2 Re (λ) v^{*} W v < 0$ ; since $W ≻ 0$ , $Re λ < 0$ . Thus the root is stabilizing. Its CARE identity also gives $A_{c} (X)^{*} X + X A_{c} (X) = - (Q + X G X) .$ Here $Q + X G X ⪰ 0$ because $Q, G ⪰ 0$ . Since $A_{c} (X)$ is Hurwitz, [F8] says the unique Lyapunov solution is its positive-semidefinite integral; uniqueness from [F2] identifies that solution with $X$ . Thus $X ⪰ 0$ , and [F7] identifies it with the unique stabilizing positive-semidefinite solution.

Depends on

Used by

Dependency tree · two levels

53 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Daniel Liberzon, Calculus of Variations and Optimal Control Theory: A Concise Introduction, Chapter 6 (standard reference, not scraped)
Peter Benner and Lihong Feng, Model Reduction for Dynamical Systems, Lecture 8 (standard reference, not scraped)