Read-back: HefferonLinAlg.jordan_canonical_form

What the declaration asserts. For every natural number $n$ (implicitly quantified, including $n = 0$) and every $n \times n$ matrix $A$ with complex entries, indexed by $\{0,1,\dots,n-1\}$ in both rows and columns, there exists exactly one finite multiset $B$ of pairs $(m,\mu) \in \mathbb{N} \times \mathbb{C}$ having the following property:

there exist a natural number $k$, a function $s : \{0,\dots,k-1\} \to \mathbb{N}$, and a function $\lambda : \{0,\dots,k-1\} \to \mathbb{C}$ such that $(s,\lambda)$ "is a Jordan form of" $A$ (unfolded below) and the multiset $\{\!\{\,(s_0,\lambda_0),\ (s_1,\lambda_1),\ \dots,\ (s_{k-1},\lambda_{k-1})\,\}\!\}$ — one entry per index $i$, counted with multiplicity, order discarded — is equal to $B$.

Unfolding "$(s,\lambda)$ is a Jordan form of $A$". This is the conjunction of two conditions:

1. Positivity of every block size: $s_i > 0$ for all $i \in \{0,\dots,k-1\}$.
2. Existence of a relabelling and a similarity: there exists a bijection

$$e : \{0,\dots,n-1\} \;\xrightarrow{\ \sim\ }\; I_s := \{\,(i,a) : i \in \{0,\dots,k-1\},\ a \in \{0,\dots,s_i-1\}\,\}$$

(the disjoint-union index set of the blocks) and there exists an $n \times n$ complex matrix $P$ with $\det P$ a unit of $\mathbb{C}$ (equivalently $\det P \neq 0$) such that

$$\bigl(P^{-1} A P\bigr)_{u,v} \;=\; J_{\,e(u),\,e(v)} \qquad \text{for all } u,v \in \{0,\dots,n-1\},$$

where $J$ is the block-diagonal matrix on the index set $I_s$ described next, and $P^{-1}$ is the total inverse operation (a genuine two-sided inverse here, since $\det P$ is a unit). Note the direction of the conjugation: it is $P^{-1} A P$ that equals the relabelled Jordan matrix, not $P A P^{-1}$.

Unfolding the Jordan matrix $J$. $J$ is indexed by pairs $(i,a) \in I_s$ and is block-diagonal:

$$J_{(i,a),(j,b)} \;=\; \begin{cases} \bigl(\text{Jordan block of size } s_i \text{ with eigenvalue } \lambda_i\bigr)_{a,b}, & i = j,\\[2pt] 0, & i \neq j,\end{cases}$$

where the Jordan block of size $m$ with eigenvalue $\mu$ has entries

$$\bigl(\text{block}\bigr)_{a,b} \;=\; \begin{cases} \mu, & a = b,\\ 1, & a = b+1,\\ 0, & \text{otherwise},\end{cases}$$

i.e. $\mu$ on the diagonal and $1$'s on the subdiagonal (below the diagonal), zeros elsewhere.

Exactly what is claimed unique. The uniqueness is asserted only for the multiset $B$. In particular the statement does not claim uniqueness of:

• the number of blocks $k$, or the functions $s$ and $\lambda$ themselves (these are existentially quantified inside the property, so many different $(k,s,\lambda)$ may realise the same $B$);
• the relabelling bijection $e$;
• the change-of-basis matrix $P$.

Because the multiset forgets the ordering of the blocks, the assertion is that the unordered collection of (block size, eigenvalue) pairs, with multiplicities, is determined by $A$.

What the uniqueness statement packages together. The "exactly one" claim carries both halves: (i) existence — at least one such multiset $B$ arises, i.e. every complex square matrix admits a decomposition of the above kind; and (ii) uniqueness — any two multisets arising this way from $A$ coincide.

Degenerate and implicit cases.

• $n = 0$ is included: $A$ is the empty $0\times 0$ matrix, and $k = 0$ with the empty block data satisfies the property vacuously (the positivity condition is vacuous, the empty bijection exists, and the empty matrix is similar to itself), so $B$ is the empty multiset.
• $k = 0$ is permitted in general (the empty multiset $B$); it is compatible with the property only when the index set has $n = 0$ elements.
• The existence of the bijection $e$ forces $n = \sum_{i} s_i$; this is a consequence of the statement rather than something written separately.
• The positivity condition $s_i > 0$ rules out zero-size blocks, so no entry of $B$ has first coordinate $0$.
• Nothing in the statement requires the values $\lambda_i$ to be distinct, nor states explicitly that they are eigenvalues of $A$, nor imposes any ordering on block sizes or eigenvalues.
• The multiset $B$ ranges over pairs whose first coordinate is a natural number and second coordinate a complex number; multiplicities are significant, order is not.
• The scalar field is fixed to $\mathbb{C}$ and the index type to a finite range $\{0,\dots,n-1\}$; no statement is made over other rings or index types.

Proof status. The declaration's proof is not supplied; the body is left as an admitted goal.