Alphabeta Math
Pipeline-generated
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.

✓ 21 results · all verified · 12 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 9 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Numerical algebraic Riccati equations and stabilizing branches

1 · Prerequisites

2 · Summary

Objective

This page fixes the real and complex CARE/DARE conventions, proves the closed-region PBH equivalences and stabilizing value solutions, and relates those solutions to Hamiltonian and symplectic-pencil stable graphs. It records finite-budget Schur/QZ candidate extraction with an exact finite stable-block reordering routine, local residual-and-margin certificates, exact and safeguarded Newton-Kleinman iteration, and discrete structure-preserving doubling. All numerical branches require actual Riccati residuals, symmetry checks, DARE positive-definiteness checks, and separate closed-loop stability evidence.

The underlying algebra permits singular A and uses homogeneous pencil coordinates, so infinite generalized eigenvalues are retained without forming A−1. A small residual alone does not identify the stabilizing branch. Unstructured Schur/QZ backward error is not interpreted as a nearby structured Hamiltonian or symplectic pencil.

Conventions and proof map

The state, input, and output matrices have sizes A∈Fn×n, B∈Fn×m, C∈Fp×n over F∈{R,C}; Q=C∗C⪰0, R=R∗≻0, and G=BR−1B∗. The CARE is A∗X+XA−XGX+Q=0. The DARE is X=Q+A∗XA−A∗XB(R+B∗XB)−1B∗XA. The feedback and closed-loop conventions are fixed in Standard CARE and DARE data, equations, and conventions.

The CARE proof constructs finite-horizon value matrices, passes to a positive-semidefinite limit, proves transversality using detectability, and establishes uniqueness. The DARE proof uses finite-horizon dynamic programming and a detectability convolution estimate; it never requires A−1. The Hamiltonian and homogeneous-pencil graph identities follow by block multiplication after the value theorems. Candidate extraction runs the finite stable-block reordering procedure after the Schur/QZ reduction; boundary, separation, swap-budget, work-budget, and graph-conditioning failures remain explicit statuses.

Numerical scope and limits

CARE and DARE local residual balls use their own derivative operators, inverse bounds, and separate stability margins. DARE stable-deflating-subspace sensitivity uses generalized Sylvester separation, paired-graph contraction, leading and reciprocal-trailing Stein margins, and a normalized graph-chart estimate. Exact Newton-Kleinman convergence is conditional on a supplied stabilizing initial feedback and exact Lyapunov solves. Inexact updates are accepted only after distinct residual, descent, and stability checks. SDA is an exact-arithmetic structure theorem; finite precision reports symmetry defects and recomputes the DARE residual and positivity evidence after any symmetrization.

Stable-block reordering acts exactly on the returned computed Schur/QZ arrays and preserves any existing unstructured reduction residual. An ordered return certifies the selected subspace of that represented form; Riccati acceptance still requires equation-level residual, symmetry, positivity where applicable, and closed-loop stability certificates. QZ backward error alone does not imply structured pencil or DARE subspace accuracy.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Stabilizability and detectability for continuous and discrete linear systems

Definition

Let F∈{R,C}, n,m,p≥1, A∈Fn×n, B∈Fn×m, and C∈Fp×n. A matrix is Hurwitz when every complex eigenvalue has strictly negative real part, as in Hurwitz matrices and the continuous Lyapunov equation. It is Schur stable when every complex eigenvalue has modulus strictly less than one.

The pair (A,B) is continuously stabilizable if some K∈Fm×n makes A−BK Hurwitz. The pair (A,C) is continuously detectable if some L∈Fn×p makes A−LC Hurwitz.

The pair (A,B) is discretely stabilizable if some K∈Fm×n makes A−BK Schur stable. The pair (A,C) is discretely detectable if some L∈Fn×p makes A−LC Schur stable. These are exact existential properties of the given finite matrices. A residual size or an approximate spectral estimate does not itself establish any of them.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Reachable block decomposition and same-field state-feedback pole placement

Statement

Let F∈{R,C}, let n,m≥0, and let A∈Fn×n and B∈Fn×m. The real case is viewed over C when a complex spectral parameter or rank is used. Define R=span⁡F{AjBeℓ:0≤j<n, 1≤ℓ≤m},r=dim⁡FR, where a span of an empty family is {0}. Then there is an invertible P∈Fn×n such that P−1AP=[ArD0Au],P−1B=[Br0]. The pair (Ar,Br) is reachable on Fr in the displayed algebraic sense, and empty blocks are permitted. For every λ∈C, rank⁡C[λI−A  B]=n⟺λ∉σC(AuC), where AuC is the complexification of Au when F=R and is Au itself when F=C.

If r=n, then for every prescribed list μ1,…,μn∈F there is a gain K∈Fm×n satisfying det⁡(zI−A+BK)=∏j=1n(z−μj). Thus a real reachable pair can be assigned any real pole list, including repetitions, and a complex reachable pair any complex list. The pole-placement claim does not assert arbitrary nonreal conjugate-pair placement for a real pair.

Facts & Assumptions

Given: Finite matrices A,B over F, with the reachable space and rank convention stated above.

[F2]

Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T: for a map with finite-dimensional domain, dimension equals rank plus nullity.

[F3]

Row rank equals column rank, and both equal the number of pivots: every finite matrix over a field has equal row rank and column rank.

[F4]

The characteristic polynomial of a block upper- or lower-triangular matrix is the product of the characteristic polynomials of its diagonal blocks: the characteristic polynomial of a block-triangular matrix is the product of those of its diagonal blocks.

Proof

1.1givenF1algebra

For each integer k≥0, put Rk=span⁡{AjBeℓ:0≤j<k, 1≤ℓ≤m}. Then Rk+1=Rk+ARk+im⁡B. If Rk+1=Rk, then im⁡B⊆Rk and ARk⊆Rk, so every later space equals Rk. Otherwise each inclusion is strict; if no equality occurs before Rn, its dimension has increased at least n times from zero, hence Rn=Fn. Therefore R=Rn is the smallest A-invariant subspace containing im⁡B.

1.2F2F3algebra

Let (E,H) be reachable on Fd. If [λI−E  H] had rank less than d over C, row-rank equality and rank-nullity applied to its adjoint would give a nonzero y∈Cd with y∗(λI−E)=0 and y∗H=0. Induction then gives y∗EjH=λjy∗H=0 for every j<d, contradicting reachability; for real data the real reachable columns complexify to span Cd. Thus the horizontal rank is d for every complex λ.

2.1givenF1step 1.1constructalgebra

Scan the finite columns of B,AB,…,An−1B, retaining a column exactly when it is outside the span of those retained; then scan the standard coordinate vectors until the retained list is a basis of Fn. This gives a basis matrix P whose first r columns span R. Invariance and im⁡B⊆R give P−1AP=[ArD0Au] and P−1B=[Br0]; the first r coordinates of the columns AjB are ArjBr and span Fr. Applying the stabilization argument of step 1.1 in dimension r shows that the first r powers already span Fr, so (Ar,Br) is reachable, including r=0. For real data, complexifying the real span gives the complex span because each complex coefficient splits into real and imaginary parts. No arbitrary basis choice is used.

2.2givenstep 1.1algebra

For any gain J, a subspace W contains im⁡H and is E-invariant exactly when it contains im⁡H and is (E−HJ)-invariant: HJW⊆im⁡H⊆W, and the converse follows from E=(E−HJ)+HJ. By step 1.1 the smallest invariant subspace containing im⁡H, hence reachability, is feedback-invariant.

3.1F5step 2.1step 1.2algebra

In the block coordinates of step 2.1, [λI−A  B] has block form [λI−Ar−DBr0λI−Au0]. A left annihilator (a,b) must satisfy a[λI−Ar  Br]=0, so step 1.2 forces a=0; a nonzero remaining annihilator exists exactly when det⁡(λI−AuC)=0, which by [F5] is exactly λ∈σC(AuC). Invertible coordinate changes preserve rank, proving the claimed equivalence in the original coordinates.

3.2F2step 1.2step 2.2choosealgebra

Prove pole placement by induction on d. For d=0 the empty gain gives determinant 1. For d>0, reachability implies rank⁡H>0. Fix μ1∈F. By step 1.2, [E−μ1I  −H] has full row rank over C; for real data a nonzero full-size minor has real nonzero determinant, so it also has full row rank over F. Its kernel has dimension m by [F2], whereas kernel vectors with first component zero have dimension m−rank⁡H<m. Choose a kernel vector (v,u) with v≠0; it satisfies (E−μ1I)v=Hu. Choose vi≠0 and define J0x=uxi/vi, so (E−HJ0)v=μ1v.

4.1F4step 1.1step 2.2step 3.2inductionalgebra∎

Let π:Fd→Fd/Fv be the quotient map, Eˉ0π=π(E−HJ0), and Hˉ=πH. The quotient pair is reachable because the spanning columns of (E−HJ0,H) project onto the quotient by step 2.2; the stabilization argument of step 1.1 in dimension d−1 shows that its first d−1 powers suffice. To obtain quotient coordinates over F, begin with v and append standard coordinate vectors whenever they increase its span; the resulting finite basis has d−1 remaining vectors whose cosets form a basis of Fd/Fv. Thus the induction applies over the original field, also when d=1 and the quotient is zero. By induction a quotient gain Jˉ places μ2,…,μd; lift it as J1=Jˉπ and set J=J0+J1. Since J1v=0, the closed loop retains eigenvalue μ1 on Fv and induces the assigned quotient characteristic polynomial. The block-triangular characteristic identity [F4] gives det⁡(zI−E+HJ)=∏j=1d(z−μj), including repeated poles and poles already in σ(E); no inverse of E or E−μI is used.

AlgorithmAlgorithm: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

Finite-budget stable block reordering for Schur and QZ forms

Definition

Inputs are an order d≥0 real or complex Schur matrix T, or a regular real or complex generalized Schur pair (S,T), with the declared diagonal block partition. Complex Schur and QZ forms have scalar blocks; real Schur forms have scalar blocks or real 2×2 blocks; real generalized Schur forms have real 1×1 or 2×2 blocks. Each generalized diagonal block pair must be regular. Optional accumulated factors are exact unitary/orthogonal products; if omitted they are identity. Other inputs are a CARE selector (strict left half-plane) or DARE selector (strict unit disk), a required integer selected dimension 0≤r≤d, nonnegative integer budgets K and W, a positive local separation threshold η, and either an exact arithmetic controller or a bounded outward evaluator.

Use the CARE selector with an ordinary Schur form and the DARE selector with a generalized Schur form; an unmatched form-selector combination returns invalid-form.

Before any charged operation, initialize attempts, accepted swaps and primitive/evaluator counts to zero, diagnostic lists to empty, and every uncomputed diagnostic to unavailable. In particular, the actual selected dimension, block labels, boundary and separation predicates, and initial inversion count remain unavailable until their respective scans or tests finish; the requested dimension r is always retained separately. Report only completed tests and certificates, together with the last committed arrays and factors, on an early exit. Unavailable predicates assert neither truth nor falsity.

The entries of the input arrays are treated as their exact represented real or complex values. All local transformed arrays and accumulated factors are retained exactly as finite products; a rounded dense copy is only a separately evaluated diagnostic. Before each scalar primitive or outward evaluation, return work-budget-exhausted if no units of W remain; otherwise consume one unit before requesting the operation. Charge validation, label and inversion-count scans, local construction, and the final ordering scan to this same budget. For rational or dyadic arrays, the exact core uses rational arithmetic and positive square roots, with exact real-algebraic sign comparisons where needed. Exact decisions on arbitrary real inputs are an exact-real arithmetic model, not a bit-computability claim. The bounded-evaluator branch returns arithmetic-inconclusive whenever a needed zero, sign, division, or normalization remains unresolved.

  1. Validate dimensions, the declared block pattern, and regularity of each generalized diagonal pair in one finite scan. For ordinary scalar blocks over either field classify tii by Re⁡tii<0 or >0 for CARE; for real 2×2 blocks first verify negative discriminant and then classify by trace less than or greater than zero. For generalized scalar blocks over either field [sii:tii], verify the pair is nonzero and classify by ∣sii∣<∣tii∣ or ∣sii∣>∣tii∣ for DARE; thus tii=0, sii≠0 is complementary and represents infinity without division. For a real generalized 2×2 block, verify det⁡(Tb)≠0 and that det⁡(Sb−λTb) has negative discriminant; its conjugate roots have common squared modulus det⁡(Sb)/det⁡(Tb), so classify by strict comparison of this ratio with one, cross-multiplying with the certified sign of det⁡(Tb). Exact equality with the selected boundary returns boundary-spectrum. A bounded enclosure touching the boundary returns separation-inconclusive. Require that the selected block sizes sum to r, or return dimension-mismatch. Invalid patterns or singular local homogeneous pairs return invalid-form. Compute the initial inversion count once by scanning all ordered block pairs after classification.

  2. Give every whole block its selected or complementary label. Locate the leftmost adjacent complementary-selected inversion. If none exists, return ordered with the current exact arrays and accumulated factors. If an inversion exists but K swap attempts have already been made, return swap-budget-exhausted. Otherwise consume one attempt before starting its local construction. Never split a real conjugate pair.

  3. Let p,q∈{1,2} be the two adjacent block sizes (over C, p=q=1), with local blocks TJJ=[AC0B] for ordinary Schur form, or SJJ=[AC0B],TJJ=[DF0E] for QZ form. With column-vectorization, form the local coefficient system H=Iq⊗A−BT⊗Ip,h=−vec⁡(C) for ordinary Schur, with unknown vec⁡(R), and H=[Iq⊗A−BT⊗IpIq⊗D−ET⊗Ip],h=−[vec⁡(C)vec⁡(F)] for QZ, with unknown [vec⁡(R);vec⁡(L)]. The transpose in BT and ET is intentional, also over C. Solve Hx=h and HY=I by finite Gaussian elimination with complete pivoting: at each stage scan the finite remaining submatrix, choose an entry of largest certified modulus with lexicographic ties, swap rows and columns, eliminate, and back-substitute while undoing column permutations. An exact all-zero remaining submatrix returns swap-singular. An unresolved pivot or range failure returns separation-inconclusive or range-failure. Verify Hx=h and HY=I exactly, or verify a usable approximate-inverse certificate ∥I−YH∥2≤θ<1 and still solve Hx=h exactly. In the latter case it gives ∥H−1∥2≤∥Y∥2/(1−θ). In the exact-inverse branch take β=∥Y∥F in exact arithmetic, or an outward upper bound for that norm; in the approximate-inverse branch take an outward bound for ∥Y∥2/(1−θ). Require ηβ≤1; otherwise return swap-separation-inconclusive. Record the threshold, solves, pivot decisions and certificate.

  4. For ordinary Schur form set V=[R;Iq]. For QZ set V=[R;Iq] and WL=[L;Iq]. Complete the columns of V, and separately WL, to exact orthonormal bases by Gram–Schmidt: process the graph columns first, then e1,…,ep+q, skipping exactly zero residuals and normalizing each nonzero residual by the positive square root of its squared norm. The graph columns are independent because their last q rows form Iq; the coordinate scan completes a basis. An unresolved zero or normalization decision in bounded mode returns arithmetic-inconclusive.

  5. Let Zloc be the ordinary orthogonal/unitary completion; for QZ let Zloc be the right completion and Qloc the left completion. Propose the local transform Zloc∗TZloc in the ordinary case, or Qloc∗SZloc and Qloc∗TZloc in the QZ case. Apply it to the entire affected row and column panels, including upper off-diagonal blocks. The lower-left block is set to exact zero only by the local equations solved in step 3. For a real QZ form, factor each newly formed real 2×2 diagonal block as Tb=LbRb by Gram–Schmidt on its two columns, apply the embedded Lb∗ to the corresponding rows of both arrays, and update Qloc←QlocLb with the same embedded factor; such a block is nonsingular because its roots are finite and nonreal. A size-one infinite pair requires no division by its zero second coordinate. Commit the provisional panels and factor updates only after every required local operation succeeds, incrementing accepted swaps by one as part of that same commit; otherwise return the previous committed arrays with a failed-attempt diagnostic and leave accepted swaps unchanged.

  6. After a committed exchange, swap the two labels and sizes and return to step 2. Ordinary accumulated factors are updated by right multiplication with Zloc; generalized accumulated factors are updated as Q←QQloc and Z←ZZloc. The first r columns of the updated factor are reported as the selected basis candidate; in QZ the right factor Z, not the left factor Q, supplies the right deflating basis.

On every exit return the current partial form, exact product factors, status, selected dimension, boundary and separation predicates, initial inversion count, attempts, accepted swaps, primitive/evaluator counts, original residual certificates, local inverse-norm certificates, and any residual transport data. Other statuses are work-budget-exhausted, arithmetic-inconclusive, range-failure, invalid-form, dimension-mismatch, boundary-spectrum, separation-inconclusive, swap-singular, swap-separation-inconclusive, and swap-budget-exhausted. ordered is distinct from any Riccati acceptance status. Reordering a computed form does not assert a structured Hamiltonian or symplectic backward-error theorem.

Facts & Assumptions

Given: The exact represented Schur or generalized Schur input, its block partition, selector, required dimension, two finite budgets and the declared exact controller or bounded evaluator.

[F1]

Real and complex Schur forms: a complex Schur form is upper triangular; a real Schur form is block upper triangular with 1×1 blocks and real 2×2 blocks of negative discriminant.

[F2]

Complex and real generalized Schur forms: complex generalized Schur factors are unitary with upper-triangular arrays and nonzero diagonal homogeneous pairs; the real form retains whole 1×1 and 2×2 diagonal blocks.

[F3]

Verified point and uniform linear residual certificate data: a uniform approximate-inverse/residual certificate is usable only under its stated strict norm bound.

[F4]

A uniform approximate inverse and residual enclose every linear solution: usable certificate data bound every exact solution; unavailable or unusable data do not assert a finite enclosure.

[F5]

Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: a finite outward evaluator enclosure contains the exact value, while non-finite statuses make no finite claim.

[F6]

Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans: finite independent vectors yield an orthonormal list with the same successive spans.

[F7]

A Neumann defect bounds the inverse norm: if ∥E∥2≤θ<1, then I−E is invertible and its inverse norm is at most (1−θ)−1.

