PropositionStatement: 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.

An invertible graph block converts an exact stable Schur or QZ basis into a Riccati solution

Statement

For the CARE case, suppose the exact Hamiltonian stable invariant subspace has a basis $U = [\begin{array}{c} U_{1} \\ U_{2} \end{array}]$ with $U_{1}$ invertible, and set $X = U_{2} U_{1}^{- 1}$ . If $X = X^{*}$ , then $X$ solves the CARE and the restriction matrix on the graph is $A - G X$ .

For the DARE case, suppose an exact stable deflating basis for the pencil $(N, M)$ is $U = [\begin{array}{c} U_{1} \\ U_{2} \end{array}]$ with $U_{1}$ invertible, and set $X = U_{2} U_{1}^{- 1}$ . If $X = X^{*}$ and $R + B^{*} X B ≻ 0$ , then $X$ solves the DARE and the restriction matrix is $A_{c} = (I + G X)^{- 1} A = A - B (R + B^{*} X B)^{- 1} B^{*} X A$ .

Facts & Assumptions

Given: The CARE or DARE definitions and exact invariant or deflating subspace equations.

[F1]

The stabilizing CARE solution is the Hamiltonian stable invariant graph: the CARE graph equation is $H [I; X] = [I; X] (A - G X)$ and its lower block is equivalent to the CARE.

[F2]

The stabilizing DARE solution is the stable deflating graph of a regular symplectic pencil: the DARE graph equation is $N [I; X] = M [I; X] A_{c}$ for $A_{c} = (I + G X)^{- 1} A$ .

[F3]

Standard CARE and DARE data, equations, and conventions: the DARE is equivalently $X = Q + A^{*} X (I + G X)^{- 1} A$ whenever $R + B^{*} X B$ is invertible.

Proof

1.1F1givenalgebra

In either case, $U_{2} = X U_{1}$ , so $U = [I; X] U_{1}$ . If $H U = U T$ in the CARE case, right multiplication by $U_{1}^{- 1}$ gives $H [I; X] = [I; X] (U_{1} T U_{1}^{- 1})$ . The top block fixes the restriction matrix as $A - G X$ ; the bottom block reads $- Q - A^{*} X = X (A - G X)$ , which is exactly $A^{*} X + X A - X G X + Q = 0$ .

2.1F2F3algebra∎

If $N U = M U T$ in the DARE case, the same normalization gives $N [I; X] = M [I; X] (U_{1} T U_{1}^{- 1})$ . The top block is $A = (I + G X) (U_{1} T U_{1}^{- 1})$ , so invertibility of $I + G X$ gives restriction matrix $(I + G X)^{- 1} A$ . The lower block is $X - Q = A^{*} X (I + G X)^{- 1} A$ , which is the DARE by [F3]. No claim survives an unverified leading-block inverse or a subsequent nonzero symmetry residual.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

Federico Poloni, Lecture notes on Riccati-type matrix equations (standard reference, not scraped)
A.A. Stoorvogel and A. Saberi, The discrete algebraic Riccati equation and linear matrix inequality, Memorandum COSOR 94-16 (standard reference, not scraped)