LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-29

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.

Linear matrix ODEs have unique global solutions on a fixed interval

Statement

Let $I = [a, b] \subseteq R$ be a compact interval, let $C : I \to M_{n} (R)$ be continuous, let $t_{0} \in I$ , and let $Y_{0} \in M_{n} (R)$ . Then the linear matrix initial value problem

$Y^{'} (t) = C (t) Y (t), Y (t_{0}) = Y_{0},$

has a unique solution on all of $I$ .

Facts & Assumptions

Given: The compact interval $I = [a, b]$ , the continuous matrix field $C : I \to M_{n} (R)$ , the time $t_{0} \in I$ , and the initial matrix $Y_{0}$ .

[F1]

Picard-Lindelof gives a unique local solution for a continuous state-Lipschitz first-order system on an open domain (Picard-Lindelöf local existence and uniqueness for first-order systems).

[F2]

A solution of a first-order system is equivalent to a solution of the associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).

[L1]

A solution whose graph approaches a compact interior region at a finite endpoint extends past that endpoint (A solution whose graph approaches a compact interior region at a finite endpoint extends past that endpoint).

[L2]

A continuous real-valued function on a nonempty compact metric space attains its maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[L3]

The norm of a vector-valued integral is at most the integral of the norm (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable).

[L4]

Gronwall's integral inequality converts $u (t) \leq A + \int_{t_{0}}^{t} m (s) u (s) d s$ into an exponential bound (Gronwall's integral inequality with variable and constant coefficients).

Proof

technique · direct

1.1

Extend $C$ continuously to the open interval $(a - 1, b + 1)$ by setting $\tilde{C} (t) : = C (a)$ for $t < a$ , $\tilde{C} (t) : = C (t)$ for $t \in I$ , and $\tilde{C} (t) : = C (b)$ for $t > b$ . Regard $M_{n} (R)$ as $R^{n^{2}}$ . Then the right-hand side $\tilde{F} (t, Y) : = \tilde{C} (t) Y$ is continuous on the open domain $(a - 1, b + 1) \times R^{n^{2}}$ and is globally Lipschitz in $Y$ on every compact time interval, because $∥ \tilde{C} (t) (Y - Z) ∥_{2} \leq ∥ \tilde{C} (t) ∥ ∥ Y - Z ∥_{2}$ . Hence [F1] gives a unique local solution through $(t_{0}, Y_{0})$ .

F1givenconstruct

2.1

Let $J = (α, β)$ be the maximal interval of existence of that solution in $(a - 1, b + 1)$ . Since $C$ is continuous on compact $I$ , [L2] supplies a bound $∥ C (t) ∥ \leq M$ on all of $I$ . For $t \in J \cap [t_{0}, b]$ , the Volterra equation from [F2] and the norm estimate [L3] give the forward inequality below.

F2L2L3L4step 1.1

$∥ Y (t) ∥_{2} \leq ∥ Y_{0} ∥_{2} + M \int_{t_{0}}^{t} ∥ Y (s) ∥_{2} d s .$

Therefore [L4] yields $∥ Y (t) ∥_{2} \leq ∥ Y_{0} ∥_{2} e^{M (t - t_{0})}$ on $J \cap [t_{0}, b]$ .

2.2

For $t \in J \cap [a, t_{0}]$ , the oriented Volterra equation gives $Y (t) = Y_{0} - \int_{t}^{t_{0}} C (s) Y (s) d s$ , so [L3] gives the reflected inequality below.

F2L2L3L4step 1.1

$∥ Y (t) ∥_{2} \leq ∥ Y_{0} ∥_{2} + M \int_{t}^{t_{0}} ∥ Y (s) ∥_{2} d s .$

The time-reflected part of [L4] therefore yields $∥ Y (t) ∥_{2} \leq ∥ Y_{0} ∥_{2} e^{M (t_{0} - t)}$ on $J \cap [a, t_{0}]$ .

3.1

Put $R : = ∥ Y_{0} ∥_{2} e^{M (b - a)}$ . If $β \leq b$ , then every sequence $t_{j} ↑ β$ in $J$ has graph points in the compact set $[a, b] \times \overline{B} (0, R) \subseteq (a - 1, b + 1) \times M_{n} (R)$ by steps 2.1 and 2.2. So [L1] extends the solution past $β$ , contradicting maximality. The same argument at the left endpoint rules out $α \geq a$ . Therefore $I \subseteq J$ , and the restriction of the maximal solution to $I$ is defined on all of $I$ .

L1step 2.1step 2.2

4.1

Step 3.1 gives existence on all of $I$ , and uniqueness is the local uniqueness already supplied by [F1].

F1step 1.1step 3.1∎

Depends on

Used by

A linear system and its fundamental matrix Example
A fundamental matrix is invertible Proposition
C¹ dependence of solutions on initial data Theorem
Smooth dependence of solutions on initial data Theorem

Dependency tree · two levels

68 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

Nigel Hitchin, Differentiable Manifolds, Appendix §10.3, Lemma 10.6 (standard reference, not scraped)
Chin-Lung Wang, Banach Calculus, §4.4 (standard reference, not scraped)