[F8]

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

[F9]

Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T: an injective or surjective endomorphism of a finite-dimensional space is bijective.

Proof

1.1givenF1F2F5algebra

The validation scan and each selector test examine finitely many matrix entries or declared blocks. The listed Schur forms and homogeneous block conventions are exactly [F1] and [F2]; every sign decision either has an exact result or a finite outward enclosure by [F5]. Invalid structure, boundary equality, an unresolved enclosure, or a dimension mismatch takes its declared return branch before a swap is committed.

1.2F3F4F5F7F8F9givenalgebra

At each local attempt p,q≤2, so the coefficient matrix has order at most eight and the pivot search is finite. Complete pivoting uses invertible row and column permutations; each elimination subtracts a pivot-row multiple and is reversed by adding it back. Exact back-substitution therefore solves the recorded system or detects an exact zero remaining block. If ∥I−YH∥2≤θ<1, [F7] makes YH invertible; (YH)−1Y is a left inverse of square H, so [F9] makes H invertible and [F8] gives ∥H−1∥2≤∥Y∥2/(1−θ). The routine still verifies Hx=h exactly. An unavailable solve, comparison, or bound takes its explicit failure status.

2.1F6step 1.1algebra

The last q rows of each graph matrix [R;Iq] and [L;Iq] form Iq, so both have independent columns. By [F6], Gram–Schmidt gives orthonormal graph columns with the same span. If the current span is proper, some standard coordinate vector lies outside it because those vectors span Fp+q; the finite scan therefore completes a basis.

3.1givenstep 1.1step 1.2step 2.1algebra∎

All remaining loops are finite scans of blocks, rows, columns, pivots, or the bounded standard basis. Every arithmetic or evaluation request consumes one unit of W before execution, and every local attempt consumes one unit of K before construction. Each failure returns without committing provisional data. Thus the procedure returns a declared status after finitely many operations or reaches ordered after finitely many committed exchanges; no unresolved comparison is retried indefinitely.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Standard CARE and DARE data, equations, and conventions

Definition

Let F∈{R,C}, A∈Fn×n, B∈Fn×m, C∈Fp×n, and R=R∗∈Fm×m be positive definite. Write Q=C∗C and G=BR−1B∗. The inverse R−1 is well-defined: A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique supplies an invertible factor R=LL∗, so R−1=L−∗L−1. Thus v∗Gv=∥L−1B∗v∥22≥0 and v∗Qv=∥Cv∥22≥0. The symbol ∗ is transpose over R and conjugate transpose over C.

The continuous algebraic Riccati equation (CARE) is A∗X+XA−XGX+Q=0. Its residual is Fc(X)=A∗X+XA−XGX+Q, its feedback is Kc(X)=R−1B∗X, and its closed-loop matrix is Ac(X)=A−BKc(X)=A−GX.

For X=X∗⪰0, SX:=R+B∗XB is positive definite because v∗SXv=v∗Rv+(Bv)∗X(Bv)>0 for every nonzero v. The discrete algebraic Riccati equation (DARE) is X=Q+A∗XA−A∗XB(R+B∗XB)−1B∗XA. Its residual is Fd(X)=Q+A∗XA−A∗XB(R+B∗XB)−1B∗XA−X. Whenever X=X∗, the matrix R+B∗XB is positive definite if X⪰0. Its feedback and closed-loop matrix are Kd(X)=(R+B∗XB)−1B∗XA,Ac(X)=A−BKd(X). A CARE solution is stabilizing when it is Hermitian and Ac(X) is Hurwitz. A DARE solution is stabilizing when it is Hermitian, R+B∗XB≻0, and Ac(X) is Schur stable. No inverse of A is part of either definition.

For Hermitian X with SX invertible, multiplication gives (I+GX)−1=I−BSX−1B∗X,X(I+GX)−1=X−XBSX−1B∗X. In either product, the additional coefficient of B is R−1−SX−1−SX−1(B∗XB)R−1=0, because SX=R+B∗XB. Thus the DARE is equivalently X=Q+A∗X(I+GX)−1A, and its closed-loop matrix is Ac(X)=(I+GX)−1A.

The associated homogeneous symplectic pencil is N=[A0−QI],M=[IG0A∗],P(α,β)=βN−αM. The homogeneous-coordinate convention is that a finite eigenvalue λ is [α:β]=[λ:1] and [1:0] denotes infinity.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Powers of a Schur-stable matrix decay geometrically up to a polynomial factor

Statement

Let M∈Cn×n be Schur stable and let r satisfy ρ(M)<r<1. For the Euclidean induced operator norm there is a finite Cr such that ∥Mk∥2≤Crrk(k≥0). For a real matrix, interpret the same statement on its complexification.

Facts & Assumptions

Given: A finite Schur-stable matrix M and r with ρ(M)<r<1.

[A1]

For n≥1, the notation ρ(M) means max⁡{∣λ∣:λ∈σC(M)}; for the unique 0×0 matrix set ρ(M)=0.

[F1]

Stabilizability and detectability for continuous and discrete linear systems: Schur stable means every eigenvalue has modulus strictly less than one.

[F2]

If the characteristic polynomial of an endomorphism splits, some orthonormal basis makes its matrix upper triangular: a complex finite-dimensional endomorphism has an orthonormal basis in which its matrix is upper triangular.

[F3]

The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2: ∥ST∥2≤∥S∥2∥T∥2 for compatible finite-dimensional maps.

[F4]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: ∥T∥2=max⁡∥v∥2=1∥Tv∥2.

[F5]

Every nonconstant polynomial in C[x] splits into linear factors: every nonconstant characteristic polynomial over C splits over C, so the hypothesis of [F2] holds.

[F6]

Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces: a unitary operator and its adjoint preserve the Euclidean norm.

Proof

1.1A1F1F2F5F7F8construct

If n=0, the unique endomorphism and every power of it is the zero map on the zero domain; its operator norm is zero, so the assertion holds with Cr=0. Assume now n≥1 and regard a real matrix, if present, as a complex matrix. Its characteristic polynomial is a nonconstant complex polynomial, so [F5] and [F2] give M=UTU∗ with U unitary and T=D+N, where D is diagonal and N is strictly upper triangular. Similar matrices have the same eigenvalues: Mv=λv is equivalent to T(U∗v)=λ(U∗v). By [F7] and [F8], the eigenvalues are the diagonal entries of T; hence ρ(M)=max⁡i∣Tii∣=∥D∥2, where the last equality follows directly from the Euclidean induced norm. Set ρ=ρ(M)<r. Each occurrence of N in a product raises the row-to-column index, while D preserves it, so every word containing at least n copies of N is zero.

2.1F3F4F6step 1.1algebra

Expand (D+N)k as the sum of noncommuting words. The terms with exactly j copies of N number (kj), vanish for j≥n, and for j<n have norm at most ρk−j∥N∥2j by [F3] and ∥D∥2=ρ. Thus ∥Tk∥2≤∑j=0min⁡(k,n−1)(kj)ρk−j∥N∥2j. Because U and U∗ preserve vector norms by [F6] and U∗ maps the unit sphere onto itself, the induced norm [F4] gives ∥Mk∥2=∥UTkU∗∥2=∥Tk∥2.

3.1step 2.1algebracases∎

If ρ=0, then D=0 and T=N, so Tk=0 for k≥n; taking Cr=max⁡0≤k<n∥Tk∥2r−k proves the claim. If 0<ρ<r, each fixed j<n satisfies (kj)ρk−j∥N∥2j/rk≤cjkj(ρ/r)k for a finite cj. The ratio of consecutive terms kj(ρ/r)k tends to ρ/r<1, so this sequence is bounded. Summing its finitely many bounds over 0≤j<n gives a finite Cr in step 2.1.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Stabilizability and detectability imply the closed-region PBH rank tests

Statement

For F∈{R,C}, n,m,p≥1, A∈Fn×n, B∈Fn×m, and C∈Fp×n, the following necessary conditions hold.

If (A,B) is continuously stabilizable, then rank⁡[λI−A  B]=n for every λ∈C with Re⁡λ≥0. If it is discretely stabilizable, the same rank is n for every ∣λ∣≥1.

If (A,C) is continuously detectable, then rank⁡[λI−AC]=n for every Re⁡λ≥0. If it is discretely detectable, the same rank is n for every ∣λ∣≥1.

This proves the necessary half of the PBH tests. The converse pole-placement implication is not asserted here.

Facts & Assumptions

Given: The matrices and continuous/discrete stabilizability and detectability definitions of Stabilizability and detectability for continuous and discrete linear systems. Every rank test and eigenvector argument is over C; when F=R, the real matrices and their real feedback or injection witnesses act complex-linearly on their complexifications.

[F1]

Stabilizability and detectability for continuous and discrete linear systems: continuous stabilizability means A−BK is Hurwitz for some K; discrete stabilizability means A−BK is Schur stable; detectability is the dual condition with A−LC.

[F2]

Row rank equals column rank, and both equal the number of pivots: for a finite matrix, row rank and column rank agree.

[F3]

Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T: for a linear map with finite-dimensional domain, dimension of domain equals rank plus nullity.

[A1]

For F=R, real matrices and feedback/injection witnesses are extended complex-linearly when tested against a complex λ.

Proof

1.1A1F1F2F3contradiction

Suppose (A,B) is continuously stabilizable and fix its same-field feedback K from [F1]. If for some λ with Re⁡λ≥0 the horizontal matrix Hλ=[λI−A  B] has rank less than n, [F2] and [F3] applied over C to Hλ∗ give a nonzero y∈Cn with y∗(λI−A)=0 and y∗B=0. By [A1], the same real or complex K acts on this vector, so y∗(A−BK)=λy∗. Thus det⁡(λI−(A−BK))=0, contradicting that A−BK is Hurwitz.

1.2A1F1F3contradiction

Suppose (A,C) is continuously detectable and fix its same-field injection L from [F1]. If Vλ=[λI−AC] has rank less than n, rank-nullity over C gives a nonzero x∈Cn with (λI−A)x=0 and Cx=0. Hence (A−LC)x=λx, which contradicts that A−LC is Hurwitz because Re⁡λ≥0.

2.1A1F1F2F3step 1.1contradiction

Suppose (A,B) is discretely stabilizable and fix its same-field Schur feedback K from [F1]. If [λI−A  B] has rank less than n for some ∣λ∣≥1, the same complex left-kernel argument as in step 1.1 gives a nonzero y with y∗(A−BK)=λy∗. Thus det⁡(λI−(A−BK))=0, contradicting Schur stability.

3.1A1F1F3step 1.2contradiction∎

Suppose (A,C) is discretely detectable and fix its same-field Schur injection L from [F1]. If the vertical matrix has rank less than n for some ∣λ∣≥1, its complex kernel contains a nonzero x and Cx=0, so (A−LC)x=λx. This contradicts Schur stability.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Finite-budget stable block reordering has exact adjacent-swap correctness and status

Statement

For an order-d real or complex Schur form, or a regular generalized Schur form, run Finite-budget stable block reordering for Schur and QZ forms with its declared selector, selected dimension r, swap budget K, primitive/evaluator budget W, and positive local threshold η. Every execution returns after its finite scans or an explicit budget, boundary, form, separation, arithmetic, or range status. Every committed exact swap uses orthogonal/unitary transformations, preserves the appropriate Schur form over the original field, and exchanges exactly the two adjacent block spectra; for generalized Schur form it exchanges the homogeneous roots with multiplicity, including infinity.

Let b be the initial number of diagonal blocks and I the number of complementary-before-selected block pairs. If the initial selected block sizes sum to r, all selector comparisons are strict, every local construction and certificate succeeds, every inverse-norm threshold passes, K≥I, and W suffices for the entire execution, including validation, label and inversion scans, all I swaps, and the final ordering scan, the procedure returns ordered. The first r columns of the updated ordinary Schur factor then span the selected invariant subspace of the current computed form; the first r columns of the updated right QZ factor span the selected right deflating subspace of the current computed pencil. When an original reduction residual is present, this is the exact subspace of its represented nearby matrix or pencil, not automatically the original data's subspace. Each accepted swap decreases the inversion count by one and I≤b(b−1)/2. Boundary, small-gap, arithmetic, or budget exits do not prove that a stabilizing Riccati solution does not exist.

If the ordinary input relation is Q0∗AQ0=T0+R0 and the cumulative exact reordering factor is V, then Qnew=Q0V, Tnew=V∗T0V, and the new residual is V∗R0V, with unchanged Frobenius norm. If the generalized input relations are Q0∗AZ0=S0+RA and Q0∗BZ0=T0+RB, then for cumulative left and right factors U,V the new residuals are U∗RAV and U∗RBV, again with unchanged Frobenius norms. Thus exact reordering preserves the original unstructured reduction certificate but creates no structured Hamiltonian or symplectic error theorem.

For k local swap attempts, the scalar-core work is O(d2+kd) in the declared exact scalar/evaluator unit model: the initial structure scan costs O(d2) and each local system has order at most eight while whole-panel updates touch O(d) entries. On success k=I, so the worst-case swap core is O(d3). Exact algebraic bit cost, evaluator implementation cost beyond the declared units, and dense evaluation of product factors are separate. From L0 bounded-support input factors, directly evaluating the first r columns costs O(L0dr+Idr); a dense residual multiplication, if used, has its own actual O(d3) cost.

Facts & Assumptions

Given: The algorithm's admitted exact Schur or generalized Schur input, block partition, strict selector, selected dimension, finite budgets and local exact or bounded-evaluator certificates.

[F1]

Finite-budget stable block reordering for Schur and QZ forms: it forms the stated ordinary or generalized Sylvester systems, completes exact orthonormal bases, applies whole-panel transformations transactionally, and returns explicit finite statuses.

[F2]

A Sylvester equation is uniquely solvable exactly when the spectra are disjoint: X↦AX+XB is invertible exactly when σ(A)∩(−σ(B))=∅.

[F3]

A nonzero polynomial of degree n over an integral domain has at most n distinct roots: a nonzero polynomial of degree q over an integral domain has at most q distinct roots.

[F4]

A finite-dimensional linear operator over a field is invertible if and only if its determinant is nonzero: a finite-dimensional square operator is invertible exactly when its determinant is nonzero.

[F5]

Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T: an injective square map on a finite-dimensional space is invertible.

[F6]

Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans: Gram–Schmidt gives an orthonormal list with the same successive spans as a finite independent input list.

[F8]

The homogeneous determinant factors across a block upper triangular pencil: the homogeneous determinant of a block upper-triangular pencil is the product of the diagonal-block homogeneous determinants.

[F9]

Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison: unitary changes preserve the Frobenius norm and ∥M∥2≤∥M∥F.

[F10]

A Neumann defect bounds the inverse norm: if ∥E∥2≤θ<1, then ∥(I−E)−1∥2≤(1−θ)−1.

[F11]

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

Proof

1.1F1givenalgebra

For an ordinary complex scalar block the diagonal entry itself classifies the root, while a real 2×2 block with negative discriminant has conjugate roots with real part tr⁡(Tb)/2. For a generalized scalar pair [s:t], a finite root is s/t, so ∣s∣<∣t∣ is exactly the disk predicate and t=0, s≠0 is infinity and complementary. For a real generalized 2×2 pair with finite nonreal roots, the root product is det⁡(Sb)/det⁡(Tb)=∣λ∣2. Thus the procedure labels whole blocks exactly and detects equality at the selector boundary.

1.2F1F2givenalgebra

For ordinary adjacent diagonal blocks A,B, column-wise expansion gives vec⁡(AR−RB)=(Iq⊗A−BT⊗Ip)vec⁡R. The selected and complementary spectra are disjoint, so [F2] applied to X↦AX+X(−B) makes this square coefficient operator invertible, giving a unique local solve.

1.3F1F2F3F4F5givenconstructalgebra

For generalized adjacent pairs (A,D) and (B,E), their homogeneous root sets are disjoint and both pairs are regular. The polynomials det⁡(A−ζD) and det⁡(B−ζE) are nonzero of degrees at most p,q; among p+q+1 distinct real integers, [F3] gives a ζ for which A0=A−ζD and B0=B−ζE have nonzero determinants, hence are invertible by [F4]. Each homogeneous root [α:β] maps injectively to μ=β/(α−ζβ), an eigenvalue of DA0−1 because D−μA0=−(βA−αD)/(α−ζβ); this also maps infinity to zero, and maps the second pair to EB0−1, so the ordinary spectra remain disjoint. If AR−LB=0 and DR−LE=0, then A0R=LB0, hence R=A0−1LB0 and DA0−1L=LEB0−1; [F2] forces L=0, then R=0. The square generalized Sylvester system has zero kernel, so [F5] makes it invertible; for real blocks its real coefficient matrix has the same nonzero determinant as its complexification.

1.4F1F9givenalgebra

For ordinary input, Q0∗AQ0=T0+R0 and Qnew=Q0V imply Qnew∗AQnew=V∗T0V+V∗R0V. For QZ, substituting Qnew=Q0U and Znew=Z0V into the two input relations gives residuals U∗RAV and U∗RBV; [F9] preserves their Frobenius norms. These unstructured residual relations assert no structured pencil perturbation.

2.1F1F5F9F10F11step 1.2step 1.3algebra

Each exact Gaussian-elimination pivot is nonzero; row and column permutations and row eliminations preserve the solution set. A zero remaining block before all pivots would contradict the invertibility in steps 1.2–1.3. Back-substitution gives the unique exact solution and applying the same operations to the coordinate vectors gives the inverse. In the approximate branch, ∥I−YH∥2≤θ<1 and [F10] make YH invertible; finite-dimensional square rank and [F11] give ∥H−1∥2=∥(YH)−1Y∥2≤∥Y∥2/(1−θ). Thus each committed swap has an exact solve and valid recorded inverse bound.

2.2F1step 1.1algebra

Every complementary-selected inversion can be removed by swapping an adjacent complementary-selected pair, which decreases the inversion count by one and leaves all other relative block orders unchanged. Thus I≤b(b−1)/2 and, after I successful swaps, no inversion remains. The finite scans, local systems, and exact return branches in [F1] give a finite declared status; exhausted K or W returns its budget status.

3.1F1F6step 2.1algebra

