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

A fundamental matrix is invertible

Statement

Let $A : I \to M_{n} (R)$ solve the variational equation

$A^{'} (t) = C (t) A (t), A (t_{0}) = I_{n},$

on an interval $I$ , where $C : I \to M_{n} (R)$ is continuous. Then every matrix $A (t)$ is invertible. Equivalently, a fundamental matrix of the variational equation is invertible at every time on its interval of definition.

Facts & Assumptions

Given: A continuous matrix field $C : I \to M_{n} (R)$ and a solution $A : I \to M_{n} (R)$ of $A^{'} = C A$ , $A (t_{0}) = I_{n}$ .

[F1]

The variational equation is exactly a linear matrix ODE with initial matrix $I_{n}$ (The variational equation along an ODE solution).

[L1]

Linear matrix ODEs on a compact interval have unique solutions (Linear matrix ODEs have unique global solutions on a fixed interval).

[L2]

One-variable derivatives obey the product rule entrywise (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

Proof

technique · direct

1.1

Fix a compact subinterval $[u, v] \subseteq I$ containing $t_{0}$ . By [F1] and [L1] the matrix ODE below has a unique solution.

F1L1choose

$B^{'} (t) = - B (t) C (t), B (t_{0}) = I_{n},$

has a unique solution $B : [u, v] \to M_{n} (R)$ .

2.1

Entrywise product differentiation from [L2] gives the identity below.

givenL2step 1.1

$\frac{d}{d t} (B (t) A (t)) = B^{'} (t) A (t) + B (t) A^{'} (t) = - B (t) C (t) A (t) + B (t) C (t) A (t) = 0.$

Thus $B (t) A (t)$ is constant on $[u, v]$ . At $t = t_{0}$ this constant is $I_{n} I_{n} = I_{n}$ , so $B (t) A (t) = I_{n}$ for all $t \in [u, v]$ .

3.1

The same calculation applied to $A (t) B (t)$ gives $\frac{d}{d t} (A (t) B (t)) = 0$ and $A (t_{0}) B (t_{0}) = I_{n}$ , hence $A (t) B (t) = I_{n}$ on $[u, v]$ . Therefore $B (t) = A (t)^{- 1}$ and $A (t)$ is invertible on $[u, v]$ . Since $t \in I$ was arbitrary and lies in some compact subinterval containing $t_{0}$ , every $A (t)$ is invertible on $I$ .

givenL2step 1.1step 2.1∎

Depends on

Used by

A linear system and its fundamental matrix Example

Dependency tree · two levels

22 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)