Read-back: HefferonLinAlg.jordan_form_exists

For every natural number $n$ (an implicit argument, so it ranges over all of $\mathbb{N}$ including $n = 0$) and every square matrix $A$ of size $n \times n$ with entries in $\mathbb{C}$, indexed by rows and columns drawn from $\{0, 1, \dots, n-1\}$, the following holds: there exist

• a natural number $k$ (the number of blocks, with $k = 0$ allowed a priori),
• a function $s : \{0,\dots,k-1\} \to \mathbb{N}$ assigning a size $s_i$ to each block, and
• a function $\lambda : \{0,\dots,k-1\} \to \mathbb{C}$ assigning a scalar $\lambda_i$ to each block,

such that both of the following are true.

(a) Every block is nonempty: $s_i > 0$ for all $i \in \{0,\dots,k-1\}$. (Sizes are natural numbers, so this rules out $s_i = 0$ and nothing else; the $s_i$ need not be distinct or ordered, and the $\lambda_i$ need not be distinct either.)

(b) There is a reindexing under which $A$ is similar to the corresponding block-diagonal Jordan matrix. Precisely, let

be the disjoint-union index set of the blocks (so $|I| = \sum_{i} s_i$), and let $J$ be the $I \times I$ matrix over $\mathbb{C}$ that is block-diagonal with $i$-th diagonal block the $s_i \times s_i$ matrix

i.e. $\lambda_i$ on the diagonal and $1$ on the subdiagonal (ones below the diagonal), and $J_{(i,a),(j,b)} = 0$ whenever $i \neq j$. Then the claim is that there exists a bijection

(the existence of such a bijection already forces $\sum_{i} s_i = n$) such that, writing $\widetilde{J}$ for the $n \times n$ matrix obtained by transporting $J$ along $e$, namely $\widetilde{J}_{uv} = J_{e(u),\,e(v)}$, we have that $A$ is similar to $\widetilde{J}$ in the following explicit sense: there exists an $n \times n$ matrix $P$ over $\mathbb{C}$ whose determinant is a unit of $\mathbb{C}$ (equivalently, $\det P \neq 0$, since $\mathbb{C}$ is a field) and which satisfies the equation in this exact orientation

where $P^{-1}$ denotes the matrix-inverse operation, which is a total function in this formalization (returning the zero matrix when the determinant is not invertible) but which, under the stated unit-determinant hypothesis, is the genuine two-sided inverse of $P$.

Scope and edge cases. The statement is an existence claim only: it asserts nothing about uniqueness of $k$, of the multiset of pairs $(s_i, \lambda_i)$, or of $P$ or $e$; no ordering, grouping, or distinctness of blocks or eigenvalues is imposed; and the $\lambda_i$ are not independently required to be eigenvalues, roots of the characteristic polynomial, or otherwise related to $A$ except through the similarity equation above. The auxiliary notion of the multiset $\{(s_i, \lambda_i)\}$ of block data is defined in the accompanying definitions file but does not appear in this statement. The degenerate case $n = 0$ is included, where $A$ is the empty matrix and the claim is satisfiable with $k = 0$ (an empty family of blocks, empty index set $I$, and the empty bijection); the hypothesis-free form of the theorem means there are no assumptions that could be vacuously satisfied — the quantifier over $A$ ranges over every complex square matrix of every size. The scalar field is fixed to $\mathbb{C}$ in this statement, even though the underlying definitions of similarity, Jordan blocks, and Jordan matrices are stated over an arbitrary commutative ring. The declaration is a theorem whose proof is not supplied in this file.