The columns of [R;Iq] and [L;Iq] are independent because their last q rows form Iq. Applying [F6] gives orthonormal graph columns; if their span is proper, some standard coordinate vector lies outside it, so the finite scan completes each required local basis.

4.1F1F7step 3.1algebra

In the ordinary case AR−RB=−C gives [AC0B][RIq]=[RIq]B. Writing [R;Iq]=Z1Rv with Rv invertible shows the leading transformed block is similar to B. The quotient map π(x,y)=x−Ry has kernel this graph and satisfies πTJJ=Aπ, so its restriction to the orthogonal complement is an isomorphism onto the quotient and the trailing block is similar to A. Embedded local unitary updates preserve the surrounding block triangular zeros because rows below the pair vanish in its columns and columns before the pair vanish in its rows; the solved equations make the new lower-left block zero. Similarity preserves the characteristic polynomial and negative discriminant of a real 2×2 block, so whole conjugate pairs remain intact.

4.2F1F7F8step 3.1algebra

In the generalized case the two local equations give SJJ[R;Iq]=[L;Iq]B and TJJ[R;Iq]=[L;Iq]E. Writing the graph matrices as Z1Rv and Q1Rw gives a zero lower-left block and a leading pair strictly equivalent to (B,E). The full homogeneous determinant changes only by nonzero factors under exact left/right transforms [F7] and factors across diagonal pairs [F8]; cancelling the nonzero leading polynomial shows that the trailing pair has exactly the old first pair's homogeneous roots with multiplicity, including infinity and regularity. A real 2×2 pair with a finite nonreal conjugate root pair has nonsingular T block, since otherwise its determinant polynomial has degree at most one. The prescribed QR restores triangularity of this block; applying the same left factor to both QZ arrays and to Q changes the homogeneous determinant only by a nonzero factor and preserves the lower-left zero. An infinite scalar pair keeps its zero second coordinate and is never divided by it. The left update changes Q, while the right update changes Z, so the selected right deflating basis comes from Z.

4.3F1step 2.2step 3.1givenalgebra

The initial structure scan costs O(d2) scalar/evaluator units. Each local solve has order at most eight, each basis completion has bounded local dimension, and each panel update touches O(d) entries; therefore k attempts cost O(d2+kd). On success k=I≤b(b−1)/2≤d(d−1)/2, giving O(d3) worst-case swap work. Evaluating L0 bounded-support input factors on r columns costs O(L0dr+Idr); dense residual multiplication costs its separate O(d3). These counts do not bound algebraic bit cost or evaluator implementation cost.

5.1F1step 1.4step 2.2step 4.1step 4.2step 4.3algebra∎

Under the stated sufficient conditions, including enough W for every scan through the final ordered return, steps 2.2 and 4.1–4.3 show that all selected blocks move before every complementary block without splitting real pairs; the first r factor columns therefore span the selected invariant subspace or right deflating subspace of the represented computed form. Step 1.4 transports only the original unstructured residual certificate. Algorithm [F1] returns explicitly on boundary, separation, arithmetic, range, form, and budget failures; none of those statuses proves nonexistence of a stabilizing Riccati solution or supplies structured backward error.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration

Definition

Inputs are CARE data with Q=C∗C⪰0, R≻0, a supplied stabilizing gain K0, a nonnegative integer outer budget N, and either exact or safeguarded-inexact solve mode. Each exact-mode pass takes an admissible control packet for Finite-budget Bartels-Stewart solve for a Sylvester equation: pivot threshold τBS≥0, a fixed c0>0, nonnegative integer Schur sweep budgets NA,NB≤c0n, and Schur controls for each coefficient matrix (deflation tolerance, positive integer stagnation period, finite exceptional-shift tables, arithmetic/range controls, and any supplied encoding or evaluator). Use its bounded-controller mode with a supplied nonnegative integer instruction budget KBS and its built-in discriminant-sign controller. In inexact mode, also supply a nonnegative integer line-search limit L; each pass takes a Hermitian proposal P~j, a stored candidate X^j and approximate inverses for the finite Lyapunov systems below, and finite factorization witnesses for each trial. Stored inputs and point-solve proposals in this mode are exact dyadics; derived gains and coefficients are retained as exact rational expressions. Every point call uses the operationwise controller of Finite precision point linear solve certificate with explicit status; every scalar enclosure uses a finite outward evaluator with a declared work budget. Write S(K)=Q+K∗RK and LA(P)=A∗P+PA.

For j=0,…,N−1, put Aj=A−BKj. In exact mode, call Finite-budget Bartels-Stewart solve for a Sylvester equation with coefficient matrices Aj∗,Aj, right-hand side −S(Kj), and that pass's complete control packet to solve LAj(Xj)=−S(Kj). If it does not return success, stop with its status. Otherwise set Kj+1=R−1B∗Xj, append the gain and residual, and continue.

In safeguarded-inexact mode, Xj denotes the unique exact solution of LAj(Xj)=−S(Kj); it exists because K0 is stabilizing and every previously accepted trial has a Hurwitz witness. Under column vectorization, use the point matrix In⊗Aj∗+AjT⊗In for LAj, as in Column vectorization is an isometry and represents the Sylvester map by a Kronecker sum. Before the current-cost point call, clear a common positive integer denominator dj from this exact rational coefficient matrix and from −vec⁡(S(Kj)). Call Finite precision point linear solve certificate with explicit status on the resulting dyadic system, with the supplied inverse proposal for the scaled coefficient and X^j as the solution proposal. Scaling both sides by dj preserves the exact solution Xj; if the scaled entries cannot be stored exactly in the declared point format, return range-failure. A range-failure returns that status; an inconclusive result returns safeguard-inconclusive. Let its solution ball have center X^j and radius sj, replacing the center by its Hermitian part if needed. Set Dj=P~j−X^j and compute the outward Gershgorin upper bound ηj=sj+max⁡i((Dj)ii+∑k≠i∣(Dj)ik∣). For Hermitian Dj, the maximum row bound above is at least λmax⁡(Dj), by applying the eigenvector equation at a coordinate of maximal modulus. Define K~j=R−1B∗P~j and inspect the finite line-search list θℓ=2−ℓ, 0≤ℓ≤L. For each trial Kℓ=Kj+θℓ(K~j−Kj), let Aℓ=A−BKℓ and use its supplied exact factor witnesses Wℓ=Lℓ∗Lℓ with nonsingular Lℓ, and Zℓ satisfying Aℓ∗Wℓ+WℓAℓ⪯−μℓI, where μℓ>0 and −Aℓ∗Wℓ−WℓAℓ−μℓI=Zℓ∗Zℓ. Verify these exact factor identities; otherwise reject the trial and continue. Vectorize LAℓ using the same coefficient matrix as for Aj. Outward-evaluate I−RℓLAℓ and let qℓ be a Frobenius upper bound. If no finite enclosure is available or qℓ≥1, reject the trial and continue. Set κℓ=∥Rℓ∥F/(1−qℓ); the Neumann estimate and ∥T∥2≤∥T∥F give κℓ≥∥LAℓ−1∥F→F. Separately outward-evaluate the raw residual and set rℓ to an upper bound for LAℓ(P~j)+Q+Kℓ∗RKℓ, with Frobenius norm. Accept the first trial satisfying ηj+κℓrℓ≤0; then set Kj+1=Kℓ, append the accepted gain and its certificates, and proceed to pass j+1. If no trial passes, return safeguard-inconclusive without changing Kj. Any unavailable outward bound is inconclusive. The inverse bound above follows from the Neumann estimate, and rℓ bounds the raw residual separately; the preconditioned residual in Verified point and uniform linear residual certificate data is a different quantity. All certificate witnesses and bounds use the finite outward evaluator; a non-finite operation returns its range status. After at most N accepted updates return the gain sequence, solve residuals, cost-matrix data and terminal status. An arbitrary approximate Lyapunov solve is never accepted without the separate stability and descent checks above.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Finite-budget structure-preserving doubling iteration for the DARE

Definition

Input F∈{R,C}, dimensions n,m,p≥1, standard DARE data A∈Fn×n, B∈Fn×m, C∈Fp×n, and R∈Fm×m with R=R∗≻0, a nonnegative integer iteration budget N, and the operationwise arithmetic/range controller. In finite mode the stored input entries are exact dyadics; also supply stored dyadic inverse and solution proposals for every recurrence and residual solve. In exact mode set G0=BR−1B∗, H0=Q=C∗C, and A0=A, the standard DARE coefficients of Standard CARE and DARE data, equations, and conventions.

For finite-mode initialization, first solve RV=B∗ by the exact complete-pivoting elimination rule below, using order m and the n right-hand sides of B∗ in place of Mj and I. Perform this preprocessing in exact rational arithmetic on the dyadic inputs. Form BV and C∗C exactly, then round each real and imaginary component once to the declared stored format (nearest, with ties to even), obtaining stored G0 and H0; set stored A0=A. A zero pivot returns inverse-inconclusive; a component outside the controller's admitted range returns range-failure. On an initialization failure return the inputs, zero completed updates, any formed initial matrices and solve data, and unavailable for every unformed matrix or diagnostic. The finite-mode notation G0,H0 denotes these rounded matrices, not an assertion that BR−1B∗ is dyadic. Record V and the initialization rounding differences separately. This exact rational preprocessing has no asserted bit-cost bound and adds no point-certifier calls.

In exact mode, for each j=0,…,N−1, form Mj=I+GjHj and solve MjWj=I by Gaussian elimination with complete pivoting: at stage k, scan the remaining submatrix, choose a nonzero entry of largest exact modulus with lexicographic tie-breaking, swap its row and column into pivot position, eliminate below it, and back-substitute for all columns of I, undoing the accumulated column permutation in the solution. If the remaining submatrix is exactly zero before all pivots, return inverse-inconclusive. This is a finite exact-arithmetic procedure; no bit-complexity bound is asserted.

In finite arithmetic, form the stored dyadic matrix M^j=fl⁡(I+GjHj). For each standard basis vector ek, call Finite precision point linear solve certificate with explicit status with (M^j,ek,Rj,w^j,k), using the supplied stored dyadic inverse and solution proposals. Assemble the returned solution centers as W^j. If any call returns range-failure, return range-failure; if any call is inconclusive, return inverse-inconclusive; otherwise apply the recurrence updates below using W^j and the declared operationwise arithmetic. The point certifier's solution balls are diagnostics for the stored solve and do not make the rounded recurrence an exact PSD-preserving recurrence.

In exact mode let Wj be the exact solve result; in finite mode let Wj=W^j. The recurrence formulas are

Aj+1=AjWjAj,Gj+1=Gj+AjWjGjAj∗,Hj+1=Hj+Aj∗HjWjAj.

These formulas use no inverse of Aj. Any range failure while forming a stored matrix or applying an update returns range-failure with the current raw matrices.

After successful initialization, if all N updates finish without a recurrence failure, return budget-exhausted with N completed updates, including when N=0. This status records only completion of the prescribed budget; the diagnostics below remain required.

At initialization and after each update, preserve the raw matrices and report ∥Gj−Gj∗∥F and ∥Hj−Hj∗∥F. To report the standard DARE residual, form Sj=R+B∗HjB exactly from the current Hj and original input entries. In exact mode, Sj need not be dyadic: independently solve SjVj=I by the same exact elimination rule, using order m, and evaluate the residual from Standard CARE and DARE data, equations, and conventions exactly using Vj. In finite mode, Sj is dyadic because the original inputs and current stored Hj are dyadic; apply the point-certified solve rule to its m columns with the separate residual proposal packet, and outward-evaluate the residual over the certified solution balls. If the residual solve or evaluation is unavailable or inconclusive, mark the residual unavailable without changing the recurrence status. Symmetrization may be used only to form a candidate and must be followed by fresh residual and positivity checks. On every exit return the current raw matrices, status, completed updates, symmetry defects, and available residual and solve certificates. No exact positive-semidefinite or structure-preserving backward-error claim is made from a rounded recurrence alone.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Closed-region PBH rank tests characterize continuous and discrete stabilizability and detectability

Statement

Let F∈{R,C} and let A∈Fn×n, B∈Fn×m and C∈Fp×n have the domains in Stabilizability and detectability for continuous and discrete linear systems. All rank tests below are over C, including for real matrices.

  • (A,B) is continuously stabilizable if and only if rank⁡C[λI−A  B]=n for every λ with Re⁡λ≥0.
  • (A,B) is discretely stabilizable if and only if that horizontal rank is n for every λ with ∣λ∣≥1.
  • (A,C) is continuously detectable if and only if rank⁡C[λI−AC]=n for every λ with Re⁡λ≥0.
  • (A,C) is discretely detectable if and only if that vertical rank is n for every λ with ∣λ∣≥1.

Whenever the converse direction constructs a feedback or injection, its entries lie in the original field F. The boundary Re⁡λ=0 or ∣λ∣=1 is included in each forbidden region. These are exact finite-dimensional tests; a small equation residual or approximate eigenvalue does not imply them.

Facts & Assumptions

Given: The finite matrices and the existential continuous/discrete stabilizability and detectability definitions of Stabilizability and detectability for continuous and discrete linear systems.

[F1]

Stabilizability and detectability for continuous and discrete linear systems: stabilizability means existence of a same-field K with A−BK Hurwitz or Schur stable; detectability means existence of a same-field L with A−LC Hurwitz or Schur stable.

[F2]

Stabilizability and detectability imply the closed-region PBH rank tests: each of the four existential stability hypotheses implies its horizontal or vertical rank test on the corresponding closed region.

[F3]

Reachable block decomposition and same-field state-feedback pole placement: the horizontal rank test for all complex λ is equivalent to the uncontrollable block having no eigenvalue there, and a reachable block admits arbitrary same-field pole assignment.

[F4]

The characteristic polynomial of a block upper- or lower-triangular matrix is the product of the characteristic polynomials of its diagonal blocks: the characteristic polynomial of a block-triangular matrix is the product of the diagonal-block characteristic polynomials.

[F5]

Row rank equals column rank, and both equal the number of pivots: the rank of a finite complex matrix equals the rank of its adjoint, so vanishing of the left nullspace is equivalent to full row rank.

Proof

1.1F2

Necessity in all four assertions is exactly [F2]. This proves the forward implications from stabilizability or detectability to the stated rank tests, including every point on each closed boundary.

1.2F1F3F4givenalgebra

Fix either forbidden closed region Ω={λ:Re⁡λ≥0} or Ω={λ:∣λ∣≥1}. Suppose the horizontal rank test holds for all λ∈Ω, and apply [F3] to (A,B) over the original field F. The uncontrollable block Au has no eigenvalue in Ω, so its eigenvalues lie in the open left half-plane or open unit disk, respectively. Assign the reachable block repeated pole −1 or 0 by [F3], obtaining Kr. With its decomposition matrix P, set K=[Kr 0]P−1; if r=0 take K=0, and if r=n omit the empty trailing block. Then P−1(A−BK)P=[Ar−BrKrD0Au]. By [F4] its eigenvalues are the assigned stable poles and those of Au, with multiplicity; hence A−BK is Hurwitz or Schur stable, and K∈Fm×n.

2.1F1F5step 1.2algebra∎

For every λ∈C, rank⁡C[λˉI−A∗  C∗]=rank⁡C[λI−AC] because these matrices are adjoints and [F5] applies. Each forbidden region is invariant under conjugation, so its vertical test for (A,C) is the horizontal test for (A∗,C∗). Step 1.2 supplies J∈Fp×n with A∗−C∗J Hurwitz or Schur stable. Its adjoint A−J∗C has conjugate eigenvalues with the same real parts and moduli, so L=J∗∈Fn×p is the required injection. This proves both detectability converses, including their boundary cases.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Stabilizability and detectability give the unique stabilizing positive-semidefinite CARE solution

Statement

Let A∈Fn×n, B∈Fn×m, C∈Fp×n, R=R∗≻0, Q=C∗C, and G=BR−1B∗. Assume (A,B) is continuously stabilizable and (A,C) is continuously detectable, using Stabilizability and detectability for continuous and discrete linear systems. Then the CARE of Standard CARE and DARE data, equations, and conventions has exactly one Hermitian positive-semidefinite solution X. Its closed-loop matrix Ac=A−GX is Hurwitz, and for every initial state x0 the infinite-horizon value inf⁡u∫0∞(x(t)∗Qx(t)+u(t)∗Ru(t)) dt=x0∗Xx0 is attained by u(t)=−R−1B∗Xx(t). Controls are locally square-integrable and states are locally absolutely continuous solutions of x˙=Ax+Bu. A finite value also forces the terminal term x(T)∗Xx(T) to tend to zero; this transversality is proved below.

Facts & Assumptions

Given: The finite matrices in the statement, continuous stabilizability/detectability, R≻0, Q=C∗C, and locally square-integrable controls.

[F1]

Stabilizability and detectability for continuous and discrete linear systems: stabilizability/detectability mean existence of a Hurwitz state-feedback or output-injection matrix.

[F2]

Standard CARE and DARE data, equations, and conventions: G=BR−1B∗ and the CARE residual is A∗X+XA−XGX+Q.

[F4]

Picard-Lindelöf local existence and uniqueness for first-order systems: a locally Lipschitz finite-dimensional ODE vector field has a unique local IVP solution.

[F5]

Every Picard–Lindelöf initial value problem has one maximal solution on an open interval: the local solution has a unique maximal interval; any solution through the same data is its restriction.

[F6]

A Hurwitz matrix exponential has a polynomial-exponential decay bound: if M is Hurwitz then etM has a bound by a polynomial times e−αt for some α>0.

[F7]

Linear matrix ODEs have unique global solutions on a fixed interval: for a continuous real matrix coefficient on a compact interval, every homogeneous linear matrix IVP has a unique solution throughout that interval.

Proof

1.1F2F3F4F5algebra

By [F3], R−1 exists and G=G∗⪰0, since v∗Gv=(B∗v)∗R−1(B∗v)≥0. Regard the Hermitian matrices as a finite-dimensional real vector space and solve the initial-value problem P′(s)=A∗P(s)+P(s)A−P(s)GP(s)+Q,P(0)=0. Its polynomial vector field is locally Lipschitz: on each bounded matrix ball, expanding the quadratic difference gives PGP−HGH=(P−H)GP+HG(P−H), which is bounded linearly in ∥P−H∥F. Thus [F4] and [F5] give a unique maximal solution. The adjoint P(s)∗ satisfies the same IVP, so uniqueness makes P(s)=P(s)∗ on its interval.

