ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Exact Newton-Kleinman decreases the cost while an unchecked inexact step can lose stability

Example

Take scalar CARE data $A = B = C = R = 1$ and the stabilizing starting gain $K_{0} = 2$ .

Facts & Assumptions

Given: The data above and the exact/inexact iteration conventions of Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration and Verified Lyapunov residual, descent, and stability checks make an inexact Newton-Kleinman step safe.

[F1]

Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration: exact mode solves $(A - B K_{j})^{*} X_{j} + X_{j} (A - B K_{j}) = - (Q + K_{j}^{*} R K_{j})$ and then sets $K_{j + 1} = R^{- 1} B^{*} X_{j}$ .

[F2]

Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration: inexact line-search trials are $K_{j} + θ_{ℓ} ({\tilde{K}}_{j} - K_{j})$ for the finite list $θ_{ℓ} = 2^{- ℓ}$ .

[F3]

Verified Lyapunov residual, descent, and stability checks make an inexact Newton-Kleinman step safe: an accepted inexact trial must have a certified Hurwitz closed loop and an exact cost matrix no greater than the current one.

Proof

1.1F1givenalgebra

At $K_{0} = 2$ , the closed loop is $- 1$ and the exact Lyapunov equation gives $- 2 X_{0} + 5 = 0$ , hence $X_{0} = 5 / 2$ and $K_{1} = 5 / 2$ . The next closed loop is $- 3 / 2$ , and its policy equation gives $- 3 X_{1} + 1 + 25 / 4 = 0$ , hence $X_{1} = 29 / 12 < 5 / 2$ .

2.1F2F3step 1.1algebra∎

Consider instead an unchecked approximate policy value $\tilde{P} = 0$ , which proposes $\tilde{K} = 0$ . A full step gives closed loop $A - B \tilde{K} = 1$ , which is unstable. More generally, a line-search trial between $K_{0} = 2$ and $0$ has $K \in [0, 2]$ . If $K \leq 1$ its closed loop $1 - K$ is not Hurwitz. If $1 < K < 2$ , its exact cost matrix is $P (K) = (1 + K^{2}) / (2 (K - 1))$ , and $P (K) - \frac{5}{2} = \frac{(K - 2) (K - 3)}{2 (K - 1)} > 0.$ Thus every nonzero trial either loses stability or increases cost; the certified safeguard rejects it.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

Sources

Peter Benner and Lihong Feng, Model Reduction for Dynamical Systems, Lecture 8 (standard reference, not scraped)