2.1F2F7step 1.1algebra

Fix T in this interval and let x follow any admissible control on [0,T]. Put S(t)=P(T−t). Differentiating x(t)∗S(t)x(t) and substituting the ODE gives x∗Qx+u∗Ru+ddt(x∗Sx)=(u+R−1B∗Sx)∗R(u+R−1B∗Sx). Integrating, using P(0)=0, yields JT(u)=x0∗P(T)x0+∫0T(u+R−1B∗Sx)∗R(u+R−1B∗Sx) dt. The candidate feedback makes x˙=(A−GS(t))x, whose coefficient is continuous on [0,T]. If F=R, [F7] gives its unique solution on the interval. If F=C, write x in real and imaginary parts and replace the coefficient M by [Re⁡M−Im⁡MIm⁡MRe⁡M]; [F7] applies to this continuous real system, and its solution is exactly the complex feedback trajectory. Thus u=−R−1B∗Sx is admissible and makes the last integral zero, so x0∗P(T)x0 is the finite-horizon value and P(T)⪰0.

3.1F1F4F5F6step 2.1

By stabilizability [F1], choose K0 with A0=A−BK0 Hurwitz. Under u=−K0x, [F6] bounds x(t)=etA0x0 by a square-integrable polynomial-exponential multiple of ∥x0∥. The control K0x(t) has the same property, so its cost on [0,T] is at most c∥x0∥2 for one finite c independent of T. Step 2.1 therefore gives 0⪯P(T)⪯cI. If the maximal interval ended at finite T∗, the polynomial ODE field would be bounded on this bounded range, so P′(s) would be bounded and every entry of P(s) would have a finite limit as s↑T∗. Applying [F4] at that limiting matrix extends the solution past T∗, contradicting maximality [F5]. Hence P exists for every s≥0.

4.1step 2.1step 3.1algebra

For T2>T1, every control on [0,T2] has nonnegative cost after T1; its restriction to [0,T1] costs at least x0∗P(T1)x0 by step 2.1. Taking infima gives P(T2)⪰P(T1). Together with the bound in step 3.1, each quadratic form v∗P(T)v increases to a finite limit. Applying this to the coordinate vectors and their pairwise sums shows every matrix entry converges to a Hermitian limit X⪰0.

5.1F2step 4.1algebracontradiction

Let Φ(P)=A∗P+PA−PGP+Q. By step 4.1 and continuity, P′(T)=Φ(P(T))→Φ(X). If Φ(X)≠0, polarization gives a vector v with v∗Φ(X)v≠0. Then the derivative of the convergent scalar function v∗P(T)v tends to a nonzero real number, so it is eventually bounded away from zero with constant sign; integration contradicts its convergence. Thus Φ(X)=0, so X solves the CARE.

6.1F2F3step 5.1algebra

Set K=R−1B∗X and Ac=A−BK=A−GX. The CARE gives Ac∗X+XAc=−Q−K∗RK. Along x˙=Acx, integration over [0,T] gives ∫0T(∥Cx(t)∥22+u(t)∗Ru(t)) dt=x0∗Xx0−x(T)∗Xx(T)≤x0∗Xx0. The Cholesky factor R=LL∗ is invertible by [F3], so u∗Ru=∥L∗u∥22 controls ∥u∥22 by the finite operator norm of L−∗. Hence Cx,u∈L2(0,∞).

7.1F1F6step 6.1algebracontradiction

By detectability [F1], choose L with Ao=A−LC Hurwitz. Then x˙=Aox+w, where w=Bu+LCx∈L2. Since x is locally absolutely continuous, w is locally integrable and the product rule gives ddt(e−tAox(t))=e−tAow(t) almost everywhere. Integrating this identity from 0 to t and multiplying by etAo proves x(t)=etAox0+∫0te(t−s)Aow(s) ds. From [F6], there are M,α>0 with ∥etAo∥2≤Me−αt after absorbing the finite polynomial factor into a smaller exponential rate. The initial term tends to zero. For the integral, split at a fixed S: the portion 0≤s≤S tends to zero as t→∞; by Cauchy–Schwarz the tail is at most M(2α)−1/2∥w∥L2(S,∞), which tends to zero as S→∞. Thus x(t)→0. Since this holds for every initial state, no eigenvalue of Ac can have nonnegative real part: an eigenvector for such an eigenvalue would not decay. Therefore Ac is Hurwitz.

8.1F1F2F3step 2.1step 6.1step 7.1algebra

For any admissible control of finite infinite-horizon cost, u,Cx∈L2. Repeating the stable-convolution argument in step 7.1 gives x(T)→0. The same square-completion identity as step 2.1, now with constant S=X, yields JT(u)=x0∗Xx0−x(T)∗Xx(T)+∫0T(u+Kx)∗R(u+Kx) dt. Taking T→∞ gives J∞(u)≥x0∗Xx0. The feedback in step 6.1 has u+Kx=0 and x(T)→0, hence attains equality.

9.1F2F6step 6.1step 7.1algebra∎

Let Y⪰0 be any other CARE solution. Repeating steps 6.1–7.1 with Y proves AY=A−GY is Hurwitz. Subtracting the CAREs and using XGX−YGY=PG(X−Y)+(X−Y)GYwith P=X gives Ac∗(X−Y)+(X−Y)AY=0. Hence the derivative of etAc∗(X−Y)etAY is zero, so this matrix equals X−Y for every t≥0. Both exponential factors tend to zero by [F6], forcing X−Y=0. Thus X is the unique positive-semidefinite solution, and in particular the unique stabilizing one.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution

Statement

Let A∈Fn×n, B∈Fn×m, C∈Fp×n, R=R∗≻0, and Q=C∗C. Assume (A,B) is discretely stabilizable and (A,C) discretely detectable, using Stabilizability and detectability for continuous and discrete linear systems. Then the DARE of Standard CARE and DARE data, equations, and conventions has exactly one Hermitian positive-semidefinite solution X. For the equivalent Riccati map f(P)=Q+A∗P(I+GP)−1A, its finite-horizon iterates P0=0, Pk+1=f(Pk) satisfy 0⪯Pk↑X. For all Hermitian positive-semidefinite Y,Z, f(Y)−f(Z)=Ac(Y)∗(Y−Z)Ac(Z),Ac(Y)=(I+GY)−1A. The solution satisfies R+B∗XB≻0, and its closed loop Ac=A−B(R+B∗XB)−1B∗XA is Schur stable. For each x0, the infinite-horizon discrete cost inf⁡(uk)∑k=0∞(xk∗Qxk+uk∗Ruk),xk+1=Axk+Buk, over sequences with finite cost equals x0∗Xx0 and is attained by uk=−Kdxk. Singular A is allowed throughout; no inverse of A is used.

Facts & Assumptions

Given: The finite matrices in the statement, discrete stabilizability/detectability, R≻0, Q=C∗C, and the discrete-time dynamics.

[F1]

Stabilizability and detectability for continuous and discrete linear systems: discrete stabilizability/detectability mean there exist a feedback/injection making the corresponding matrix Schur stable.

[F2]

Standard CARE and DARE data, equations, and conventions: G=BR−1B∗ and the DARE residual and feedback are defined there.

[F3]

Powers of a Schur-stable matrix decay geometrically up to a polynomial factor: if M is Schur stable, then for any r with ρ(M)<r<1, ∥Mk∥2≤Crrk.

[F5]

A non-negative operator has a unique non-negative square root: if P⪰0 and v∗Pv=0, then Pv=0.

[F6]

Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T: an injective endomorphism of a finite-dimensional space is invertible.

Proof

1.1F2F4algebrainduction

Define P0=0 and recursively Sj=R+B∗PjB,Kj=Sj−1B∗PjA,Pj+1=Q+A∗PjA−A∗PjBSj−1B∗PjA. If Pj⪰0, then for nonzero v, v∗Sjv=v∗Rv+(Bv)∗Pj(Bv)>0, so Sj−1 exists. For each x,u, expansion and completion of the positive square gives x∗Qx+u∗Ru+(Ax+Bu)∗Pj(Ax+Bu)=x∗Pj+1x+(u+Kjx)∗Sj(u+Kjx). Thus x∗Pj+1x is the finite-horizon value for j+1 stages, attained by the minimizing first control; induction gives Pj⪰0.

1.2F2F5F6algebra

For positive-semidefinite P,Q, if (I+PQ)v=0, multiplication by v∗Q gives v∗Qv+(Qv)∗P(Qv)=0. Both terms are nonnegative, so [F5] gives Qv=0 and then v=0. Interchanging P,Q proves the same for I+QP. Thus I+YG, I+GY, I+GZ, and I+ZG are injective and hence invertible by [F6]. Since (I+YG)Y=Y(I+GY), multiplication by the established inverses gives (I+YG)−1Y=Y(I+GY)−1. Further, multiplying both sides of Y(I+GY)−1−Z(I+GZ)−1=(I+YG)−1(Y−Z)(I+GZ)−1 by I+YG on the left and I+GZ on the right reduces both sides to Y−Z. Substitution into f(Y)−f(Z) proves the difference identity in the Statement.

2.1F1F3step 1.1algebra

Longer horizons add nonnegative stage costs, so their value matrices increase in the Loewner order: 0⪯Pj⪯Pj+1. By stabilizability [F1], choose K0 so A0=A−BK0 is Schur stable. Under that fixed feedback the cost is bounded by ∑k≥0(∥C∥22+∥K0∗RK0∥2)∥A0kx0∥22≤c∥x0∥22, because [F3] gives a summable geometric-square bound. Therefore Pj⪯cI. The forms on ei, ei+ej, and ei+iej are bounded and monotone; they determine the diagonal entries and the real and imaginary parts of each Hermitian off-diagonal entry. Thus all entries converge to a Hermitian X⪰0.

3.1F2F4step 1.1step 2.1algebra

The update map is continuous on P⪰0: R+B∗PB⪰R≻0, so its inverse varies continuously there. Passing to the limit in step 1.1 gives the DARE for X, and the same inequality gives R+B∗XB≻0.

4.1F1F2step 1.1step 3.1algebra

Put S=R+B∗XB, K=S−1B∗XA, and Ac=A−BK. The square identity in step 1.1 with Pj=X yields x∗Qx+u∗Ru+(Ax+Bu)∗X(Ax+Bu)−x∗Xx=(u+Kx)∗S(u+Kx). For u=−Kx, summing from k=0 to N−1 gives total stage cost x0∗Xx0−xN∗XxN≤x0∗Xx0. Thus u,Cx∈ℓ2.

5.1F1F3step 4.1algebracontradiction

By detectability [F1], choose L such that Ao=A−LC is Schur stable. Along the feedback trajectory, xk+1=Aoxk+wk,wk=Buk+LCxk∈ℓ2. Variation of constants gives xk=Aokx0+∑j=0k−1Aok−1−jwj. The first term tends to zero by [F3]. For any fixed J, the finite sum over j<J also tends to zero. The remaining sum is bounded by (∑ℓ≥0∥Aoℓ∥22)1/2(∑j≥J∥wj∥22)1/2. The first factor is finite by [F3], and the second tends to zero as J→∞. Hence xk→0. This holds for every initial state, so no eigenvalue of Ac can satisfy ∣λ∣≥1; therefore Ac is Schur stable.

6.1F1F2step 4.1step 5.1algebra

For any finite-cost control, u,Cx∈ℓ2; the same detectability argument in step 5.1, now with its state equation, gives xk→0. Summing the square identity in step 4.1 and taking N→∞ gives cost at least x0∗Xx0. The stabilizing feedback makes the square term zero and has xN→0, so it attains equality.

7.1F2F3step 5.1step 1.2algebra∎

Let Y⪰0 be another DARE solution. Step 5.1 applied to Y shows its closed loop AY=(I+GY)−1A is Schur stable. Since both X and Y are fixed points, step 1.2 gives X−Y=Ac(X)∗(X−Y)AY. Iteration yields X−Y=(Ac(X)∗)k(X−Y)AYk. By [F3], both powers tend to zero, so the right side tends to zero and X=Y.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

The DARE doubling recurrence composes two Riccati steps and preserves positive semidefiniteness

Statement

For Hermitian G,H⪰0, define ΦG(X)=X(I+GX)−1 and f(X)=H+A∗ΦG(X)A on X⪰0. One step of the exact inverse recurrence in Finite-budget structure-preserving doubling iteration for the DARE is well-defined, preserves Gj,Hj⪰0, and its updated triple satisfies f∘f(X)=H1+A1∗X(I+G1X)−1A1, where A1=A(I+GH)−1A,G1=G+A(I+GH)−1GA∗,H1=H+A∗H(I+GH)−1A. Consequently, starting from (A,G,H), the exact recurrence satisfies Hj=f2j(0) after j updates. These claims concern exact arithmetic; the rounded branch has only its separately reported diagnostics.

Facts & Assumptions

Given: Finite matrices A and Hermitian positive-semidefinite G,H over F∈{R,C}.

[F1]

Finite-budget structure-preserving doubling iteration for the DARE: the exact-mode update formulas are A1=A(I+GH)−1A, G1=G+A(I+GH)−1GA∗, and H1=H+A∗H(I+GH)−1A.

[F2]

Standard CARE and DARE data, equations, and conventions: for G=BR−1B∗, the DARE map is X↦Q+A∗X(I+GX)−1A.

[F3]

A non-negative operator has a unique non-negative square root: a positive-semidefinite matrix has a positive-semidefinite square root.

Proof

1.1F1F3algebra

If (I+GH)v=0, then multiplication by v∗H gives v∗Hv+(Hv)∗G(Hv)=0. Both terms are nonnegative, so Hv=0 and then v=0. Thus I+GH is invertible; the same argument applies to I+HG. The identities (I+GH)−1G=G(I+HG)−1=G1/2(I+G1/2HG1/2)−1G1/2, H(I+GH)−1=(I+HG)−1H=H1/2(I+H1/2GH1/2)−1H1/2 follow by multiplication and the push-through identity. Their middle matrices are positive definite, so both displayed products are Hermitian positive semidefinite. Therefore the updates in [F1] give G1,H1⪰0 and use only an inverse already proved to exist.

1.2F1F2algebra

For any invertible displayed factors, direct multiplication gives the resolvent identity ΦG(X)−ΦG(Y)=(I+XG)−1(X−Y)(I+GY)−1, and the push-through identity (I+UV)−1U=U(I+VU)−1. For X≻0, ΦG(X)−1=X−1+G. Put U=ΦG(X) and Y=A∗UA. Applying the resolvent identity at H+Y and H gives ΦG(H+Y)−ΦG(H)=(I+(H+Y)G)−1Y(I+GH)−1. Since I+(H+Y)G=(I+HG)+YG, multiplication verifies (I+(H+Y)G)−1Y=(I+HG)−1Y(I+G(I+HG)−1Y)−1. Substituting Y=A∗UA and applying push-through twice rewrites this difference as (I+HG)−1A∗(U−1+AG(I+HG)−1A∗)−1A(I+GH)−1. Using U−1=X−1+G and [F1], the middle inverse is X(I+G1X)−1. Now f(f(X))−H1=A∗(ΦG(H+Y)−ΦG(H))A. Its left factor is A∗(I+HG)−1A∗=A1∗ and its right factor is A(I+GH)−1A=A1. Adding H1=H+A∗ΦG(H)A proves the composition formula for X≻0.

2.1F1step 1.1step 1.2inductionalgebra∎

For singular X⪰0, replace it by X+εI in step 1.2 and let ε↓0. Step 1.1 guarantees every I+G(X+εI) and I+G1(X+εI) is invertible; matrix inversion is continuous at these invertible limits. Hence the composition identity extends to every X⪰0, including singular A and singular X. By induction on j, the updated Riccati map is f2j and its value at zero is Hj.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The stabilizing CARE solution is the Hamiltonian stable invariant graph

Statement

Let X⪰0 be the stabilizing CARE solution from Stabilizability and detectability give the unique stabilizing positive-semidefinite CARE solution, let G=BR−1B∗, and define H=[A−G−Q−A∗],Ac=A−GX. Then H[IX]=[IX]Ac. Moreover, H has exactly n eigenvalues in the open left half-plane and n in the open right half-plane, none on the imaginary axis, and Ran⁡[IX] is its stable invariant subspace.

Facts & Assumptions

Given: The standard CARE data and the Hermitian positive-semidefinite stabilizing solution X.

[F1]

Stabilizability and detectability give the unique stabilizing positive-semidefinite CARE solution: Ac=A−GX is Hurwitz and A∗X+XA−XGX+Q=0.

[F2]

Standard CARE and DARE data, equations, and conventions: G=BR−1B∗ is Hermitian positive semidefinite and ∗ is the adjoint.

[F3]

The characteristic polynomial of a block upper- or lower-triangular matrix is the product of the characteristic polynomials of its diagonal blocks: the characteristic polynomial of a block-triangular matrix is the product of those of its diagonal blocks.

[F4]

For every finite-dimensional space, σF(T) is exactly the set of roots in F of χT: over C, eigenvalues are precisely the roots of the characteristic polynomial.

[F5]

Every nonconstant polynomial in C[x] splits into linear factors: each degree-n complex characteristic polynomial has n roots counted with algebraic multiplicity.

[F6]

Every finite-dimensional endomorphism over an algebraically closed field has Jordan form: generalized eigenspaces span the complex space and their dimensions equal the corresponding algebraic multiplicities.

Proof

1.1F1F2algebra

Block multiplication gives H[IX]=[A−GX−Q−A∗X]. By [F1], −Q−A∗X=XA−XGX=X(A−GX), proving the graph identity.

2.1F1F3F4F5F6step 1.1algebra∎

Set TX=[I0XI], whose inverse is [I0−XI]. Using [F1], TX−1HTX=[A−GX−G0−(A−GX)∗]. The eigenvalues of the first diagonal block lie in the open left half-plane by [F1]. If λ is a root of its characteristic polynomial, then −λ‾ is a root of the characteristic polynomial of −(A−GX)∗, since det⁡(−λ‾I+(A−GX)∗)=det⁡(−λI+(A−GX))‾=0; these reflected roots lie in the open right half-plane. By [F5] each diagonal characteristic polynomial has degree n and splits into n roots counted with algebraic multiplicity. The characteristic polynomial factorization [F3] and root/eigenvalue connection [F4] therefore give exactly n eigenvalues of H in each open half-plane and none on the imaginary axis. The first coordinate subspace is invariant and its restriction has the stable spectrum of A−GX. Any generalized eigenvector of the displayed triangular matrix for a stable eigenvalue has trailing component in the kernel of a power of (−(A−GX)∗−λI); that matrix is invertible because the trailing spectrum is in the open right half-plane, so the trailing component is zero. By [F6] these generalized eigenspaces have total dimension equal to the stable algebraic multiplicity n from [F5], so they fill the first coordinate subspace, which is therefore the stable invariant subspace. Applying TX maps it to Ran⁡[IX].

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The stabilizing DARE solution is the stable deflating graph of a regular symplectic pencil

Statement

Let X⪰0 be the stabilizing DARE solution, G=BR−1B∗, and N=[A0−QI],M=[IG0A∗],Ac=A−B(R+B∗XB)−1B∗XA. Then N[IX]=M[IX]Ac. The pencil (N,M) is regular. Its homogeneous determinant has n roots strictly inside the unit disk and n roots strictly outside the closed unit disk, with infinite roots counted in the latter group. Thus it has no unit-circle roots, even if A is singular, and Ran⁡[IX] is its stable deflating graph.

Facts & Assumptions

[F1]

Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution: X=X∗⪰0, S=R+B∗XB≻0, and Ac=A−BS−1B∗XA is Schur stable.

[F2]

Standard CARE and DARE data, equations, and conventions: G=BR−1B∗ and the DARE residual is Q+A∗XA−A∗XBS−1B∗XA−X.

[F3]

A non-negative operator has a unique non-negative square root: each finite-dimensional non-negative self-adjoint matrix has a non-negative square root.

[F4]

Regular matrix pencils and homogeneous generalized eigenvalues: a square pencil is regular when its homogeneous determinant is not the zero polynomial.

[F5]

For same-sized finite square matrices over a commutative ring, det⁡(AB)=det⁡(A)det⁡(B): determinants multiply under finite square matrix products, so the determinant is unchanged by the determinant-one shears used below.

[F6]

The determinant of a triangular matrix is the product of its diagonal entries: the determinant of a triangular matrix is the product of its diagonal entries; in particular, the two unit-triangular shears below have determinant one.

[F7]

The homogeneous determinant factors across a block upper triangular pencil: the homogeneous determinant of a block upper-triangular pencil factors across its diagonal blocks.

[F8]

For every finite-dimensional space, σF(T) is exactly the set of roots in F of χT: finite eigenvalues of a matrix are exactly the roots of its characteristic polynomial.

[F9]

Every nonconstant polynomial in C[x] splits into linear factors: each complex characteristic polynomial of degree n has n roots counted with algebraic multiplicity.

[F10]

Every finite-dimensional endomorphism over an algebraically closed field has Jordan form: generalized eigenvectors span a complex finite-dimensional space, with total dimension counted by algebraic multiplicity.

Proof

1.1F1F2F3algebra

The matrix I+GX is invertible. Indeed, if (I+GX)v=0, multiplication by v∗X gives v∗Xv+(Xv)∗G(Xv)=0. Both summands are nonnegative. By [F3], v∗Xv=0 implies Xv=0, and the original equation then gives v=0. Also S=R+B∗XB≻0 by [F1]. The identity (I+GX)−1=I−BS−1B∗X is verified by multiplying the right side by I+GX: the extra term is B[R−1−S−1−S−1(B∗XB)R−1]B∗X=0, since S=R+B∗XB. Therefore Ac=(I+GX)−1A.

2.1F1F2step 1.1algebra

The DARE and the identity in step 1.1 imply X−Q=A∗X(I+GX)−1A=A∗XAc. Consequently, N[IX]=[AX−Q]=[I+GXA∗X]Ac=M[IX]Ac. This proves the deflating graph identity.

3.1F1F4F5F6F7F8F9F10step 1.1step 2.1algebra∎

Put TX=[I0XI] and LX=[I0−A∗X(I+GX)−1I]. By [F6] both are block triangular with identity diagonal and determinant one. For arbitrary homogeneous coordinates [α:β], LX(βN−αM)TX=[(I+GX)(βAc−αI)−αG0βI−αAc∗]. The lower-left block vanishes by X−Q=A∗XAc; the lower-right block uses (I+GX)−1G=G(I+XG)−1 and I−X(I+GX)−1G=(I+XG)−1. Taking determinants and using [F5] and [F7] gives det⁡(βN−αM)=det⁡(I+GX)det⁡(βAc−αI)det⁡(βI−αAc∗). The first homogeneous factor has n roots, counted with multiplicity; all are finite and equal to eigenvalues of Ac, hence strictly inside the disk by [F1] and [F8]. The roots of Ac∗ are the conjugates of those of Ac, since det⁡(μI−Ac∗)=det⁡(μ‾I−Ac)‾; hence each nonzero eigenvalue of Ac∗ has modulus less than one. The second factor has n roots, counted with multiplicity: each finite root is the reciprocal of a nonzero eigenvalue of Ac∗ and therefore has modulus greater than one, while every zero eigenvalue of Ac∗ contributes a root at β=0, which is infinite. The root counts follow from [F9], with finite eigenvalues identified by [F8]. Neither factor vanishes on ∣α∣=∣β∣, so the pencil is regular with the stated root split. The homogeneous determinant is invariant under these transforms because [F5] gives multiplicativity and both shear determinants equal one by [F6]. Finally, (I+GX) is invertible by step 1.1, so M[I;X] has full column rank. A Jordan basis of Ac from [F10], together with N[I;X]=M[I;X]Ac from step 2.1, shows that the graph carries all n stable finite root chains; the determinant factorization shows there are exactly n stable roots in total, so this is the stable deflating graph. This uses no inverse of A.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

Verified Lyapunov residual, descent, and stability checks make an inexact Newton-Kleinman step safe

Statement

Consider a trial gain Kt in the safeguarded-inexact branch of Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration, with At=A−BKt. Suppose outward certificates give W≻0, μ>0, At∗W+WAt⪯−μI, an inverse bound κ≥∥LAt−1∥F→F, a residual bound r for a Hermitian approximation P~ to At∗P+PAt+Q+Kt∗RKt=0, and an upper bound η≥λmax⁡(P~−Xj) with η+κr≤0. Then At is Hurwitz, its exact cost matrix Pt exists and is positive semidefinite, and Pt⪯Xj. Thus every accepted line-search step preserves stability and does not increase the exact closed-loop cost matrix.

Facts & Assumptions

Given: The current exact cost matrix Xj, trial gain, residual data, and verified bounds in the statement.

[F1]

Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration: a trial is accepted only if its Lyapunov margin, inverse bound, residual bound, and descent upper bound satisfy the stated tests.

[F2]

Standard CARE and DARE data, equations, and conventions: Q=C∗C⪰0 and R≻0.

[F3]

The Hurwitz Lyapunov integral is the unique solution and has the stated positivity: for Hurwitz At, the solution of At∗P+PAt+S=0 is the unique integral ∫0∞etAt∗SetAt dt, and is positive semidefinite for S⪰0.

[F4]

A Sylvester equation is uniquely solvable exactly when the spectra are disjoint: when At is Hurwitz, the Lyapunov operator E↦At∗E+EAt is invertible.

[F5]

Verified point and uniform linear residual certificate data specifies bounds for an approximate-inverse defect and a preconditioned linear residual, with a usable certificate requiring q<1. The raw Lyapunov residual bound r and inverse-norm bound κ in this proposition are separate hypotheses of the Statement.

Proof

1.1F1givenalgebra

If Atv=λv with v≠0, the certificate gives 2Re⁡(λ)v∗Wv=v∗(At∗W+WAt)v≤−μ∥v∥22<0. Because W≻0, every eigenvalue has negative real part, so At is Hurwitz.

2.1givenF1F2F3F4F5step 1.1algebra∎

Let Pt be the exact solution of the Lyapunov equation; it exists uniquely by [F3] and [F4], and Pt⪰0 by [F2]–[F3]. If Rt denotes the exact residual of P~, then LAt(P~−Pt)=Rt. The Statement's certified inverse and raw residual bounds give ∥P~−Pt∥F≤κr; these are distinct from the certificate quantities described in [F5]. For each unit vector v, v∗(Pt−Xj)v≤v∗(P~−Xj)v+∥Pt−P~∥2≤η+κr≤0. Thus Pt⪯Xj.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

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

Statement

Let X^=X^∗ be a CARE candidate, A^c=A−GX^, and L(E)=A^c∗E+EA^c,Fc(X)=A∗X+XA−XGX+Q. Assume A^c is certified Hurwitz, L is invertible on Hermitian matrices, and outward-verified bounds satisfy κ≥∥L−1∥F→F,r≥∥Fc(X^)∥F,g≥∥G∥2, with ρ>0 such that κ(r+gρ2)≤ρ,2κgρ<1. Then there is exactly one Hermitian CARE root in the closed Frobenius ball ∥X−X^∥F≤ρ.

If also a verified Hermitian W≻0 and γ>0 satisfy −(A^c∗W+WA^c)⪰γI,2∥W∥2gρ<γ, 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: Fc(X)=A∗X+XA−XGX+Q and Ac(X)=A−GX.

[F2]

A Sylvester equation is uniquely solvable exactly when the spectra are disjoint: E↦A^c∗E+EA^c is invertible when σ(A^c∗)∩(−σ(A^c))=∅; this holds for Hurwitz 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 ∥AXB∥F≤∥A∥2∥X∥F∥B∥2.

[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 Ac, the solution of Ac∗Y+YAc=−S is the convergent integral Y=∫0∞etAc∗SetAc dt, 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 Fc(X^+E)=Fc(X^)+L(E)−EGE. Thus the root equation is equivalent to E=T(E):=−L−1Fc(X^)+L−1(EGE).

2.1A1F3F4F5F9step 1.1algebra

By [F5], ∥EGE∥F≤g∥E∥F2. The assumptions give ∥T(E)∥F≤κ(r+gρ2)≤ρ on the closed ball. Also EGE−FGF=(E−F)GE+FG(E−F), so [F5] gives ∥T(E)−T(F)∥F≤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=X^+E be this root. Its closed loop is Ac(X)=A^c−GE. Expanding, Ac(X)∗W+WAc(X)=A^c∗W+WA^c−EGW−WGE. By [F6] and [A1], ∥EGW+WGE∥2≤2∥W∥2gρ<γ. Hence the left side is negative definite. For any eigenpair Ac(X)v=λv, v≠0, this gives 2Re⁡(λ)v∗Wv<0; since W≻0, Re⁡λ<0. Thus the root is stabilizing. Its CARE identity also gives Ac(X)∗X+XAc(X)=−(Q+XGX). Here Q+XGX⪰0 because Q,G⪰0. Since Ac(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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

A DARE residual, Stein inverse bound, and Lyapunov margin certify a stabilizing root

Statement

Let X^=X^∗ be a DARE candidate, S(X)=R+B∗XB, K(X)=S(X)−1B∗XA, Ac(X)=A−BK(X), and let Fd(X)=Q+A∗XA−A∗XBS(X)−1B∗XA−X. Suppose S(X^)⪰δ0I is outward-certified. For a proposed radius ρ>0 put a=∥A∥2,b=∥B∥2,m=∥X^∥F+ρ,δ=δ0−b2ρ. Require δ>0 and define LK=abδ+ab3mδ2,Mc=a+ab2mδ,Lc=bLK,LD=2McLc. Let D(E)=Ac(X^)∗EAc(X^)−E be invertible on Hermitian matrices, with outward-certified κ≥∥D−1∥F→F and r≥∥Fd(X^)∥F. If κ(r+LDρ2/2)≤ρ,κLDρ<1, there is exactly one Hermitian DARE root in the closed Frobenius ρ-ball, and R+B∗XB⪰δI throughout that ball.

For the stabilizing branch, additionally suppose A^c=Ac(X^) is Schur stable and an outward-certified W≻0 satisfies W−A^c∗WA^c⪰γI. If, with η=Lcρ, ∥W∥2(2Mcη+η2)<γ, then the root is Schur-stabilizing. Under the standard DARE hypotheses of Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution, it is the unique stabilizing positive-semidefinite solution.

Facts & Assumptions

Given: The DARE data and residual map of Standard CARE and DARE data, equations, and conventions, a Hermitian candidate, and the verified constants in the Statement.

[F1]

Standard CARE and DARE data, equations, and conventions: S(X)=R+B∗XB, Ac(X)=A−BS(X)−1B∗XA, and Fd(X)=Q+A∗XA−A∗XBS(X)−1B∗XA−X.

[F2]

Verified point and uniform linear residual certificate data specifies mathematical bounds for a linear approximate-inverse defect and preconditioned residual, and does not prescribe how to establish them. The DARE bounds used here are the separate hypotheses in [A1].

[F3]

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

[F4]

Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison: ∥AXB∥F≤∥A∥2∥X∥F∥B∥2 and ∥X∥2≤∥X∥F.

[F6]

Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution: under the standard discrete hypotheses there is a unique stabilizing positive-semidefinite DARE solution.

[F7]

Powers of a Schur-stable matrix decay geometrically up to a polynomial factor: if Ac is Schur stable, then ∣Ack∣2→0 geometrically.

[F8]

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 lower eigenvalue bound δ0, norm bounds, residual bound, inverse bound κ, and Lyapunov margin are outward-verified inputs. If any bound is unavailable, this item supplies no certificate.

Proof

1.1F1A1F3F4F5algebra

For any Hermitian E with ∥E∥F≤ρ, [F3] and [F4] give S(X^+E)=S(X^)+B∗EB⪰(δ0−b2ρ)I=δI. Thus S(X) is invertible on the ball and ∥S(X)−1∥2≤δ−1. The resolvent identity gives ∥S(X)−1−S(Y)−1∥2≤b2δ−2∥X−Y∥F. Using K(X)=S(X)−1B∗XA and splitting the difference into the change in X and the change in S−1 yields ∥K(X)−K(Y)∥F≤LK∥X−Y∥F,∥Ac(X)∥2≤Mc,∥Ac(X)−Ac(Y)∥2≤Lc∥X−Y∥F.

2.1F1A1F4F5step 1.1algebra

Differentiating S−1S=I gives d(S−1)[E]=−S−1(B∗EB)S−1. Substituting this in the derivative of Fd and using K=S−1B∗XA gives Fd′(X)[E]=Ac(X)∗EAc(X)−E. Consequently, for DX=Fd′(X) and DY=Fd′(Y), [F4]–[F5] give ∥DX−DY∥F→F≤(∥Ac(X)∥2+∥Ac(Y)∥2)∥Ac(X)−Ac(Y)∥2≤LD∥X−Y∥F. Integrating the derivative along the segment from X^ to X^+E gives a Taylor remainder R(E) with Fd(X^+E)=Fd(X^)+D(E)+R(E),∥R(E)∥F≤LD∥E∥F2/2.

3.1A1F2F8step 2.1algebra

The root equation is the fixed-point equation E=T(E):=−D−1Fd(X^)−D−1R(E). The bounds in [A1], separate from the linear certificate data in [F2], make T a self-map of the closed ball. For E,F in that ball, integrating DX−D along the segment between them gives ∥R(E)−R(F)∥F≤LDρ∥E−F∥F, so T has contraction factor at most κLDρ<1. Iteration from zero has successive differences bounded by a geometric sequence, hence is Cauchy. The closed Hermitian ball is complete by [F8], so the sequence converges in the ball; continuity makes its limit a fixed point. The same contraction inequality makes it unique.

4.1A1F1F6F7step 3.1algebra∎

Let X=X^+E be the root. Then ∥Ac(X)−A^c∥2≤Lcρ=η. Expanding the Stein form, Ac(X)∗WAc(X)−A^c∗WA^c=A^c∗WΔ+Δ∗WA^c+Δ∗WΔ, where Δ=Ac(X)−A^c. Its norm is at most ∥W∥2(2Mcη+η2)<γ. Hence W−Ac(X)∗WAc(X)≻0. For an eigenvector Ac(X)v=λv, this gives (1−∣λ∣2)v∗Wv>0, so ∣λ∣<1. Let K=K(X), S=R+B∗XB, and xk+1=Ac(X)xk, uk=−Kxk. Since SK=B∗XA, we have K∗SK=A∗XBS−1B∗XA. Expanding Ac∗XAc=(A−BK)∗X(A−BK) gives Ac∗XAc=A∗XA−K∗SK−K∗SK+K∗B∗XBK=A∗XA−K∗SK−K∗RK. The DARE root equation therefore gives X=Q+K∗RK+Ac∗XAc, which along xk+1=Acxk and uk=−Kxk is the exact square identity xk∗Qxk+uk∗Ruk+xk+1∗Xxk+1=xk∗Xxk. Summing to N−1 yields x0∗Xx0=∑k<N(xk∗Qxk+uk∗Ruk)+xN∗XxN. By [F7], xN→0, so x0∗Xx0 is a sum of nonnegative terms; hence X⪰0. Now [F6] identifies it as the unique stabilizing positive-semidefinite solution.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Exact Newton-Kleinman iteration preserves stability, decreases cost matrices, and converges quadratically locally

Statement

Assume the continuous stabilizability and detectability hypotheses of Stabilizability and detectability give the unique stabilizing positive-semidefinite CARE solution. From a supplied stabilizing K0, define the infinite exact recurrence, for every j≥0, by Aj=A−BKj,Aj∗Xj+XjAj=−(Q+Kj∗RKj),Kj+1=R−1B∗Xj. These exact Lyapunov solutions exist uniquely. Every closed loop Aj=A−BKj is Hurwitz, every exact Lyapunov matrix Xj is positive semidefinite, and Xj+1⪯Xj. The sequence converges to the unique stabilizing CARE solution X∗. Once j is sufficiently large, there is a finite constant C such that ∥Xj+1−X∗∥F≤C∥Xj−X∗∥F2. Every successful exact update of Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration agrees with this recurrence, so a finite call returns only a prefix, possibly shortened by a solver failure. Convergence and the eventual quadratic estimate concern the infinite recurrence; no such guarantee is asserted for arbitrary inexact solves.

Facts & Assumptions

Given: Continuous CARE data, continuous stabilizability/detectability, a stabilizing K0, and the infinite exact Lyapunov recurrence in the Statement.

[F1]

Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration: Aj=A−BKj, Aj∗Xj+XjAj=−(Q+Kj∗RKj), and Kj+1=R−1B∗Xj.

[F2]

Stabilizability and detectability give the unique stabilizing positive-semidefinite CARE solution: there is a unique Hermitian positive-semidefinite stabilizing solution X∗.

[F3]

The Hurwitz Lyapunov integral is the unique solution and has the stated positivity: a Hurwitz Lyapunov equation with positive-semidefinite forcing has its unique positive-semidefinite integral solution.

[F4]

A Hurwitz matrix exponential has a polynomial-exponential decay bound: a Hurwitz matrix exponential is bounded by a polynomial times a decaying exponential.

[F5]

Standard CARE and DARE data, equations, and conventions: G=BR−1B∗ and the CARE residual is A∗X+XA−XGX+Q.

Proof

1.1F1F3F5giveninductioncontradiction

Suppose Aj is Hurwitz. By [F3], the exact solution Xj of the policy Lyapunov equation is Xj=∫0∞etAj∗(Q+Kj∗RKj)etAj dt⪰0. For Δj=Kj+1−Kj, expansion using B∗Xj=RKj+1 gives Aj+1∗Xj+XjAj+1+Q+Kj+1∗RKj+1=−Δj∗RΔj. If Aj+1v=λv with Re⁡λ≥0, the quadratic form of the left side is 2Re⁡(λ)v∗Xjv+v∗Qv+(Kj+1v)∗R(Kj+1v)≥0, while the right side is nonpositive. Equality forces Kj+1v=0 and Δjv=0, hence Kjv=0 and Ajv=Av=λv, contradicting that Aj is Hurwitz. Starting from K0, induction proves every Aj Hurwitz and every Xj⪰0.

2.1F1F2F3step 1.1algebra

Subtracting the Lyapunov equations for Xj and Xj+1 after expressing both under Aj+1 gives Aj+1∗(Xj−Xj+1)+(Xj−Xj+1)Aj+1=−Δj∗RΔj. The Lyapunov integral [F3] therefore yields Xj−Xj+1⪰0. The decreasing sequence is bounded below by zero, so each quadratic form converges. Evaluating at ei, ei+ej, and ei+iej shows convergence of every matrix entry to a Hermitian limit X∞⪰0. Since Kj+1=R−1B∗Xj, the gains also converge. Passing to the limit in the policy Lyapunov equation gives the CARE for X∞; [F2] identifies this positive-semidefinite root as X∗.

3.1F1F2F3F4step 2.1algebra∎

Let Ej=Xj−X∗ and A∗=A−BR−1B∗X∗. Put Dj=Kj+1−K∗=R−1B∗Ej. Subtract the CARE identity at X∗ from the policy Lyapunov equation under Aj+1 to obtain Aj+1∗Ej+1+Ej+1Aj+1=−Dj∗RDj. By [F2], A∗ is Hurwitz. Choose W=∫0∞etA∗∗IetA∗ dt≻0 using [F3], so A∗∗W+WA∗=−I. Since Aj+1→A∗, for all large j one has Aj+1∗W+WAj+1⪯−12I. Along x˙=Aj+1x, differentiation gives ddt(x∗Wx)≤−12∥x∥22≤−12∥W∥2x∗Wx. Consequently ∥etAj+1∥2≤Me−αt with M=(∥W∥2/λmin⁡(W))1/2 and α=1/(4∥W∥2), uniformly for all sufficiently large j. Applying the Lyapunov integral to the error equation yields ∥Ej+1∥F≤(∫0∞M2e−2αt dt)∥R∥2∥R−1B∗∥22∥Ej∥F2. The integral is finite and supplies the stated local quadratic constant.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Finite-budget CARE and DARE candidate extraction from ordered Schur and QZ forms

Definition

Inputs are finite CARE or DARE data from Standard CARE and DARE data, equations, and conventions, finite Schur or QZ sweep budgets, an adjacent-swap budget K, a scalar/evaluator work budget W, a positive local separation threshold η, and the exact arithmetic controller or bounded outward evaluator for Finite-budget stable block reordering for Schur and QZ forms. The budget W also charges every graph-product enclosure and local acceptance comparison. The graph stage also takes finite dyadic proposals Rg,Y^ for a point inverse and solution matrix, together with outward enclosures of the exact product-factor entries and the certificate data required by the applicable local residual-ball theorem. If a proposal, enclosure, or certificate is unavailable, the corresponding graph or acceptance result is inconclusive. For CARE form H=[A−G−Q−A∗]; for DARE form N=[A0−QI] and M=[IG0A∗]. The procedure never forms A−1 and does not require a separately supplied ordered basis.

Each local residual-ball packet contains its proposed radius, residual and inverse-norm bounds, norm bounds, and the required Lyapunov or Stein witness matrices with exact factorization witnesses for positive-definite and positive-semidefinite inequalities. Check all supplied matrix equalities exactly and all scalar bounds with the finite outward evaluator. A missing witness or unresolved comparison returns inconclusive; failure of a sufficient residual-ball test alone does not reject a candidate.

  1. For CARE, run Finite-budget computed Francis Schur reduction with explicit statuses on H. For DARE, run Finite-budget QZ iteration with homogeneous status and residual output on (N,M). Propagate any budget, range, invariant-pattern, or pencil-regularity failure as an explicit inconclusive status. The returned residuals and factor backward-error certificates are those specified by the corresponding supplier items; they are not interpreted as structure-preserving perturbations.
  2. On a successful reduction, invoke Finite-budget stable block reordering for Schur and QZ forms with the CARE strict-left-half-plane selector or DARE strict-unit-disk selector and required selected dimension n. Propagate every non-ordered result as its explicit status, including boundary-spectrum, separation-inconclusive, swap-separation-inconclusive, arithmetic-inconclusive, range-failure, swap-budget-exhausted, and work-budget-exhausted. The returned exact product factors, together with Finite-budget stable block reordering has exact adjacent-swap correctness and status, certify ordering of the represented computed form and transport the original unstructured reduction residual. For CARE take the first n columns of the updated Schur factor; for DARE take the first n columns of the updated right QZ factor, never the left factor. If the relevant exact factor or residual certificate is unavailable, keep the corresponding diagnostic inconclusive.
  3. Write the ordered exact product basis as U=[U1U2] and view the supplied n×n matrix Y^ by columns y^j. Enclose the entries of Ag=U1∗ and Bg=U2∗ by finite outward rectangles. Using the supplied dyadic proposals, outward-evaluate I−RgAg once and let q be an upper bound for its Frobenius norm; the same enclosure applies to every matrix in the product of entry rectangles. If q≥1 or the enclosure is unavailable, return graph-block-inconclusive. For each column bj of Bg, outward-evaluate the full uniform residual enclosure Rg(bj−Agy^j) over the rectangles and choose a common finite upper bound r for its Euclidean norm. If any enclosure fails, return graph-block-inconclusive. Apply A uniform approximate inverse and residual enclose every linear solution to each column: the exact system AgY=Bg has a unique solution and each column is within r/(1−q) of the corresponding column of Y^. Moreover Ag and hence U1 are invertible, and ∥U1−1∥2≤∥Rg∥F/(1−q) by the Neumann bound and submultiplicativity. Return this bound as the graph-block certificate; no explicit inverse is formed.
  4. Set X0=Y^∗ and X^=(X0+X0∗)/2. Compute outward enclosures for the CARE or DARE residual, the Hermitian symmetry defect, and, for DARE, R+B∗X^B. Validate the supplied certificate packet against the hypotheses of A CARE residual and Lyapunov margin certify a unique stabilizing root in a matrix ball or A DARE residual, Stein inverse bound, and Lyapunov margin certify a stabilizing root, respectively. If the theorem certifies a unique stabilizing root in the stated ball, return the candidate, residual data, graph-block bound, stability witness and certified root ball. A direct exact witness that the candidate fails a required positivity or stability condition returns candidate-rejected; failure of a sufficient theorem test or unavailable data returns inconclusive. No residual by itself certifies the stabilizing branch or a nearby positive Q,R.

This is the finite candidate-extraction stage for the ordered Schur/QZ solvers. Its ordering prerequisite is the finite adjacent-block routine and correctness theorem cited above; a successful order applies to the represented computed form, with the separately stated diagnostics still required for Riccati acceptance.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

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=[U1U2] with U1 invertible, and set X=U2U1−1. If X=X∗, then X solves the CARE and the restriction matrix on the graph is A−GX.

For the DARE case, suppose an exact stable deflating basis for the pencil (N,M) is U=[U1U2] with U1 invertible, and set X=U2U1−1. If X=X∗ and R+B∗XB≻0, then X solves the DARE and the restriction matrix is Ac=(I+GX)−1A=A−B(R+B∗XB)−1B∗XA.

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−GX) 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]Ac for Ac=(I+GX)−1A.

[F3]

Standard CARE and DARE data, equations, and conventions: the DARE is equivalently X=Q+A∗X(I+GX)−1A whenever R+B∗XB is invertible.

Proof

1.1F1givenalgebra

In either case, U2=XU1, so U=[I;X]U1. If HU=UT in the CARE case, right multiplication by U1−1 gives H[I;X]=[I;X](U1TU1−1). The top block fixes the restriction matrix as A−GX; the bottom block reads −Q−A∗X=X(A−GX), which is exactly A∗X+XA−XGX+Q=0.

2.1F2F3algebra∎

If NU=MUT in the DARE case, the same normalization gives N[I;X]=M[I;X](U1TU1−1). The top block is A=(I+GX)(U1TU1−1), so invertibility of I+GX gives restriction matrix (I+GX)−1A. The lower block is X−Q=A∗X(I+GX)−1A, which is the DARE by [F3]. No claim survives an unverified leading-block inverse or a subsequent nonzero symmetry residual.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

DARE structure-preserving doubling converges with a quantified quadratic error envelope

Statement

Under the discrete stabilizability and detectability hypotheses of Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution, start the exact recurrence of Finite-budget structure-preserving doubling iteration for the DARE from A0=A, G0=BR−1B∗, and H0=Q. Then all inverses exist, Gj,Hj⪰0, and Hj converges to the stabilizing DARE solution X∗. More quantitatively, there are q∈(0,1), an index j0, and C>0 such that ∥Hj−X∗∥F,W−1≤Cq2j+1(j≥j0), where W≻0 is a Stein witness constructed from the closed-loop matrix. The envelope ϵj=Cq2j+1 obeys ϵj+1=ϵj2/C. The constants are conditional on the closed-loop spectral separation and its norm conditioning; no uniform constant depending only on dimension is asserted.

Facts & Assumptions

Given: The standard DARE data and the exact discrete stabilizability/detectability hypotheses.

[F1]

Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution: the finite-horizon iterates P0=0, Pk+1=f(Pk) increase to X∗, and Ac(X∗) is Schur stable.

[F2]

The DARE doubling recurrence composes two Riccati steps and preserves positive semidefiniteness: the recurrence is well-defined, preserves Gj,Hj⪰0, and Hj=f2j(0).

[F3]

Powers of a Schur-stable matrix decay geometrically up to a polynomial factor: powers of every Schur-stable matrix have a geometric bound with any rate above its spectral radius.

[F4]

A non-negative operator has a unique non-negative square root: a positive-semidefinite matrix has a positive-semidefinite square root; for W≻0 this square root is positive definite.

[F5]

Proof

1.1F1F2algebra

By [F2], Hj=P2j and Gj,Hj remain positive semidefinite. Since [F1] gives Pk→X∗, the subsequence Hj=P2j also converges to X∗. No inverse of A is used.

1.2F1F3F4algebra

Put M=Ac(X∗). By [F1], M is Schur stable; [F3] therefore makes W=∑k=0∞(M∗)kMk converge in norm. It is positive definite, W⪰I, and M∗WM=W−I. If w=∥W∥2, then v∗M∗WMv≤(1−w−1)v∗Wv, so the induced W-norm ∥M∥W:=∥W1/2MW−1/2∥2 is at most q0=1−w−1<1. Choose q with q0<q<1. Since Pk→X∗ and Ac(Pk) is continuous on Pk⪰0, choose k0 so ∥Ac(Pk)∥W≤q for all k≥k0.

2.1F1F5step 1.2algebrainduction∎

Let Ek=X∗−Pk⪰0. The Riccati-map difference identity in [F1] gives Ek+1=M∗EkAc(Pk). Define ∥E∥F,W−1=∥W−1/2EW−1/2∥F. By [F5], for k≥k0, ∥Ek+1∥F,W−1≤∥M∥W∥Ac(Pk)∥W∥Ek∥F,W−1≤q2∥Ek∥F,W−1. Iteration gives ∥Ek∥F,W−1≤∥Ek0∥F,W−1q2(k−k0). Taking k=2j and setting C=max⁡{1,∥Ek0∥F,W−1q−2k0} proves the displayed envelope for all 2j≥k0. Since C>0, direct calculation gives ϵj+1=Cq2j+2=ϵj2/C.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Separated DARE pencils have quantitatively stable deflating graphs

Statement

Let (N,M) be the order-2n DARE pencil in The stabilizing DARE solution is the stable deflating graph of a regular symplectic pencil, with n≥1. Work over C, also for real input. Suppose exact unitary matrices Q,V give an ordered complex generalized Schur pair Q∗NV=S=[S11S120S22],Q∗MV=T=[T11T120T22], where each diagonal block has order n, all four diagonal blocks are upper triangular, the leading homogeneous roots are strictly inside the unit disk, and the trailing roots are strictly outside its closure, including infinity. This ordered representation is an explicit input; existence of an unordered generalized Schur form is not an ordering certificate.

Give pairs of n×n matrices the product Frobenius norm ∥(Y,Z)∥P=(∥Y∥F2+∥Z∥F2)1/2, and define the lower-oriented generalized Sylvester separation γ=min⁡∥(Y,Z)∥P=1∥(S22Y−ZS11,T22Y−ZT11)∥P. Then γ>0. Write κ=γ−1, h=(∥S12∥22+∥T12∥22)1/2. For arbitrary pencil perturbations ΔN,ΔM, put E=Q∗ΔNV, F=Q∗ΔMV, and δ=(∥E∥F2+∥F∥F2)1/2=(∥ΔN∥F2+∥ΔM∥F2)1/2. If r>0 satisfies κ[δ+2δr+(h+δ)r2]≤r,κ[2δ+2(h+δ)r]<1, there is a unique pair (Y,Z) in the product radius-r ball for which the right and left graphs V[I;Y] and Q[I;Z] form matching deflating spaces of the perturbed pair. In particular ∥Y∥F,∥Z∥F≤r. For δ>0, a sufficient choice is r=2κδ whenever, with θ=κδ, 4θ+4κhθ+4θ2<1. For δ=0, take Y=Z=0.

Here are separate sufficient margins identifying these graphs as the stable spaces. Set a=δ+(∥S12∥2+δ)r,b=δ+(∥T12∥2+δ)r, Ks=T11−1S11,Ku=S22−1T22. The inverses exist and Ks,Ku are Schur stable. For j=s,u, choose Wj≻0 with Wj−Kj∗WjKj=I; the convergent Stein series supplies such a matrix. Require ∥T11−1∥2b<1,∥S22−1∥2a<1, and define ϵs=∥T11−1∥2(a+b∥Ks∥2)1−∥T11−1∥2b,ϵu=∥S22−1∥2(b+a∥Ku∥2)1−∥S22−1∥2a. If ∥Wj∥2(2∥Kj∥2ϵj+ϵj2)<1(j=s,u), then the perturbed pencil is regular, has precisely n stable roots and n outside roots, and the constructed right graph is its stable deflating space. For fixed ordered input these margins hold for all sufficiently small δ with r=2κδ.

For normalized right bases, write V=[U V2] and U^=(U+V2Y)(I+Y∗Y)−1/2,y=∥Y∥2,β(y)=2(1−11+y2). Then U^∗U^=I, ∥U^−U∥2=β(y)≤y≤r, and ∥(I−UU∗)U^∥2=y1+y2. If the physical top block U1 of U=[U1;U2] is invertible, X=U2U1−1, and ∥U1−1∥2β(y)<1, then U^1 is invertible and ∥U^2U^1−1−X∥2≤(1+∥X∥2)β(y)∥U1−1∥2−1−β(y). For the directly computable bound with β(r), impose the stronger margin ∥U1−1∥2β(r)<1; replacing β(y) by β(r) then gives a valid weaker estimate. An independently rotated orthonormal basis of the same perturbed space produces the identical chart, so it need not be close to U before alignment. The conclusion concerns an unstructured perturbed pencil; it does not certify Hermitian symmetry, Riccati residual, positive data, or the stabilizing Riccati branch after symmetrization.

Facts & Assumptions

Given: The regular DARE pencil and stable graph, an exact ordered complex unitary generalized Schur representation with the stated strict stable split, perturbations of both pencil matrices, the stated contraction radius, and the indicated separate stability and chart margins.

[F1]

The stabilizing DARE solution is the stable deflating graph of a regular symplectic pencil: the DARE pencil is regular, has n stable finite roots and n outside roots including infinity, and its stable right deflating space is a graph.

[F2]

Complex and real generalized Schur forms: a complex generalized Schur representation has exact unitary left/right factors and upper-triangular arrays with homogeneous scalar diagonal pairs.

[F3]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: a finite-dimensional linear map has a smallest singular value; it is positive exactly when the map is injective.

[F4]

The Frobenius norm ∥A∥F=(∑i,j∣aij∣2)1/2 on real or complex matrices: the Frobenius norm is the Euclidean norm of the matrix entry list, including for zero-sized blocks.

[F5]

Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison: unitary factors preserve Frobenius and operator norms, and ∥M∥2≤∥M∥F.

[F6]

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

[F7]

Powers of a Schur-stable matrix decay geometrically up to a polynomial factor: powers of a Schur-stable matrix decay geometrically up to a finite constant.

[F8]

Every finite-dimensional normed space is Banach: every finite-dimensional normed real or complex space is complete.

[F9]

A non-negative operator has a unique non-negative square root and [F3]: I+Y∗Y has a positive inverse square root with the singular-value formulas used below.

[F10]

The homogeneous determinant factors across a block upper triangular pencil: the homogeneous determinant factors across the diagonal blocks of a block upper-triangular pencil.

[F11]

Every finite-dimensional endomorphism over an algebraically closed field has Jordan form: each finite-dimensional complex endomorphism has a basis of generalized eigenvectors.

[F12]

A Neumann defect bounds the inverse norm: if ∥E∥2≤q<1, then I−E is invertible and ∥(I−E)−1∥2≤(1−q)−1.

[F15]

Regular matrix pencils and homogeneous generalized eigenvalues: the homogeneous roots of (N,M) are zeros of det⁡(βN−αM); β=0 represents infinity.

Proof

1.1F1F2F3F4givenconstructalgebra

By [F1], the regular base DARE pencil has an n+n stable/outside split, and the ordered representation [F2] puts the stable roots in the leading blocks and the outside roots in the trailing blocks. Write trailing diagonal pairs as (si,ti) and leading ones as (pj,qj). Disjoint homogeneous roots give pjti−siqj≠0 for every i,j, including ti=0. In the system S22Y−ZS11=C, T22Y−ZT11=D, process rows i=n,n−1,…,1 and within each row columns j=1,…,n; upper triangularity makes all other terms involve already determined Ykj with k>i or Ziℓ with ℓ<j. The two unknowns (Yij,Zij) have coefficient matrix [si−pjti−qj] with determinant pjti−siqj≠0, so the lower-oriented generalized Sylvester map is bijective. Its minimum singular value [F3] is therefore γ>0, and its inverse norm is κ=γ−1.

2.1F1F4F5F6F8step 1.1algebra

Define CY=S11+E11+(S12+E12)Y and DY=T11+F11+(T12+F12)Y. Block multiplication gives (S+E)[I;Y]=[I;Z]CY and (T+F)[I;Y]=[I;Z]DY exactly when L(Y,Z)=(S22Y−ZS11,T22Y−ZT11) equals (−E21−E22Y+ZE11+Z(S12+E12)Y, −F21−F22Y+ZF11+Z(T12+F12)Y). On the product radius-r ball, the right side has norm at most δ+2δr+(h+δ)r2: the constant pair is bounded by δ, the two linear pairs by δ∥Y∥F and δ∥Z∥F, and the quadratic pair by (h+δ)∥Z∥F∥Y∥F. Splitting the quadratic difference into its Y and Z changes bounds the Lipschitz constant by 2δ+2(h+δ)r. Applying L−1 gives a self-map and contraction under the stated inequalities; iteration from zero has geometrically summable increments, so completeness [F8] gives a limit in the closed ball, continuity gives a fixed point, and contraction gives uniqueness. For r=2κδ and θ=κδ, substitution gives self-map ratio κ[δ+2δr+(h+δ)r2]/r=1/2+2θ+2κhθ+2θ2 and contraction constant 2θ+4κhθ+4θ2; the displayed strict condition implies both. For δ=0, the exact pair Y=Z=0 solves the graph equations.

3.1F2F5F6F7F12step 2.1algebra

Set RY=[I0YI] and LZ=[I0−ZI]. They are invertible shears of determinant one, and the graph equations from step 2.1 give LZ(S+E)RY=[CYS12+E120A′] and LZ(T+F)RY=[DYT12+F120B′], where A′=S22+E22−Z(S12+E12) and B′=T22+F22−Z(T12+F12). Unitary invariance, ∥M∥2≤∥M∥F [F5], and submultiplicativity [F6] give ∥CY−S11∥2,∥A′−S22∥2≤a and ∥DY−T11∥2,∥B′−T22∥2≤b. Every leading stable root is finite, so T11 is invertible and Ks=T11−1S11 is upper triangular with diagonal moduli below one. Every trailing outside root has nonzero first homogeneous coordinate, so S22 is invertible and Ku=S22−1T22 is upper triangular with diagonal moduli below one, including zero for infinity; thus both are Schur stable. By [F7], Wj=∑k≥0(Kj∗)kKjk converges for j=s,u, is positive definite, and satisfies Wj−Kj∗WjKj=I. The two Neumann margins and [F12] make DY,A′ invertible with inverse norms at most ∥T11−1∥2/(1−∥T11−1∥2b) and ∥S22−1∥2/(1−∥S22−1∥2a). The identities DY−1CY−Ks=DY−1[(CY−S11)−(DY−T11)Ks] and A′−1B′−Ku=A′−1[(B′−T22)−(A′−S22)Ku] give exactly the stated ϵs,ϵu bounds.

3.2F3F5F9givenstep 2.1algebra

Put PY=(I+Y∗Y)−1/2. Since V=[U V2] is unitary, (U+V2Y)∗(U+V2Y)=I+Y∗Y, so U^∗U^=I and U∗U^=PY. Therefore (U^−U)∗(U^−U)=2(I−PY). The largest eigenvalue of Y∗Y is y2, so [F3], [F5], and [F9] give the exact norm ∥U^−U∥2=β(y). The scalar function g(t)=t−2(1−(1+t)−1/2) has g(0)=0 and g′(t)=1−(1+t)−3/2≥0 for t≥0, proving β(y)≤y≤r. Also (I−UU∗)U^=V2YPY, whose largest singular value is y/1+y2 by [F3] and [F5].

4.1F6F10F11F13F14F15givenstep 3.1algebra

If K is either quotient in step 3.1 and ∥H∥2≤ϵ, then W−(K+H)∗W(K+H)=I−(K∗WH+H∗WK+H∗WH). The subtracted Hermitian term has norm at most ∥W∥2(2∥K∥2ϵ+ϵ2)<1, so the left side is positive definite; an eigenvector of K+H with eigenvalue λ gives (1−∣λ∣2)v∗Wv>0, hence ∣λ∣<1. Applied to DY−1CY and A′−1B′, this makes the leading perturbed roots finite and stable, and the trailing roots outside, with zero eigenvalues of A′−1B′ representing infinity. The shears have determinant one, so [F13] preserves the homogeneous determinant under their left/right transformations; [F10] factors it across the diagonal blocks. Since DY and A′ are invertible, both diagonal pencils are regular and their product is a regular pencil with the claimed n+n root split. The regular base and perturbed determinant polynomials have finite root sets by [F14]; choose λ0∈C outside their union. Put R=(N′−λ0M′)−1M′ for N′=LZ(S+E)RY and M′=LZ(T+F)RY. Then N′−λM′=(N′−λ0M′)[I−(λ−λ0)R], so [F13] expresses the pencil determinant as a nonzero constant times det⁡(I−(λ−λ0)R). Jordan form [F11] factors the latter into ∏j(1−(λ−λ0)μj) over the eigenvalues μj of R, with algebraic multiplicity. Thus each finite root maps injectively to μ=1/(λ−λ0), and the polynomial degree is the number of nonzero μj, counted with algebraic multiplicity. Its homogeneous form is det⁡(βN′−αM′)=β2ndet⁡(N′−(α/β)M′); by [F15], its multiplicity at [1:0] is 2n minus that degree, exactly the multiplicity of the zero eigenvalue of R. The matrix R is block upper triangular with diagonal blocks (CY−λ0DY)−1DY and (A′−λ0B′)−1B′, whose spectra are disjoint because their pencil-root groups are disjoint and the projective map is injective. For a generalized eigenvector [x;y] belonging to a leading-block eigenvalue μ, its trailing equation is (R22−μI)ky=0; disjoint spectra force y=0. Conversely, Jordan form [F11] supplies a basis of generalized eigenvectors of the leading n×n block, which embed as [x;0] and span exactly the full leading-root generalized eigenspace. Undoing the graph shears and unitary factors identifies this right subspace with V[I;Y] and its matching left deflating graph with Q[I;Z].

4.2F5F6F12step 3.2algebra

Write ΔU=U^−U. Under the strict chart margin, U^1=U1(I+U1−1ΔU1) and ∥U1−1ΔU1∥2≤∥U1−1∥2β(y)<1. By [F12], U^1 is invertible and ∥U^1−1∥2≤(∥U1−1∥2−1−β(y))−1. Using U2=XU1 gives U^2U^1−1−X=(ΔU2−XΔU1)U^1−1; [F6] yields the stated chart estimate. Since β is increasing and β(y)≤β(r), the stronger margin ∥U1−1∥2β(r)<1 gives the computable weaker bound. An independently rotated orthonormal basis of the same space is U^R0 for unitary R0 and has the same chart because (U^1R0)−1=R0−1U^1−1. The proof assumes no structure on E,F, so it gives no Riccati residual, symmetry, positivity, or post-symmetrization stability certificate.

5.1givenstep 2.1step 3.1step 4.1algebra∎

As δ→0 with r=2κδ, θ→0, a,b→0, and ϵs,ϵu→0; hence the contraction, Neumann, and both Stein margins in the Statement hold for all sufficiently small δ. If U1 is invertible, also ∥U1−1∥2β(r)<1 for all sufficiently small δ, so the computable chart margin holds.

No arbitrary Axiom of Choice is used: all constructions are finite-dimensional scans, norm-convergent series, or selections from complements of finite subsets of C.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

Finite Riccati candidate, Newton-Kleinman, and doubling wrappers return a status

Statement

Use admitted inputs and the finite solver/arithmetic/evaluator controllers stipulated by each of Finite-budget CARE and DARE candidate extraction from ordered Schur and QZ forms, Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration, and Finite-budget structure-preserving doubling iteration for the DARE. Then each procedure terminates with its declared output or status, retaining its specified failure diagnostics.

Candidate extraction makes one matching Schur or QZ reduction, at most one stable-block reordering call, and at most n graph-column certificate passes followed by finite acceptance checks. Exact Newton–Kleinman makes at most N policy evaluations; its safeguarded mode inspects at most N(L+1) trial gains and makes at most N point-certificate calls for the current cost matrices. SDA makes at most N solve/update passes, at most nN point-certificate calls for recurrence solves, and at most m(N+1) calls for residual solves (R∈Fm×m), followed by finite symmetry/residual reporting. Early failures may shorten these counts. These conclusions are conditional on the declared finite controller contracts; they do not derive termination of an unspecified certificate-producing routine from an enclosure theorem.

Successful ordering concerns the represented computed form. The original Riccati residual, symmetry, positivity and closed-loop checks remain separate. This finite-status result asserts no convergence for arbitrary inexact proposals and no rounded PSD or structured-backward-error guarantee.

Facts & Assumptions

Given: The three procedures' admitted finite matrix data, their finite Schur/QZ, reordering, outer-iteration and line-search budgets, and exactly the finite solver/verifier interfaces supplied in their Definitions.

[A1]

For candidate extraction, every supplied arithmetic/evaluator controller has the finite execution and explicit failure behavior declared in its Definition. For Newton–Kleinman the finite line-search controller and each point-certificate call return their result or status; for SDA each point certificate, exact factorization, and arithmetic operation returns its result or failure in finite work. These are the existing operational hypotheses, not inferred root-finding or precision-success guarantees.

[F1]

Finite-budget CARE and DARE candidate extraction from ordered Schur and QZ forms calls its matching reduction, then stable-block reordering, then its finite verified graph solve and outward acceptance diagnostics.

[F3]

Finite-budget stable block reordering has exact adjacent-swap correctness and status proves finite status return, selected invariant/right-deflating subspace on an ordered return, and transport of the original unstructured reduction residual.

[F4]

A uniform approximate inverse and residual enclose every linear solution and Verified point and uniform linear residual certificate data supply the interpretation of usable verified linear-solve and inverse/residual data. Outward-rounded operations are inclusion-isotone and enclose DAG evaluations gives enclosure soundness for finite DAG evaluations.

[F5]

Certified QZ residuals give a backward error bound for both pencil matrices concerns the specified nearby unstructured pencil, not a structured Riccati perturbation.

[F6]

Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration has at most N outer updates, at most L+1 safeguarded trials per pass, and at most one current-cost point-certificate call per pass. Finite precision point linear solve certificate with explicit status has a finite status, and The point linear solve certifier returns a sound solution ball on success gives the solution ball on a certified return. Finite Bartels–Stewart statuses and successful-pivot uniqueness proves finite policy-solve status return and uniqueness on successful exact solves.

[F7]

Finite-budget structure-preserving doubling iteration for the DARE uses exact elimination for recurrence and residual solves in exact mode. Finite mode uses at most n point-certificate calls per recurrence solve and at most m calls for each residual diagnostic at initialization and after each update, since R+B∗HjB has order m. An unavailable residual does not change recurrence status. The point solver has finite status by [F6]. The residual/feedback conventions are Standard CARE and DARE data, equations, and conventions.

Proof

1.1givenA1F1F2algebra

Each candidate-extraction branch calls only its matching finite Schur or QZ routine. The finite controls and declared status behavior are covered by [F1]–[F2]. Any reduction, regularity, range or budget failure immediately propagates its inconclusive status; no convergence-until-success loop is present.

1.2givenA1F6algebra

Exact Newton–Kleinman performs at most N policy evaluations. Each admitted Bartels–Stewart call has the complete per-pass control packet and returns a finite success or failure status by [F6]; failure stops immediately and success is followed by one finite gain update. Hence exact mode returns within its declared outer budget.

1.3A1F4F6algebra

Each safeguarded outer pass clears finitely many positive integer denominators from the rational current-cost system, preserving its solution while making the stored point-call data dyadic, or returns range-failure. It inspects the finite list of L+1 gains and makes one current-cost point-certificate call. Each trial then uses finitely many outward operations to verify its inverse, residual and stability bounds. By [A1] each call and outward check returns its enclosure or status in finite work, with certified balls interpreted by [F4] and [F6]. A trial passes the certified acceptance inequality or is rejected; if no trial passes, the routine returns safeguard-inconclusive without changing the current gain. At most N outer passes therefore make at most N(L+1) trial inspections and N point-certificate calls. No assertion of convergence for arbitrary inexact proposals follows from this finite search.

1.4givenA1F6F7algebra

Each SDA pass j<N requests one solve with I+GjHj and, in finite mode, at most n point-certificate calls for its columns. The finite-mode initialization solves the order-m system RV=B∗ on finite dyadic encodings by finite exact rational elimination, forms BV,C∗C, and rounds finitely many components or returns its declared failure; it makes no point-certificate call. At initialization and after each update, form Sj=R+B∗HjB exactly. In exact mode its possibly non-dyadic entries are handled by the finite exact elimination rule, as are the recurrence solves; the residual is then evaluated exactly. In finite mode Sj is dyadic, so its order-m residual solve uses at most m point-certificate calls followed by outward residual evaluation. By [A1] and [F6] all these operations return a result or failure in finite work. An unavailable residual is reported without changing recurrence status. Failure of the recurrence solve immediately returns its declared range/inverse status; success is followed by the fixed finite matrix updates. Thus every pass and final report terminate.

2.1A1F1F3F4F5step 1.1algebra

On successful reduction, reordering inspects finitely many blocks and returns ordered or an explicit status by [F3]. On an ordered return its first required factor columns are the selected subspace of the represented computed form, with only the original unstructured residual certificate transported. Under [A1] the graph-block bound and verified solve [F4] terminate; missing invertibility or a failed solve takes the stated inconclusive branch. Residual, symmetry, positivity and closed-loop diagnostics use finitely many matrix/enclosure operations, and failure or unavailable evidence takes its explicit return. The enclosure interpretation in [F4] does not itself produce a terminating verifier; that is the supplied contract [A1]. The QZ diagnostic retains precisely the limitation in [F5]. Thus the wrapper returns in finite work with ordering and equation-level acceptance kept separate.

3.1A1F7step 2.1step 1.2step 1.3step 1.4algebra∎

There are at most N such passes. The final symmetry defects and, when its solve is available, the standard DARE residual use finite-dimensional arithmetic under [A1] and the conventions [F7]. Therefore the exact and finite-arithmetic paths return their declared output/status by the cap. The recorded raw matrices and defects supply no rounded PSD or structured-backward-error claim without separate checks, just as the candidate and safeguarded branches retain their original acceptance restrictions.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

Dense Riccati work counts and numerical acceptance require equation-level diagnostics

Statement

In the dense arithmetic model, a single-matrix Schur reduction or regular-pair QZ reduction of order n with at most s Francis/QZ sweeps has core work O(n3+sn2): the initial Hessenberg or Hessenberg-triangular reduction costs O(n3) and each full bulge-chasing sweep costs O(n2). Forming a graph candidate by solving XU1=U2 with dense n×n factorization, n right-hand sides, and residual multiplication costs O(n3).

After an order-d reduction, finite stable-block reordering with k actual attempts costs O(d2+kd) scalar operations. If the form has b diagonal blocks and I complementary-before-selected inversions, then I≤b(b−1)/2; successful ordering requires K≥I and enough scalar/evaluator budget W for the entire execution, including validation, label and inversion scans, all I swaps, and the final ordering scan. For a Riccati pencil or Hamiltonian with d=2n, successful reordering, graph solve and equation-level residual multiplication preserve the O(n3+sn2) scalar-core bound. This exact postprocessing count excludes algebraic bit cost, evaluator implementation cost beyond its declared unit budget, dense product-factor evaluation, local residual-ball certificate production or validation beyond the charged dense operations, and any additional dense residual multiplication. It is not a fixed-precision floating-point flop or structured backward-stability bound.

One dense Bartels–Stewart Lyapunov solve in its specified cubic branch costs O(n3); J exact Newton-Kleinman policy evaluations therefore cost O(m3+Jn3+J(n2m+nm2)) for state dimension n and input dimension m, charging one factorization of R of order m once. One exact-arithmetic SDA recurrence step costs O(n3), so N exact steps cost O(Nn3); finite point-certificate and residual-enclosure work is separate.

Every computed candidate still requires its actual CARE/DARE residual and Hermitian symmetry defect. A DARE candidate also requires a positive lower bound for R+B∗XB; both equations require an independently certified closed-loop Hurwitz/Schur condition before the stabilizing branch is accepted. A computed QZ backward error for an unstructured nearby pencil does not certify nearby Hamiltonian/symplectic structure or positive Q,R.

Facts & Assumptions

Given: Dense scalar arithmetic, finite Schur/QZ sweep budgets, dense direct factors and solves, and exact matrix dimensions.

[F1]

Finite-budget CARE and DARE candidate extraction from ordered Schur and QZ forms: candidate extraction calls finite Schur/QZ reductions and exact stable-block reordering, solves XU1=U2, and reports actual Riccati residual, symmetry defect, positivity, and closed-loop stability data.

[F2]

Finite-budget computed Francis Schur reduction with explicit statuses: Francis reduction first reduces to Hessenberg form and then performs bounded QR bulge-chasing sweeps.

[F3]

Finite-budget QZ iteration with homogeneous status and residual output: QZ iteration first reduces a regular pair to Hessenberg-triangular form and then performs bounded QZ sweeps.

[F4]

Finite-budget Bartels-Stewart solve for a Sylvester equation: its cubic branch sets NA≤c0m and NB≤c0n for the two Schur reductions, then solves the resulting triangular Sylvester equation.

[F5]

Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration: each exact Newton-Kleinman update performs one Lyapunov solve and one gain update.

[F6]

Finite-budget structure-preserving doubling iteration for the DARE: each SDA update solves with I+GjHj and forms three dense matrix updates.

[F7]

Certified QZ residuals give a backward error bound for both pencil matrices: the QZ backward-error statement certifies the computed pair against an unstructured nearby pencil.

[F8]

Standard CARE and DARE data, equations, and conventions: the acceptance quantities are the CARE/DARE residuals, symmetry, DARE matrix R+B∗XB, and the corresponding closed-loop matrices.

[F9]

Finite-budget stable block reordering for Schur and QZ forms: the exact reordering has initial form-validation work, bounded-size local solves, whole-panel updates, and separate finite K,W budgets.

[F10]

Finite-budget stable block reordering has exact adjacent-swap correctness and status: each accepted adjacent inversion swap reduces the count by one and the exact factors transport existing unstructured residual norms.

[F11]

Finite Bartels–Stewart statuses and successful-pivot uniqueness: the admitted finite solve terminates with a declared status and every successful local pivot is unique.

[A1]

Dense reductions and exact equation solves use classical dense multiplication, factorization, and triangular solve costs. Reordering counts exact scalar primitives and declared evaluator units; algebraic bit cost, evaluator implementation cost, factor evaluation, local residual-ball verifier work, and any uncounted enclosure work remain separate.

Proof

1.1A1F2F3givenalgebra

In a Householder Hessenberg reduction, there are at most n reflectors. At each stage a reflector updates a trailing block with at most n2 entries using matrix-vector and rank-one operations, so the initialization costs O(n3). In a Francis or QZ bulge-chasing sweep, there are O(n) rotations/reflections; each is applied to O(n) entries in the active matrix and accumulated factor, hence a sweep costs O(n2). The finite budgets in [F2]–[F3] therefore give O(n3+sn2) core work.

2.1A1F1F4F11step 1.1algebra

Dense LU factorization of U1 costs O(n3); applying its factors to n right-hand sides costs O(n3). The residual product (XU1−U2) is also O(n3), yielding the candidate solve count in [F1]. In the Lyapunov branch, [F4] imposes NA,NB≤c0n. By step 1.1, each of its two dense Schur reductions therefore costs O(n3); exact certificate checks and factor transformations are also O(n3). Triangular substitution for n2 unknown entries with O(n) work per entry costs O(n3), so one solve in this cubic branch costs O(n3). The fixed controller is bounded there; arbitrary-terminating-controller work is separate.

3.1A1F1F9F10step 1.1step 2.1algebra

Let d be the reduction order, b its diagonal block count and I its initial inversion count. The reordering validation scan costs O(d2). Each local system has order at most eight, and each exact factor update touches O(d) panel entries, so k attempts cost O(d2+kd) by [F9]. On success, [F10] gives k=I≤b(b−1)/2≤d(d−1)/2, so the worst-case reordering core is O(d3); this success path also requires K≥I and sufficient W for the entire execution through its final ordering scan. For a Riccati matrix of order 2n, combining reduction, reordering, graph solve and dense equation residual multiplication preserves O(n3+sn2) scalar-core work. Exact algebraic bit cost, evaluator implementation, dense factor-product evaluation and any additional dense residual multiplication are separate costs.

3.2A1F5F6step 2.1algebra

Each exact Newton-Kleinman pass has one Bartels–Stewart solve by [F5], costing O(n3) by step 2.1. Factorizing R once costs O(m3). With m controls, forming B∗X and the gain uses O(n2m+m2n) arithmetic including triangular solves with this pre-factored R; forming K∗RK and A−BK is bounded by the same O(n2m+nm2) term. Summing over J passes gives O(m3+Jn3+J(n2m+nm2)). Each exact-arithmetic SDA recurrence step uses one dense n×n solve and a fixed number of dense products, each O(n3); [F6] therefore gives O(Nn3) over N exact steps. Finite point-certificate and residual-enclosure work is separate under [A1].

4.1F1F7F8givenalgebra∎

A small backward error for a computed QZ pair, as supplied by [F7], is a statement about an unstructured nearby pencil. It contains no premise that the perturbation preserves Hamiltonian or symplectic block relations, nor that it preserves positive definiteness of Q or R. Consequently acceptance must separately compute the equation residual and symmetry defect, check R+B∗XB≻0 for DARE, and certify the closed-loop stability property in [F8]; [F1] explicitly reports these quantities. Neither ordering a computed form nor its unstructured backward error establishes a structured pencil perturbation or an equation-level stabilizing certificate.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Riccati residual sensitivity and invariant graph conditioning retain spectral separation

Statement

Let Xc and Xd be the stabilizing CARE and DARE solutions under the hypotheses of Stabilizability and detectability give the unique stabilizing positive-semidefinite CARE solution and Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution. Their residual derivatives on Hermitian matrices are Lc(E)=Ac(Xc)∗E+EAc(Xc),Ld(E)=Ac(Xd)∗EAc(Xd)−E. When invertible, the local residual condition numbers are κc=∥Lc−1∥F→F and κd=∥Ld−1∥F→F. If additive Hermitian residual perturbations admit radii satisfying the contraction and separate stability-margin hypotheses of A CARE residual and Lyapunov margin certify a unique stabilizing root in a matrix ball or A DARE residual, Stein inverse bound, and Lyapunov margin certify a stabilizing root, the perturbed equations have stabilizing roots within those radii; the linear leading sensitivity is −Lc−1Δ or −Ld−1Δ.

For CARE, write TX=[I0XcI] and let σ=sep⁡(−Ac(Xc)∗,Ac(Xc))>0, with κs=1/σ. For a Hamiltonian perturbation ΔH, put Z=TX−1ΔHTX, ζ=∥Z∥F, θ=κsζ, and μ=κs∥G∥2. If 6θ+4μθ+4θ2<1, the perturbed Hamiltonian has an invariant graph Ran⁡[I;Xc+Y] with ∥Y∥F≤2θ. If its restriction is certified Hurwitz and the perturbed Hamiltonian is certified to have exactly n left-half-plane eigenvalues, this graph is its stable subspace.

Finally, for either an exact CARE invariant graph basis or DARE deflating graph basis U=[U1;U2] with invertible U1, let X=U2U1−1 and let U~=U+ΔU. If ∥U1−1∥2∥ΔU1∥2<1, then U~1 remains invertible and ∥U~2U~1−1−X∥2≤∥ΔU2∥2+∥X∥2∥ΔU1∥2∥U1−1∥2−1−∥ΔU1∥2. This basis-chart estimate does not by itself certify a perturbed QZ deflating subspace.

For the DARE pencil, Separated DARE pencils have quantitatively stable deflating graphs gives a separate perturbation-to-stable-deflating-space estimate from a generalized Sylvester separation, explicit contraction inequalities, and distinct leading/trailing Stein margins. Under those conditions its aligned orthonormal stable basis changes by at most β(r)≤r. The computable physical chart estimate additionally requires ∥U1−1∥2β(r)<1; without that margin the chart remains inconclusive. A QZ pencil backward-error bound alone supplies none of these conditions.

Facts & Assumptions

Given: Standard CARE/DARE data, their stabilizing solutions and graph representations, and the indicated residual or basis perturbation bounds.

[F1]

Stabilizability and detectability give the unique stabilizing positive-semidefinite CARE solution: the CARE has a unique Hermitian positive-semidefinite solution whose closed loop is Hurwitz.

[F2]

Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution: the DARE has a unique Hermitian positive-semidefinite solution whose closed loop is Schur stable.

[F3]

Standard CARE and DARE data, equations, and conventions: Fc(X)=A∗X+XA−XGX+Q and Fd(X)=Q+A∗X(I+GX)−1A−X on their stated domains.

[F4]

The stabilizing CARE solution is the Hamiltonian stable invariant graph: H[I;Xc]=[I;Xc]Ac(Xc).

[F5]

The stabilizing DARE solution is the stable deflating graph of a regular symplectic pencil: N[I;Xd]=M[I;Xd]Ac(Xd) for the stated homogeneous DARE pencil.

[F6]

Sylvester operator and Frobenius separation number: sep⁡(P,−Q) is the smallest singular value of Y↦PY+YQ in Frobenius norm.

[F7]

A CARE residual and Lyapunov margin certify a unique stabilizing root in a matrix ball: CARE residual radius conditions are κ(r+gρ2)≤ρ and 2κgρ<1, with a separate Lyapunov stability margin.

[F8]

A DARE residual, Stein inverse bound, and Lyapunov margin certify a stabilizing root: DARE residual radius conditions use κ(r+LDρ2/2)≤ρ and κLDρ<1, with a separate Stein stability margin.

[F9]

A Sylvester equation is uniquely solvable exactly when the spectra are disjoint: Y↦PY+YQ is invertible when σ(P)∩[−σ(Q)]=∅.

[F10]

Every finite-dimensional normed space is Banach: finite-dimensional Frobenius matrix spaces are complete.

[F11]

Powers of a Schur-stable matrix decay geometrically up to a polynomial factor: powers of a Schur-stable matrix decay geometrically, so the Stein series in the proof converges.

[F12]

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

[F13]

The Hurwitz Lyapunov integral is the unique solution and has the stated positivity: for a Hurwitz matrix, the Lyapunov integral with positive-definite forcing is positive definite and solves the associated Lyapunov equation.

[F14]

Separated DARE pencils have quantitatively stable deflating graphs: generalized Sylvester separation, paired-graph contraction, separate leading and reciprocal-trailing Stein margins, and normalized basis/chart estimates bound the perturbed DARE stable deflating graph, including infinite roots.

[A1]

Residual perturbations are Hermitian and the verified norm and stability bounds in the applicable radius certificate enclose their exact values.

[A2]

For the CARE subspace part, the perturbed stable eigenvalue count and the Hurwitz property of the restriction are supplied as verified inputs when stable-subspace identity is asserted.

Proof

1.1F3givenalgebra

By [F3], expanding the CARE polynomial at a Hermitian X gives Fc(X+E)−Fc(X)=LcX(E)−EGE, where LcX(E)=(A−GX)∗E+E(A−GX). For the DARE, set f(X)=Q+A∗X(I+GX)−1A. Direct multiplication gives ΦG(X+E)−ΦG(X)=(I+(X+E)G)−1E(I+GX)−1,ΦG(X)=X(I+GX)−1. Taking the derivative at E=0 and multiplying by A∗,A gives Df(X)[E]=Ac(X)∗EAc(X); since Fd=f−X, this gives DFd(X)[E]=Ac(X)∗EAc(X)−E.

1.2F14given

Apply [F14] to the exact ordered unitary DARE pencil representation and the supplied perturbations of both pencil matrices. Its paired generalized Sylvester operator and contraction inequalities give the radius-r right and left deflating graphs; its separate Neumann and Stein margins establish the perturbed stable split. Its normalized basis construction gives distance at most β(r)≤r, and its computable physical chart estimate retains the inverse graph-block norm and the strict margin ∥U1−1∥2β(r)<1. No part of this conclusion follows from QZ backward error alone.

2.1A1F1F2F7F8F10F11F12F13step 1.1algebra

For a CARE additive residual perturbation Δ, write X=Xc+E and let δ=∥Δ∥F. Then Fc(Xc)=0 and step 1.1 makes the perturbed root equation equivalent to E=−Lc−1Δ+Lc−1(EGE). If ρ satisfies κc(δ+∥G∥2ρ2)≤ρ and 2κc∥G∥2ρ<1, the map sends the closed radius-ρ Hermitian ball to itself and has Lipschitz constant at most the second displayed quantity. Iteration from zero gives geometric successive differences; [F10] gives a limit in the ball, continuity gives a fixed point, and contraction gives uniqueness. Let Wc=∫0∞etAc∗etAc dt≻0; then Ac∗Wc+WcAc=−I. If also 2∥Wc∥2∥G∥2ρ<1, then ∥EGWc+WcGE∥2≤2∥Wc∥2∥G∥2ρ<1. Hence (Ac−GE)∗Wc+Wc(Ac−GE)≺0; an eigenvector v with eigenvalue λ gives 2Re⁡(λ)v∗Wcv<0, so the perturbed loop is Hurwitz. For DARE, [F2] gives Schur stability and [F11] gives the Stein inverse Ld−1(Y)=−∑k≥0(Ac∗)kYAck. On a sufficiently small ball, S(X)=R+B∗XB⪰δSI, where δS=λmin⁡S(Xd)−b2ρ>0. Put a=∥A∥2, b=∥B∥2, and m=∥Xd∥F+ρ. The resolvent identity gives ∥S(X)−1∥2≤δS−1 and ∥S(X)−1−S(Y)−1∥2≤b2δS−2∥X−Y∥F. Splitting K(X)−K(Y) into its X and inverse-factor changes yields ∥K(X)−K(Y)∥F≤LK∥X−Y∥F, where LK=ab/δS+ab3m/δS2; hence ∥Ac(X)∥2≤Mc=a+ab2m/δS and ∥Ac(X)−Ac(Y)∥2≤Lc∥X−Y∥F, Lc=bLK. Since DFd(X)[E]=Ac(X)∗EAc(X)−E, subtraction gives ∥DFd(X)−DFd(Y)∥F→F≤2McLc∥X−Y∥F=:LD∥X−Y∥F. Integrating this derivative along line segments gives R(E)=Fd(Xd+E)−Fd(Xd)−Ld(E) with ∥R(E)∥F≤LD∥E∥F2/2 and ∥R(E)−R(F)∥F≤LDρ∥E−F∥F on the ball. Thus E=−Ld−1(Δ+R(E)) is a self-map when κd(δ+LDρ2/2)≤ρ and a contraction when κdLDρ<1. The same completeness argument gives its unique local root. For a separate stability margin, take Wd=∑k≥0(Ac∗)kAck≻0, so Wd−Ac∗WdAc=I by [F11]. Put η=Lcρ. Expanding the Stein form bounds its change by ∥Wd∥2(2Mcη+η2); choose ρ so this is below 1. Then Wd−Ac(X)∗WdAc(X)≻0, and an eigenvector gives (1−∣λ∣2)v∗Wdv>0, so the perturbed loop is Schur stable. For sufficiently small δ>0, take ρ=2κcδ in CARE when ∥G∥2>0; the contraction and stability inequalities hold for small enough δ, giving ∥E∥F=O(δ). If G=0, the equation is linear and this order bound is exact. In DARE, take ρ=2κdδ when LD>0; for sufficiently small δ this satisfies the self-map, contraction, S(X)≻0, and Stein-margin bounds, again giving ∥E∥F=O(δ). If LD=0, the local equation is linear. The remainders are therefore O(δ2), proving the first-order terms −Lc−1Δ and −Ld−1Δ.

2.2A2F3F4F6F9F10F12step 1.1algebra

Put TX=[I 0;Xc I]. Multiplying the Hamiltonian in [F4] on the right by TX and then on the left by TX−1=[I 0;−Xc I], and using the CARE identity in [F3], gives TX−1HTX=[Ac−G0−Ac∗]. The Sylvester map S(Y)=−Ac∗Y−YAc has smallest singular value σ=sep⁡(−Ac∗,Ac)>0: [F9] applies because σ(−Ac∗) lies in the right half-plane while −σ(−Ac)=σ(Ac) lies in the left half-plane; [F6] gives inverse norm κs=1/σ. In the perturbed coordinates, write Z=[Zij] and seek an invariant graph [I;Y]. Its lower-block graph equation is −Ac∗Y−YAc+Z21+Z22Y−YZ11+YGY−YZ12Y=0. Hence Y is a fixed point of T(Y)=−S−1(Z21+Z22Y−YZ11+YGY−YZ12Y). On the Frobenius ball ∥Y∥F≤2θ, each block norm of Z is at most ζ. The map norm is at most κs[ζ+2ζ∥Y∥F+(∥G∥2+ζ)∥Y∥F2], hence at most θ+4θ2+4μθ2+4θ3≤2θ under the displayed smallness condition. Its Lipschitz constant is at most 2θ+4μθ+4θ2<1. Completeness [F10] and iteration therefore give a unique fixed point in the ball. Returning through TX turns [I;Y] into [I;Xc+Y], proving the graph bound. Under [A2], the restriction has n stable eigenvalues and the perturbed matrix has exactly n stable eigenvalues in total. In a basis beginning with this invariant graph, the perturbed matrix is block upper triangular with this stable restriction as its first diagonal block; the quotient block therefore has no stable eigenvalues. A stable generalized eigenvector must project to a stable generalized eigenvector of the quotient, which is impossible, so every stable generalized eigenspace lies in the graph. Both spaces have dimension n, hence the graph is the stable spectral subspace.

3.1F4F5F12givenalgebra∎

Since U~1=U1+ΔU1=U1(I+U1−1ΔU1) and ∥U1−1ΔU1∥2<1, the Neumann geometric series makes the second factor invertible and gives ∥U~1−1∥2≤(∥U1−1∥2−1−∥ΔU1∥2)−1. Using U2=XU1, U~2U~1−1−X=(ΔU2−XΔU1)U~1−1. Submultiplicativity [F12] proves the displayed basis-chart bound. This derivation uses only the graph equation, so it applies to both the CARE invariant graph and the DARE deflating graph; it does not convert a pencil backward error into a deflating-subspace error.

5 · Examples, counterexamples and false statements

None yet.

Sources